[Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists

oleg at okmij.org oleg at okmij.org
Sat Sep 22 09:23:38 CEST 2012

> do you have any references for the extension of lambda-encoding of
> data into dependently typed systems?

> Is there a way out of this quagmire?  Or are we stuck defining actual
> datatypes if we want dependent types?

Although not directly answering your question, the following paper

 Inductive Data Types: Well-ordering Types Revisited
 Healfdene Goguen Zhaohui Luo

might still be relevant. Sec 2 reviews the major approaches to
inductive data types in Type Theory.

More information about the Haskell-Cafe mailing list