> On Tue, Sep 18, 2012 at 4:09 PM, Dan Doel <

dan.doel <at> gmail.com> wrote:

>>

>> 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.spam <at> 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, <

oleg <at> 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 <at> haskell.org
>> >>

http://www.haskell.org/mailman/listinfo/haskell-cafe
>> >

>> >

>> >

>> > _______________________________________________

>> > Haskell-Cafe mailing list

>> >

Haskell-Cafe <at> haskell.org
>> >

http://www.haskell.org/mailman/listinfo/haskell-cafe
>> >

>

>