[TYPES] Types theories with first-class definitional extensions

[William J. Bowman]

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

-- 
William J. Bowman
Northeastern University
College of Computer and Information Science