Re: [TYPES] Types theories with first-class definitional extensions
"William J. Bowman" <wjb-r2/fXjr+/[email protected]>
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] 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