This paper: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.957
Induction is Not Derivable in Second Order Dependent Type Theory, shows, well, that you can't encode naturals with a strong induction principle in said theory. At all, no matter what tricks you try. However, A Logic for Parametric Polymorphism, http://www.era.lib.ed.ac.uk/bitstream/1842/205/1/Par_Poly.pdf Indicates that in a type theory incorporating relational parametricity of its own types, the induction principle for the ordinary Church-like encoding of natural numbers can be derived. I've done some work here: http://code.haskell.org/~dolio/agda-share/html/ParamInduction.html for some simpler types (although, I've been informed that sigma was novel, it not being a Simple Type), but haven't figured out natural numbers yet (I haven't actually studied the second paper above, which I was pointed to recently). -- Dan On Tue, Sep 18, 2012 at 5:41 PM, Ryan Ingram <ryani.s...@gmail.com> wrote: > Oleg, do you have any references for the extension of lambda-encoding of > data into dependently typed systems? > > In particular, consider Nat: > > nat_elim :: forall P:(Nat -> *). P 0 -> (forall n:Nat. P n -> P (succ > n)) -> (n:Nat) -> P n > > The naive lambda-encoding of 'nat' in the untyped lambda-calculus has > exactly the correct form for passing to nat_elim: > > nat_elim pZero pSucc n = n pZero pSucc > > with > > zero :: Nat > zero pZero pSucc = pZero > > succ :: Nat -> Nat > succ n pZero pSucc = pSucc (n pZero pSucc) > > But trying to encode the numerals this way leads to "Nat" referring to its > value in its type! > > type Nat = forall P:(Nat -> *). P 0 -> (forall n:Nat. P n -> P (succ n)) > -> P ??? > > Is there a way out of this quagmire? Or are we stuck defining actual > datatypes if we want dependent types? > > -- ryan > > > > On Tue, Sep 18, 2012 at 1:27 AM, <o...@okmij.org> wrote: >> >> >> There has been a recent discussion of ``Church encoding'' of lists and >> the comparison with Scott encoding. >> >> I'd like to point out that what is often called Church encoding is >> actually Boehm-Berarducci encoding. That is, often seen >> >> > newtype ChurchList a = >> > CL { cataCL :: forall r. (a -> r -> r) -> r -> r } >> >> (in http://community.haskell.org/%7Ewren/list-extras/Data/List/Church.hs ) >> >> is _not_ Church encoding. First of all, Church encoding is not typed >> and it is not tight. The following article explains the other >> difference between the encodings >> >> http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html >> >> Boehm-Berarducci encoding is very insightful and influential. The >> authors truly deserve credit. >> >> P.S. It is actually possible to write zip function using Boehm-Berarducci >> encoding: >> http://okmij.org/ftp/ftp/Algorithms.html#zip-folds >> >> >> >> >> _______________________________________________ >> Haskell-Cafe mailing list >> Haskell-Cafe@haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe > > > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe