headers
oleg | 18 Sep 2012 10:27

Church vs Boehm-Berarducci encoding of Lists


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
Permalink | Reply |
headers
Ivan Lazar Miljenovic | 18 Sep 2012 11:07
Picon
Gravatar

Re: Church vs Boehm-Berarducci encoding of Lists

On 18 September 2012 18:27,  <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

You have one too many "ftp/" in there (in case others get confused
about why the link fails).

>
(Continue reading)

Permalink | Reply |
headers
Kim-Ee Yeoh | 18 Sep 2012 11:15
Favicon

Re: Church vs Boehm-Berarducci encoding of Lists

Oleg,


Let me try to understand what you're saying here:

(1) Church encoding was discovered and investigated in an untyped setting. I understand your tightness criterion to mean surjectivity, the absence of which means having to deal with junk.

(2) Church didn't give an encoding for pattern-matching to match with construction. Boehm and Berarducci did. So properly speaking, tail and pred for Church-encoded lists and nats are trial-and-error affairs. But the point is they need not be if we use B-B encoding, which looks _exactly_ the same, except one gets a citation link to a systematic procedure.

So it looks like you're trying to set the record straight on who actually did what.


-- Kim-Ee


On Tue, Sep 18, 2012 at 3:27 PM, <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
Permalink | Reply |
headers
Ryan Ingram | 18 Sep 2012 23:41
Picon

Re: Church vs Boehm-Berarducci encoding of Lists

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
Permalink | Reply |
headers
Dan Doel | 19 Sep 2012 01:09
Picon
Gravatar

Re: Church vs Boehm-Berarducci encoding of Lists

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
>
Permalink | Reply |
headers
Ryan Ingram | 19 Sep 2012 05:19
Picon

Re: Church vs Boehm-Berarducci encoding of Lists

Fascinating!

But it looks like you still 'cheat' in your induction principles...

×-induction : ∀{A B} {P : A × B → Set} → ((x : A) → (y : B) → P (x , y)) → (p : A × B) → P p ×-induction {A} {B} {P} f p rewrite sym (×-η p) = f (fst p) (snd p)Can you somehow define

x-induction {A} {B} {P} f p = p (P p) f


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
>

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |
headers
Dan Doel | 19 Sep 2012 05:39
Picon
Gravatar

Re: Church vs Boehm-Berarducci encoding of Lists

On Tue, Sep 18, 2012 at 11:19 PM, Ryan Ingram <ryani.spam <at> gmail.com> wrote:
> Fascinating!
>
> But it looks like you still 'cheat' in your induction principles...
>
> ×-induction : ∀{A B} {P : A × B → Set}
>             → ((x : A) → (y : B) → P (x , y))
>             → (p : A × B) → P p
> ×-induction {A} {B} {P} f p rewrite sym (×-η p) = f (fst p) (snd p)
>
> Can you somehow define
>
> x-induction {A} {B} {P} f p = p (P p) f

No, or at least I don't know how.

The point is that with parametricity, I can prove that if p : A × B,
then p = (fst p , snd p). Then when I need to prove P p, I change the
obligation to P (fst p , snd p). But i have (forall x y. P (x , y))
given.

I don't know why you think that's cheating. If you thought it was
going to be a straight-forward application of the Church (or some
other) encoding, that was the point of the first paper (that's
impossible). But parametricity can be used to prove statements _about_
the encodings that imply the induction principle.

> 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
>> >
>
>

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |
headers
Ryan Ingram | 19 Sep 2012 05:58
Picon

Re: Church vs Boehm-Berarducci encoding of Lists

On Tue, Sep 18, 2012 at 8:39 PM, Dan Doel <dan.doel <at> gmail.com> wrote:

On Tue, Sep 18, 2012 at 11:19 PM, Ryan Ingram <ryani.spam <at> gmail.com> wrote:
> Fascinating!
>
> But it looks like you still 'cheat' in your induction principles...
>
> ×-induction : ∀{A B} {P : A × B → Set}
>             → ((x : A) → (y : B) → P (x , y))
>             → (p : A × B) → P p
> ×-induction {A} {B} {P} f p rewrite sym (×-η p) = f (fst p) (snd p)
>
> Can you somehow define
>
> x-induction {A} {B} {P} f p = p (P p) f

No, or at least I don't know how.

