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

[Ryan Ingram]

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