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

[Dan Doel]

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
>