Jacques Carette
2016-11-02 02:43:44 UTC
[ 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
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