[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
