[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
See my papers with Chris Stone, and his dissertation, on singleton kinds/types, and also David Aspinall’s work on singletons. Bob Harper > On Nov 1, 2016, at 22:43, 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 >
