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

[Dan Doel]

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