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

[Ryan Ingram]

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