The point is that with parametricity, I can prove that if p : A × B,
then p = (fst p , snd p). Then when I need to prove P p, I change the
obligation to P (fst p , snd p). But i have (forall x y. P (x , y))
given.

I don't know why you think that's cheating. If you thought it was
going to be a straight-forward application of the Church (or some
other) encoding, that was the point of the first paper (that's
impossible). But parametricity can be used to prove statements _about_
the encodings that imply the induction principle.

The line of logic I was thinking is that you could lift the parametricity proof to the (proof-irrelevant) typelevel; that is, you rewrite the type of f from

f :: (x : A) -> (y : B) -> P (x,y)

to

f :: A -> B -> P p

given that p = (x,y), to make f 'compatible' with p.  But I see the trickiness, because if you allow yourself to do that, you no longer are constrained to pass (fst p) and (snd p) to f, you could pass any objects of type A and B.

Wait, can't you just use x-lemma1 to rewrite the rhs of x-induction?
×-lemma₁ : ∀{A B R} → (p : A × B) (k : A → B → R) → k (fst p) (snd p) ≡ p R k
x-lemma1 {A} {B} {P p} p f :: f (fst p) (snd p) = p (P p) f

Or is the problem that the "k" parameter to x-lemma1 isn't 'dependently typed' enough?

  -- ryan

 

> 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
>> >
>
>

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |
headers
oleg | 22 Sep 2012 09:23

Re: Church vs Boehm-Berarducci encoding of Lists


> 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.
Permalink | Reply |
headers
wren ng thornton | 20 Sep 2012 02:36

Re: Church vs Boehm-Berarducci encoding of Lists

On 9/18/12 4: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.

I know that Church encodings were explored in the untyped setting (and 
hence cannot be tight); but I was unaware of a citation for the typed 
version of the same encoding. I've since corrected the names of the 
above module.

N.B., for folks following along at home, the above module and the Scott 
version aren't actually in list-extras yet. I just dumped them there for 
lack of somewhere else to stash the code from last time this comparison 
came up.

> P.S. It is actually possible to write zip function using Boehm-Berarducci
> encoding:
> 	http://okmij.org/ftp/ftp/Algorithms.html#zip-folds

Of course it is; I just never got around to doing it :)

--

-- 
Live well,
~wren
Permalink | Reply |
headers
Dan Doel | 20 Sep 2012 03:24
Picon
Gravatar

Re: Church vs Boehm-Berarducci encoding of Lists

On Wed, Sep 19, 2012 at 8:36 PM, wren ng thornton <wren <at> freegeek.org> wrote:
>> P.S. It is actually possible to write zip function using Boehm-Berarducci
>> encoding:
>>         http://okmij.org/ftp/ftp/Algorithms.html#zip-folds
>
>
> Of course it is; I just never got around to doing it :)

