> 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 http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.17.8970&rep=rep1&type=pdf might still be relevant. Sec 2 reviews the major approaches to inductive data types in Type Theory. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
