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

[Ryan Ingram]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120918/d122f629/attachment.htm>