CODEWITHSUNDEEP
coqagdadependent-typeidris
Konstantin Solomatov
Konstantin Solomatov

Reputation: 10332

Representing inductive types

I implemented dependently typed lambda calculus in the spirit of this article: http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf The calculus, works and I experimented with it and extended with several things: many universes, hardcoded induction axioms. However, I want to add inductive types to do more complex stuff.

I am thinking about two ways of doing so

I like neither of the ways. The first one is too low level and requires substantial effort for converting from high-level language to the core language. The second way is quite work intensive, and error prone, since generation of recursion principles of complicated inductive types have many corner cases, i.e. positive/negative occurences.

How this can be done? How the types are implemented in existing systems such as Coq, Agda and Idris?

Upvotes: 3

Views: 207

Answers (1)

Vinz
Vinz

Reputation: 6047

Sorry, but I don't know about Idris.

For Agda, I recommend Ulf Norell Phd Thesis as a starting point, but the system evolved since.

Coq introduces a third bullet in your list: automatically generated predicates. Each inductive type comes with 3 (1 in some special cases) induction schemes that are automatically defined for the user, and named your_type_rect, your_type_rec and your_type_ind (only the latter one in the special cases). These are actual terms of the languages, generated automatically for the user, and used by the induction tactic (I'm not 100% sure about that last one), and not axioms.

In fact you can shut down this automatic generation and write your induction schemes yourself.

Some documentation about induction can be found here. I advises that you ask your question on the Coq mailing-list, where devs might give you more insight about the internals of Coq.

Best, V.

Upvotes: 3

Related Questions