Re: [Haskell-cafe] 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. LS does not cite BB. Could they be the same algorithm? -- Kim-Ee On Wed, Sep 26, 2012 at 11:41 AM, o...@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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
On Wed, Sep 26, 2012 at 12:41 AM, o...@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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
On Thu, Sep 20, 2012 at 3:15 PM,o...@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, o...@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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.8970rep=rep1type=pdf might still be relevant. Sec 2 reviews the major approaches to inductive data types in Type Theory. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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)]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
On Thu, 20 Sep 2012, o...@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)]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
On Thu, 20 Sep 2012, Jay Sulzberger wrote:
On Thu, 20 Sep 2012, o...@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)]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
On 9/18/12 4:27 AM, o...@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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
On Wed, Sep 19, 2012 at 8:36 PM, wren ng thornton w...@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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
On 18 September 2012 18:27, o...@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).
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
Ivan Lazar Miljenovic
ivan.miljeno...@gmail.com
http://IvanMiljenovic.wordpress.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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, o...@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.hshttp://community.haskell.org/~wren/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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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, o...@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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.s...@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, o...@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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.d...@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.s...@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, o...@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
On Tue, Sep 18, 2012 at 11:19 PM, Ryan Ingram ryani.s...@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.d...@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.s...@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, o...@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists
On Tue, Sep 18, 2012 at 8:39 PM, Dan Doel dan.d...@gmail.com wrote:
On Tue, Sep 18, 2012 at 11:19 PM, Ryan Ingram ryani.s...@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.d...@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.s...@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, o...@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@haskell.org
