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 BoehmBerarducci encoding. That is, often seen > newtype ChurchList a = > CL { cataCL :: forall r. (a > r > r) > r > r } (in http://community.haskell.org/%7Ewren/listextras/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/taglessfinal/course/BoehmBerarducci.html BoehmBerarducci encoding is very insightful and influential. The authors truly deserve credit. P.S. It is actually possible to write zip function using BoehmBerarducci encoding: http://okmij.org/ftp/ftp/Algorithms.html#zipfolds _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
On 18 September 2012 18:27, <[hidden email]> 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 BoehmBerarducci encoding. That is, often seen > >> newtype ChurchList a = >> CL { cataCL :: forall r. (a > r > r) > r > r } > > (in http://community.haskell.org/%7Ewren/listextras/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/taglessfinal/course/BoehmBerarducci.html > > BoehmBerarducci encoding is very insightful and influential. The > authors truly deserve credit. > > P.S. It is actually possible to write zip function using BoehmBerarducci > encoding: > http://okmij.org/ftp/ftp/Algorithms.html#zipfolds You have one too many "ftp/" in there (in case others get confused about why the link fails). > > > > > _______________________________________________ > HaskellCafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskellcafe  Ivan Lazar Miljenovic [hidden email] http://IvanMiljenovic.wordpress.com _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
Administrator

In reply to this post by oleg30
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 patternmatching to match with construction. Boehm and Berarducci did. So properly speaking, tail and pred for Churchencoded lists and nats are trialanderror affairs. But the point is they need not be if we use BB 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.  KimEe
On Tue, Sep 18, 2012 at 3:27 PM, <[hidden email]> wrote:
_______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by oleg30
Oleg, do you have any references for the extension of lambdaencoding 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 lambdaencoding of 'nat' in the untyped lambdacalculus 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, <[hidden email]> wrote:
_______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
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 Churchlike encoding of natural numbers can be derived. I've done some work here: http://code.haskell.org/~dolio/agdashare/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 <[hidden email]> wrote: > Oleg, do you have any references for the extension of lambdaencoding 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 lambdaencoding of 'nat' in the untyped lambdacalculus 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, <[hidden email]> 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 BoehmBerarducci encoding. That is, often seen >> >> > newtype ChurchList a = >> > CL { cataCL :: forall r. (a > r > r) > r > r } >> >> (in http://community.haskell.org/%7Ewren/listextras/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/taglessfinal/course/BoehmBerarducci.html >> >> BoehmBerarducci encoding is very insightful and influential. The >> authors truly deserve credit. >> >> P.S. It is actually possible to write zip function using BoehmBerarducci >> encoding: >> http://okmij.org/ftp/ftp/Algorithms.html#zipfolds >> >> >> >> >> _______________________________________________ >> HaskellCafe mailing list >> [hidden email] >> http://www.haskell.org/mailman/listinfo/haskellcafe > > > > _______________________________________________ > HaskellCafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskellcafe > _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
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 xinduction {A} {B} {P} f p = p (P p) f On Tue, Sep 18, 2012 at 4:09 PM, Dan Doel <[hidden email]> wrote: This paper: _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
On Tue, Sep 18, 2012 at 11:19 PM, Ryan Ingram <[hidden email]> 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 > > xinduction {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 straightforward 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 <[hidden email]> 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 >> Churchlike encoding of natural numbers can be derived. I've done some >> work here: >> >> http://code.haskell.org/~dolio/agdashare/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 <[hidden email]> wrote: >> > Oleg, do you have any references for the extension of lambdaencoding 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 lambdaencoding of 'nat' in the untyped lambdacalculus 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, <[hidden email]> 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 BoehmBerarducci encoding. That is, often seen >> >> >> >> > newtype ChurchList a = >> >> > CL { cataCL :: forall r. (a > r > r) > r > r } >> >> >> >> (in >> >> http://community.haskell.org/%7Ewren/listextras/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/taglessfinal/course/BoehmBerarducci.html >> >> >> >> BoehmBerarducci encoding is very insightful and influential. The >> >> authors truly deserve credit. >> >> >> >> P.S. It is actually possible to write zip function using >> >> BoehmBerarducci >> >> encoding: >> >> http://okmij.org/ftp/ftp/Algorithms.html#zipfolds >> >> >> >> >> >> >> >> >> >> _______________________________________________ >> >> HaskellCafe mailing list >> >> [hidden email] >> >> http://www.haskell.org/mailman/listinfo/haskellcafe >> > >> > >> > >> > _______________________________________________ >> > HaskellCafe mailing list >> > [hidden email] >> > http://www.haskell.org/mailman/listinfo/haskellcafe >> > > > _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
On Tue, Sep 18, 2012 at 8:39 PM, Dan Doel <[hidden email]> wrote:
The line of logic I was thinking is that you could lift the parametricity proof to the (proofirrelevant) 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 xlemma1 to rewrite the rhs of xinduction? ×lemma₁ : ∀{A B R} → (p : A × B) (k : A → B → R) → k (fst p) (snd p) ≡ p R k xlemma1 {A} {B} {P p} p f :: f (fst p) (snd p) = p (P p) f Or is the problem that the "k" parameter to xlemma1 isn't 'dependently typed' enough?  ryan
_______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by oleg30
On 9/18/12 4:27 AM, [hidden email] 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 BoehmBerarducci encoding. That is, often seen > >> newtype ChurchList a = >> CL { cataCL :: forall r. (a > r > r) > r > r } > > (in http://community.haskell.org/%7Ewren/listextras/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 listextras 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 BoehmBerarducci > encoding: > http://okmij.org/ftp/ftp/Algorithms.html#zipfolds Of course it is; I just never got around to doing it :)  Live well, ~wren _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
On Wed, Sep 19, 2012 at 8:36 PM, wren ng thornton <[hidden email]> wrote:
>> P.S. It is actually possible to write zip function using BoehmBerarducci >> encoding: >> http://okmij.org/ftp/ftp/Algorithms.html#zipfolds > > > 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 _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by oleg30
Dan Doel wrote: > >> P.S. It is actually possible to write zip function using BoehmBerarducci > >> encoding: > >> http://okmij.org/ftp/Algorithms.html#zipfolds > > 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 BoehmBerarducci 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 Pnumerals http://okmij.org/ftp/Computation/lambdacalc.html#pnumerals It turns out, I have rediscovered them after Michel Parigot (so my name Pnumerals 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 constanttime cons, head, tail and trivially expressible fold and zip. KimEe Yeoh wrote: > So properly speaking, tail and pred for Churchencoded lists and nats > are trialanderror affairs. But the point is they need not be if we > use BB 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)] _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
On Thu, 20 Sep 2012, [hidden email] wrote: > > Dan Doel wrote: >>>> P.S. It is actually possible to write zip function using BoehmBerarducci >>>> encoding: >>>> http://okmij.org/ftp/Algorithms.html#zipfolds >> >> 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 BoehmBerarducci 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 Pnumerals > http://okmij.org/ftp/Computation/lambdacalc.html#pnumerals > It turns out, I have rediscovered them after Michel Parigot (so my > name Pnumerals 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? ooJS. > > 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 constanttime cons, head, tail and trivially > expressible fold and zip. > > > KimEe Yeoh wrote: >> So properly speaking, tail and pred for Churchencoded lists and nats >> are trialanderror affairs. But the point is they need not be if we >> use BB 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)] > _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
On Thu, 20 Sep 2012, Jay Sulzberger wrote: > > > On Thu, 20 Sep 2012, [hidden email] wrote: > >> >> Dan Doel wrote: >>>>> P.S. It is actually possible to write zip function using >>>>> BoehmBerarducci >>>>> encoding: >>>>> http://okmij.org/ftp/Algorithms.html#zipfolds >>> >>> 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 BoehmBerarducci 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 Pnumerals >> http://okmij.org/ftp/Computation/lambdacalc.html#pnumerals >> It turns out, I have rediscovered them after Michel Parigot (so my >> name Pnumerals 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? > > ooJS. Ah, I have just read the forany vs forall part of http://okmij.org/ftp/Computation/lambdacalc.html#pnumerals and I think I understand something. ooJS. > > >> >> 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 constanttime cons, head, tail and trivially >> expressible fold and zip. >> >> >> KimEe Yeoh wrote: >>> So properly speaking, tail and pred for Churchencoded lists and nats >>> are trialanderror affairs. But the point is they need not be if we >>> use BB 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)] >> > > _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
In reply to this post by Ryan Ingram
> do you have any references for the extension of lambdaencoding 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: Wellordering 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. _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
Administrator

In reply to this post by oleg30
On Thu, Sep 20, 2012 at 3:15 PM,<[hidden email]> 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 BoehmBerarducci'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 BB procedure used?  KimEe On Thu, Sep 20, 2012 at 3:15 PM, <[hidden email]> wrote:
_______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
> Wouldn't you say then that "Church encoding" is still the more appropriate > reference given that BoehmBerarducci'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 BB procedure used? First of all, the BoehmBerarducci 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 BoehmBerarducci encoding: plain System F. BoehmBerarducci encoding uses _no_ recursion: not at the term level, not at the type level. In contrast, the efficient for patternmatch encodings need general recursive types. With such types, a fixpoint combinator becomes expressible, and the system, as a logic, becomes inconsistent. _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
On Wed, Sep 26, 2012 at 12:41 AM, <[hidden email]> wrote:
> First of all, the BoehmBerarducci 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 BoehmBerarducci encoding gets you that and more (map g xs f = xs (f . g) ; map h (map g xs) = \f > xs (f . g . h)).  Dan _______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
Administrator

In reply to this post by oleg30
Both are excellent points, thank you. Your mention of general recursion prompts the following: in 1995, ten years after publication of BoehmBerarducci, Launchbury and Sheard investigated transformation of programs written in general recursive form into buildfoldr 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?  KimEe On Wed, Sep 26, 2012 at 11:41 AM, <[hidden email]> wrote:
_______________________________________________ HaskellCafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskellcafe 
Free forum by Nabble  Edit this page 