If you do, you might want to consider not using the above method, as I
seem to recall it doing an undesirable amount of extra work (repeated
O(n) tail). One can do better with some controversial types (this is
not my idea originally; ski (don't know his real name) on freenode's
#haskell showed it to me a long time ago):

---- snip ----

{-# LANGUAGE PolymorphicComponents #-}

module ABC where

newtype L a = L { unL :: forall r. (a -> r -> r) -> r -> r }

nil :: L a
nil = L $ \_ z -> z

cons :: a -> L a -> L a
cons x (L xs) = L $ \f -> f x . xs f

newtype A a c = Roll { unroll :: (a -> A a c -> L c) -> L c }

type B a c = a -> A a c -> L c

zipWith :: (a -> b -> c) -> L a -> L b -> L c
zipWith f (L as) (L bs) = unroll (as consA nilA) (bs consB nilB)
 where
 -- nilA :: A a c
 nilA = Roll $ const nil

 -- consA :: a -> A a c -> A a c
 consA x xs = Roll $ \k -> k x xs

 -- nilB :: B a c
 nilB _ _ = nil

 -- consB :: b -> B a c -> B a c
 consB y ys x xs = f x y `cons` unroll xs ys

---- snip ----

This traverses each list only once.

-- Dan
Permalink | Reply |
headers
oleg | 20 Sep 2012 10:15

Re: Church vs Boehm-Berarducci encoding of Lists


Dan Doel wrote:
> >> P.S. It is actually possible to write zip function using Boehm-Berarducci
> >> encoding:
> >>         http://okmij.org/ftp/Algorithms.html#zip-folds
>
> If you do, you might want to consider not using the above method, as I
> seem to recall it doing an undesirable amount of extra work (repeated
> O(n) tail). 
It is correct. The Boehm-Berarducci web page discusses at some extent
the general inefficiency of the encoding, the need for repeated
reflections and reifications for some (but not all) operations. That
is why arithmetic on Church numerals is generally a bad idea.

A much better encoding of numerals is what I call P-numerals
	http://okmij.org/ftp/Computation/lambda-calc.html#p-numerals
It turns out, I have re-discovered them after Michel Parigot (so my
name P-numerals is actually meaningful). Not only they are faster; one
can _syntactically_ prove that PRED . SUCC is the identity.

The general idea of course is Goedel's recursor R.

   R b a 0 = a
   R b a (Succ n) = b n (R b a n)

which easily generalizes to lists. The enclosed code shows the list
encoding that has constant-time cons, head, tail and trivially
expressible fold and zip.

Kim-Ee Yeoh wrote:
> So properly speaking, tail and pred for Church-encoded lists and nats
> are trial-and-error affairs. But the point is they need not be if we
> use B-B encoding, which looks _exactly_ the same, except one gets a
> citation link to a systematic procedure.
>
> So it looks like you're trying to set the record straight on who actually
> did what.

Exactly. Incidentally, there is more than one way to build a
predecessor of Church numerals. Kleene's solution is not the only
one. Many years ago I was thinking on this problem and designed a
different predecessor:

excerpted from http://okmij.org/ftp/Haskell/LC_neg.lhs

    One ad hoc way of defining a predecessor of a positive numeral
		    predp cn+1 ==> cn
    is to represent "predp cn" as "cn f v"
    where f and v are so chosen that (f z) acts as
	    if z == v then c0 else (succ z)
    We know that z can be either a numeral cn or a special value v. All
    Church numerals have a property that (cn combI) is combI: the identity
    combinator is a fixpoint of every numeral. Therefore, ((cn combI) (succ
    cn)) reduces to (succ cn). We only need to choose the value v in such
    a way that ((v I) (succ v)) yields c0.

    > predp = eval $
    >   c ^ c 
    >        # (z ^ (z # combI # (succ # z)))       -- function f(z)
    >        # (a ^ x ^ c0)                         -- value v

{-# LANGUAGE Rank2Types #-}

-- List represented with R

newtype R x = R{unR :: forall w.
  -- b
  (x -> R x -> w -> w)
  -- a
  -> w
  -- result
  -> w}

nil :: R x
nil = R (\b a -> a)

-- constant type
cons :: x -> R x -> R x
cons x r = R(\b a -> b x r (unR r b a))

-- constant time
rhead :: R x -> x
rhead (R fr) = fr (\x _ _ -> x) (error "head of the empty list")

-- constant time
rtail :: R x -> R x
rtail (R fr) = fr (\_ r _ -> r) (error "tail of the empty list")

-- fold
rfold :: (x -> w -> w) -> w -> R x -> w
rfold f z (R fr) = fr (\x _ w -> f x w) z

-- zip is expressed via fold
rzipWith :: (x -> y -> z) -> R x -> R y -> R z
rzipWith f r1 r2 =  rfold f' z r1 r2
 where f' x tD = \r2 -> cons (f x (rhead r2)) (tD (rtail r2))
       z       = \_  -> nil

-- tests

toR :: [a] -> R a
toR = foldr cons nil

toL :: R a -> [a]
toL = rfold (:) []

l1 = toR [1..10]
l2 = toR "abcde"

t1 = toL $ rtail l2
-- "bcde"

t2 = toL $ rzipWith (,) l2 l1
-- [('a',1),('b',2),('c',3),('d',4),('e',5)]
Permalink | Reply |
headers
Jay Sulzberger | 20 Sep 2012 21:54
Picon
Favicon

Re: Church vs Boehm-Berarducci encoding of Lists


On Thu, 20 Sep 2012, oleg <at> okmij.org wrote:

>
> Dan Doel wrote:
>>>> P.S. It is actually possible to write zip function using Boehm-Berarducci
>>>> encoding:
>>>>         http://okmij.org/ftp/Algorithms.html#zip-folds
>>
>> If you do, you might want to consider not using the above method, as I
>> seem to recall it doing an undesirable amount of extra work (repeated
>> O(n) tail).
> It is correct. The Boehm-Berarducci web page discusses at some extent
> the general inefficiency of the encoding, the need for repeated
> reflections and reifications for some (but not all) operations. That
> is why arithmetic on Church numerals is generally a bad idea.
>
> A much better encoding of numerals is what I call P-numerals
> 	http://okmij.org/ftp/Computation/lambda-calc.html#p-numerals
> It turns out, I have re-discovered them after Michel Parigot (so my
> name P-numerals is actually meaningful). Not only they are faster; one
> can _syntactically_ prove that PRED . SUCC is the identity.

What is the setup that, here, gives the distinction between a
syntactic proof and some other kind of proof?

oo--JS.

>
> The general idea of course is Goedel's recursor R.
>
>   R b a 0 = a
>   R b a (Succ n) = b n (R b a n)
>
> which easily generalizes to lists. The enclosed code shows the list
> encoding that has constant-time cons, head, tail and trivially
> expressible fold and zip.
>
>
> Kim-Ee Yeoh wrote:
>> So properly speaking, tail and pred for Church-encoded lists and nats
>> are trial-and-error affairs. But the point is they need not be if we
>> use B-B encoding, which looks _exactly_ the same, except one gets a
>> citation link to a systematic procedure.
>>
>> So it looks like you're trying to set the record straight on who actually
>> did what.
>
> Exactly. Incidentally, there is more than one way to build a
> predecessor of Church numerals. Kleene's solution is not the only
> one. Many years ago I was thinking on this problem and designed a
> different predecessor:
>
> excerpted from http://okmij.org/ftp/Haskell/LC_neg.lhs
>
>
>    One ad hoc way of defining a predecessor of a positive numeral
> 		    predp cn+1 ==> cn
>    is to represent "predp cn" as "cn f v"
>    where f and v are so chosen that (f z) acts as
> 	    if z == v then c0 else (succ z)
>    We know that z can be either a numeral cn or a special value v. All
>    Church numerals have a property that (cn combI) is combI: the identity
>    combinator is a fixpoint of every numeral. Therefore, ((cn combI) (succ
>    cn)) reduces to (succ cn). We only need to choose the value v in such
>    a way that ((v I) (succ v)) yields c0.
>
>    > predp = eval $
>    >   c ^ c
>    >        # (z ^ (z # combI # (succ # z)))       -- function f(z)
>    >        # (a ^ x ^ c0)                         -- value v
>
>
> {-# LANGUAGE Rank2Types #-}
>
> -- List represented with R
>
> newtype R x = R{unR :: forall w.
>  -- b
>  (x -> R x -> w -> w)
>  -- a
>  -> w
>  -- result
>  -> w}
>
> nil :: R x
> nil = R (\b a -> a)
>
> -- constant type
> cons :: x -> R x -> R x
> cons x r = R(\b a -> b x r (unR r b a))
>
> -- constant time
> rhead :: R x -> x
> rhead (R fr) = fr (\x _ _ -> x) (error "head of the empty list")
>
> -- constant time
> rtail :: R x -> R x
> rtail (R fr) = fr (\_ r _ -> r) (error "tail of the empty list")
>
> -- fold
> rfold :: (x -> w -> w) -> w -> R x -> w
> rfold f z (R fr) = fr (\x _ w -> f x w) z
>
> -- zip is expressed via fold
> rzipWith :: (x -> y -> z) -> R x -> R y -> R z
> rzipWith f r1 r2 =  rfold f' z r1 r2
> where f' x tD = \r2 -> cons (f x (rhead r2)) (tD (rtail r2))
>       z       = \_  -> nil
>
> -- tests
>
> toR :: [a] -> R a
> toR = foldr cons nil
>
> toL :: R a -> [a]
> toL = rfold (:) []
>
>
> l1 = toR [1..10]
> l2 = toR "abcde"
>
>
> t1 = toL $ rtail l2
> -- "bcde"
>
> t2 = toL $ rzipWith (,) l2 l1
> -- [('a',1),('b',2),('c',3),('d',4),('e',5)]
>
Permalink | Reply |
headers
Jay Sulzberger | 20 Sep 2012 22:00
Picon
Favicon

Re: Church vs Boehm-Berarducci encoding of Lists


On Thu, 20 Sep 2012, Jay Sulzberger wrote:

>
>
> On Thu, 20 Sep 2012, oleg <at> okmij.org wrote:
>
>> 
>> Dan Doel wrote:
>>>>> P.S. It is actually possible to write zip function using 
>>>>> Boehm-Berarducci
>>>>> encoding:
>>>>>         http://okmij.org/ftp/Algorithms.html#zip-folds
>>> 
>>> If you do, you might want to consider not using the above method, as I
>>> seem to recall it doing an undesirable amount of extra work (repeated
>>> O(n) tail).
>> It is correct. The Boehm-Berarducci web page discusses at some extent
>> the general inefficiency of the encoding, the need for repeated
>> reflections and reifications for some (but not all) operations. That
>> is why arithmetic on Church numerals is generally a bad idea.
>> 
>> A much better encoding of numerals is what I call P-numerals
>> 	http://okmij.org/ftp/Computation/lambda-calc.html#p-numerals
>> It turns out, I have re-discovered them after Michel Parigot (so my
>> name P-numerals is actually meaningful). Not only they are faster; one
>> can _syntactically_ prove that PRED . SUCC is the identity.
>
> What is the setup that, here, gives the distinction between a
> syntactic proof and some other kind of proof?
>
> oo--JS.

Ah, I have just read the for-any vs for-all part of

   http://okmij.org/ftp/Computation/lambda-calc.html#p-numerals

and I think I understand something.

oo--JS.

>
>
>> 
>> The general idea of course is Goedel's recursor R.
>>
>>   R b a 0 = a
>>   R b a (Succ n) = b n (R b a n)
>> 
>> which easily generalizes to lists. The enclosed code shows the list
>> encoding that has constant-time cons, head, tail and trivially
>> expressible fold and zip.
>> 
>> 
>> Kim-Ee Yeoh wrote:
>>> So properly speaking, tail and pred for Church-encoded lists and nats
>>> are trial-and-error affairs. But the point is they need not be if we
>>> use B-B encoding, which looks _exactly_ the same, except one gets a
>>> citation link to a systematic procedure.
>>> 
>>> So it looks like you're trying to set the record straight on who actually
>>> did what.
>> 
>> Exactly. Incidentally, there is more than one way to build a
>> predecessor of Church numerals. Kleene's solution is not the only
>> one. Many years ago I was thinking on this problem and designed a
>> different predecessor:
>> 
>> excerpted from http://okmij.org/ftp/Haskell/LC_neg.lhs
>> 
>>
>>    One ad hoc way of defining a predecessor of a positive numeral
>> 		    predp cn+1 ==> cn
>>    is to represent "predp cn" as "cn f v"
>>    where f and v are so chosen that (f z) acts as
>> 	    if z == v then c0 else (succ z)
>>    We know that z can be either a numeral cn or a special value v. All
>>    Church numerals have a property that (cn combI) is combI: the identity
>>    combinator is a fixpoint of every numeral. Therefore, ((cn combI) (succ
>>    cn)) reduces to (succ cn). We only need to choose the value v in such
>>    a way that ((v I) (succ v)) yields c0.
>>
>>    > predp = eval $
>>    >   c ^ c
>>    >        # (z ^ (z # combI # (succ # z)))       -- function f(z)
>>    >        # (a ^ x ^ c0)                         -- value v
>> 
>> 
>> {-# LANGUAGE Rank2Types #-}
>> 
>> -- List represented with R
>> 
>> newtype R x = R{unR :: forall w.
>>  -- b
>>  (x -> R x -> w -> w)
>>  -- a
>>  -> w
>>  -- result
>>  -> w}
>> 
>> nil :: R x
>> nil = R (\b a -> a)
>> 
>> -- constant type
>> cons :: x -> R x -> R x
>> cons x r = R(\b a -> b x r (unR r b a))
>> 
>> -- constant time
>> rhead :: R x -> x
>> rhead (R fr) = fr (\x _ _ -> x) (error "head of the empty list")
>> 
>> -- constant time
>> rtail :: R x -> R x
>> rtail (R fr) = fr (\_ r _ -> r) (error "tail of the empty list")
>> 
>> -- fold
>> rfold :: (x -> w -> w) -> w -> R x -> w
>> rfold f z (R fr) = fr (\x _ w -> f x w) z
>> 
>> -- zip is expressed via fold
>> rzipWith :: (x -> y -> z) -> R x -> R y -> R z
>> rzipWith f r1 r2 =  rfold f' z r1 r2
>> where f' x tD = \r2 -> cons (f x (rhead r2)) (tD (rtail r2))
>>       z       = \_  -> nil
>> 
>> -- tests
>> 
>> toR :: [a] -> R a
>> toR = foldr cons nil
>> 
>> toL :: R a -> [a]
>> toL = rfold (:) []
>> 
>> 
>> l1 = toR [1..10]
>> l2 = toR "abcde"
>> 
>> 
>> t1 = toL $ rtail l2
>> -- "bcde"
>> 
>> t2 = toL $ rzipWith (,) l2 l1
>> -- [('a',1),('b',2),('c',3),('d',4),('e',5)]
>> 
>
>
Permalink | Reply |
headers
Kim-Ee Yeoh | 23 Sep 2012 16:36
Favicon

Re: Church vs Boehm-Berarducci encoding of Lists

On Thu, Sep 20, 2012 at 3:15 PM,<oleg <at> okmij.org> wrote:
Incidentally, there is more than one way to build a predecessor of Church numerals. Kleene's solution is not the only one. 

Wouldn't you say then that "Church encoding" is still the more appropriate reference given that Boehm-Berarducci's algorithm is rarely used? And also that on discovering Church numerals in the untyped setting, one easily sees how to get it to work in Haskell? Even when one has no inkling of the larger picture of the embedding into System F?

When I need to encode pattern matching it's goodbye Church and hello Scott. Aside from your projects, where else is the B-B procedure used?


-- Kim-Ee


On Thu, Sep 20, 2012 at 3:15 PM, <oleg <at> okmij.org> wrote:

Dan Doel wrote:
> >> P.S. It is actually possible to write zip function using Boehm-Berarducci
> >> encoding:
> >>         http://okmij.org/ftp/Algorithms.html#zip-folds
>
> If you do, you might want to consider not using the above method, as I
> seem to recall it doing an undesirable amount of extra work (repeated
> O(n) tail).
It is correct. The Boehm-Berarducci web page discusses at some extent
the general inefficiency of the encoding, the need for repeated
reflections and reifications for some (but not all) operations. That
is why arithmetic on Church numerals is generally a bad idea.

A much better encoding of numerals is what I call P-numerals
        http://okmij.org/ftp/Computation/lambda-calc.html#p-numerals
It turns out, I have re-discovered them after Michel Parigot (so my
name P-numerals is actually meaningful). Not only they are faster; one
can _syntactically_ prove that PRED . SUCC is the identity.

The general idea of course is Goedel's recursor R.

   R b a 0 = a
   R b a (Succ n) = b n (R b a n)

which easily generalizes to lists. The enclosed code shows the list
encoding that has constant-time cons, head, tail and trivially
expressible fold and zip.


Kim-Ee Yeoh wrote:
> So properly speaking, tail and pred for Church-encoded lists and nats
> are trial-and-error affairs. But the point is they need not be if we
> use B-B encoding, which looks _exactly_ the same, except one gets a
> citation link to a systematic procedure.
>
> So it looks like you're trying to set the record straight on who actually
> did what.

Exactly. Incidentally, there is more than one way to build a
predecessor of Church numerals. Kleene's solution is not the only
one. Many years ago I was thinking on this problem and designed a
different predecessor:

excerpted from http://okmij.org/ftp/Haskell/LC_neg.lhs


    One ad hoc way of defining a predecessor of a positive numeral
                    predp cn+1 ==> cn
    is to represent "predp cn" as "cn f v"
    where f and v are so chosen that (f z) acts as
            if z == v then c0 else (succ z)
    We know that z can be either a numeral cn or a special value v. All
    Church numerals have a property that (cn combI) is combI: the identity
    combinator is a fixpoint of every numeral. Therefore, ((cn combI) (succ
    cn)) reduces to (succ cn). We only need to choose the value v in such
    a way that ((v I) (succ v)) yields c0.

    > predp = eval $
    >   c ^ c
    >        # (z ^ (z # combI # (succ # z)))       -- function f(z)
    >        # (a ^ x ^ c0)                         -- value v


{-# LANGUAGE Rank2Types #-}

-- List represented with R

newtype R x = R{unR :: forall w.
  -- b
  (x -> R x -> w -> w)
  -- a
  -> w
  -- result
  -> w}

nil :: R x
nil = R (\b a -> a)

-- constant type
cons :: x -> R x -> R x
cons x r = R(\b a -> b x r (unR r b a))

-- constant time
rhead :: R x -> x
rhead (R fr) = fr (\x _ _ -> x) (error "head of the empty list")

-- constant time
rtail :: R x -> R x
rtail (R fr) = fr (\_ r _ -> r) (error "tail of the empty list")

-- fold
rfold :: (x -> w -> w) -> w -> R x -> w
rfold f z (R fr) = fr (\x _ w -> f x w) z

-- zip is expressed via fold
rzipWith :: (x -> y -> z) -> R x -> R y -> R z
rzipWith f r1 r2 =  rfold f' z r1 r2
 where f' x tD = \r2 -> cons (f x (rhead r2)) (tD (rtail r2))
       z       = \_  -> nil

-- tests

toR :: [a] -> R a
toR = foldr cons nil

toL :: R a -> [a]
toL = rfold (:) []


l1 = toR [1..10]
l2 = toR "abcde"


t1 = toL $ rtail l2
-- "bcde"

t2 = toL $ rzipWith (,) l2 l1
-- [('a',1),('b',2),('c',3),('d',4),('e',5)]



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |
headers
oleg | 26 Sep 2012 06:41

Re: Church vs Boehm-Berarducci encoding of Lists


> Wouldn't you say then that "Church encoding" is still the more appropriate
> reference given that Boehm-Berarducci's algorithm is rarely used? 
>
> When I need to encode pattern matching it's goodbye Church and hello Scott.
> Aside from your projects, where else is the B-B procedure used?

First of all, the Boehm-Berarducci encoding is inefficient only when
doing an operation that is not easily representable as a fold. Quite
many problems can be efficiently tackled by a fold.

Second, I must stress the foundational advantage of the
Boehm-Berarducci encoding: plain System F. Boehm-Berarducci encoding
uses _no_ recursion: not at the term level, not at the type level.  In
contrast, the efficient for pattern-match encodings need general
recursive types. With such types, a fix-point combinator becomes
expressible, and the system, as a logic, becomes inconsistent.
Permalink | Reply |
headers
Dan Doel | 26 Sep 2012 07:06
Picon
Gravatar

Re: Church vs Boehm-Berarducci encoding of Lists

On Wed, Sep 26, 2012 at 12:41 AM,  <oleg <at> okmij.org> wrote:
> First of all, the Boehm-Berarducci encoding is inefficient only when
> doing an operation that is not easily representable as a fold. Quite
> many problems can be efficiently tackled by a fold.

Indeed. Some operations are even more efficient than usually expected
when operating on folds. For instance:

    snoc xs x f = xs f . f x

People often recommend using ([a] -> [a]) for efficiently building up
lists without worrying about introducing O(n^2) costs through bad
associativity, but the Boehm-Berarducci encoding gets you that and
more (map g xs f = xs (f . g) ; map h (map g xs) = \f -> xs (f . g .
h)).

-- Dan
Permalink | Reply |
headers
Kim-Ee Yeoh | 26 Sep 2012 15:48
Favicon

Re: Church vs Boehm-Berarducci encoding of Lists

Both are excellent points, thank you.

Your mention of general recursion prompts the following: in 1995, ten years after publication of Boehm-Berarducci, Launchbury and Sheard investigated transformation of programs written in general recursive form into build-foldr form, with an eye towards the normalization laid out in "A Fold for All Seasons."

L&S does not cite B&B. Could they be the same algorithm?


-- Kim-Ee


On Wed, Sep 26, 2012 at 11:41 AM, <oleg <at> okmij.org> wrote:

> Wouldn't you say then that "Church encoding" is still the more appropriate
> reference given that Boehm-Berarducci's algorithm is rarely used?
>
> When I need to encode pattern matching it's goodbye Church and hello Scott.
> Aside from your projects, where else is the B-B procedure used?

First of all, the Boehm-Berarducci encoding is inefficient only when
doing an operation that is not easily representable as a fold. Quite
many problems can be efficiently tackled by a fold.

Second, I must stress the foundational advantage of the
Boehm-Berarducci encoding: plain System F. Boehm-Berarducci encoding
uses _no_ recursion: not at the term level, not at the type level.  In
contrast, the efficient for pattern-match encodings need general
recursive types. With such types, a fix-point combinator becomes
expressible, and the system, as a logic, becomes inconsistent.


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Permalink | Reply |

Gmane