[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Jacques,
Most refinement type systems can do something _like_ adding equalities using
“selfified” types (Ou et al., TCS 2004) like {x:Int | x = 5}, i.e., x is an Int
such that x is 5. The Sage language (Knowles et al., Scheme Workshop 2006) adds
equalities to the context in a more direct way. Knowles and Flanagan have a
technical report that uses existentials to tame the holes in the dyke of
abstraction introduced by dependent types
<https://sage.soe.ucsc.edu/UCSC-SOE-08-17.pdf>.
Cheers,
Michael
> On Nov 1, 2016, at 7:43 PM, Jacques Carette <[email protected]> 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.
>
> Of course, from a semantic point of view, this is entirely unnecessary, as
> such definitions can simply be expanded away. However, from a categorical
> standpoint (amongst others), things are not so trivial: what is the proper
> meaning of morphisms (substitutions) in such a case?
>
> The motivation comes from the remark that the category of contexts for a type
> theory is the opposite category of that of theory presentations (aka
> algebraic theories, algebraic specifications, etc). By applying the 'little
> theories' approach, it is really the theory morphisms that carry the most
> interesting information. And that, in practice, one uses "conservative
> extensions" of theories all the time.
>
> Some concrete examples:
> - in Agda, in a parametric record definition, one can also define generic
> functions which 'depend' on the fields of the record;
> - in Haskell, in a typeclass definition, one can define default
> implementations;
> - in Scala, in a trait, one can similarly define default implementations.
> These 3 things are essentially the same idea, of a conservative extension of
> a theory.
>
> The problem arises when one wants to build theory morphisms (which would be
> typeclass-to-typeclass functions in Haskell, or trait-to-trait functions in
> Scala, neither of which are available AFAIK): what to do with the
> definitions? Again, from a semantic point-of-view, there is no intrinsic
> difficulty, and multiple different designs are equivalent. The question only
> really becomes interesting when considering the pragmatics. Some designs
> lead to huge combinatorial explosions of definitions once your theory library
> gets into the 100s of theories, never mind the 1000s, which is what a
> realistic library of mathematics+CS needs.
>
> This is not entirely straightforward. For example, the old theorem prover
> IMPS actually has 4 different ways to handle the transport of definitional
> extension along theory morphisms.
>
> I have tried to look into the literature for related work, but I have not
> been successful. Thus this query.
>
> Jacques
>
