[TYPES] Types theories with first-class definitional extensions

[Frank Pfenning]

Since you are mentioning the pragmatics, we did quite a bit of work in
Twelf to handle notational definitions efficiently, which doesn't seem to
be widely known.  First, there is the notion of *strict definitions*

Frank Pfenning and Carsten Schürmann. Algorithms for equality and
unification in the presence of notational definitions
<http://www.cs.cmu.edu/~fp/papers/types98.pdf>, TYPES'98.

which, in the implementation, is combined with a "depth index" to steer
minimal incremental expansion of definitions for the purpose of equality
testing and unification.  This has been extended to encompass proof
irrelevance.

Jason Reed, Proof Irrelevance and Strict Definitions in a Logical Framework
<http://reports-archive.adm.cs.cmu.edu/anon/2002/CMU-CS-02-153.pdf>, TR
CMU-CS-02-153, June 2002

and there also has been quite a bit on redundancy elimination in dependent
type theories, which interacts with notational definitions.
Jason Reed.  Redundancy Elimination for LF
<http://www.cs.cmu.edu/~jcreed/papers/lfm2004.ps>. LFM'04.

    - Frank


On Tue, Nov 1, 2016 at 10: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
>
>


-- 
Frank Pfenning, Professor and Head
Department of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213-3891

http://www.cs.cmu.edu/~fp
+1 412 268-6343
GHC 7019