[TYPES] Types theories with first-class definitional extensions

[Jacques Carette]

Thanks for the many answers.  Some of my comments below could have been 
attached to other answers as well - I am not targetting CIC or 
transculent sums in particular!

On 2016-11-02 12:26 PM, William J. Bowman wrote:
> On Tue, Nov 01, 2016 at 10:43:44PM -0400, Jacques Carette wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>> I am looking for literature on (higher-order, potentially dependent) type
>> theories where a context (telescope) can contain not just declarations, but
>> also definitions.
> I may misunderstand your question, but doesn't CIC have this (and other languages with dependent let)?
>
> The typing rule for dependent let adds a definition to the context:
>
> Δ;Γ ⊢ e : t
> Δ;Γ,x = e :t ⊢ e' : t
> ----------------------
> Δ;Γ ⊢ let x = e in e' : t[e/x]
>
> https://coq.inria.fr/refman/Reference-Manual006.html
>
> This also reminds me of translucency.
> A translucent type add a definition to the type declaration:
>
> (x = e : t) -> t'
> ∃ (x = e : t). t
>
> The original work on translucent sums:
> https://www.cs.cmu.edu/~rwh/theses/lillibridge.pdf
>
> I've also seen translucent functions here, which has a good explanation of translucency and more
> citations to chase:
> http://dl.acm.org/citation.cfm?id=237791
>

This seems really close, but there is something I don't see: how are the 
morphisms defined in the Contextual Category that corresponds to Coq's 
CIC's term language?  The 'obvious' definition of substitution works, 
but has very unpleasant properties, especially if you are trying to 
build a nice user interface.  The language of "with" for type signatures 
is very impoverished, and not up to the job of doing that.

It is not so much just having definitional extensions which are of 
interest (as that's been around for a long time), but having good 
behaviour, especially good *syntactic* behaviour, under repeated transport.

For an extreme example of this, see
     Adrian Mathias, A Term of Length 4,523,659,424,929 
<http://www.dpmms.cam.ac.uk/%7Eardm/inefff.dvi>, Synthese 133 (2002) 75--86.
     https://www.dpmms.cam.ac.uk/~ardm/inefff.pdf

Buried in an answer on
http://mathoverflow.net/questions/14356/bourbakis-epsilon-calculus-notation
you can also find similar numbers for ZFC.

Without care, the same can happen in a type theory, if definitional 
extensions are not treated as having important syntactic content, along 
with its (trivial!) semantic content.

Jacques