[TYPES] Types theories with first-class definitional extensions

[Michael Greenberg]

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 <carette at mcmaster.ca> 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
>