Using the y combinator in haskell

Question

I'm a beginner in haskell, and trying to implement the Church encoding for natural numbers, as explained in this guide. I used a definition of y combinator from this answer, but not sure how to apply it.

I'd like to implement a simple function in lambda calculus which computues the sum of [1..n] as demonstrated here.

{-# LANGUAGE RankNTypes #-}

import Unsafe.Coerce

y :: (a -> a) -> a
y = \f -> (\x -> f (unsafeCoerce x x)) (\x -> f (unsafeCoerce x x))

true = (\x y -> x)
false = (\x y -> y)

newtype Chur = Chr (forall a. (a -> a) -> (a -> a))

zer :: Chur
zer = Chr (\x y -> y)

suc :: Chur -> Chur
suc (Chr cn) = Chr (\h -> cn h . h)

ci :: Chur -> Integer
ci (Chr cn) = cn (+ 1) 0

ic :: Integer -> Chur
ic 0 = zer
ic n = suc $ ic (n - 1)


-- church pair
type Chp = (Chur -> Chur -> Chur) -> Chur

pair :: Chur -> Chur -> Chp
pair (Chr x) (Chr y)  f = f (Chr x) (Chr y)

ch_fst :: Chp -> Chur
ch_fst p = p true

ch_snd :: Chp -> Chur
ch_snd p = p false

next_pair :: Chp -> Chp
next_pair = (\p x -> x (suc (p true)) (p true))

n_pair :: Chur -> Chp -> Chp
n_pair (Chr n) p = n next_pair p

p0 = pair zer zer
pre :: Chur -> Chur
pre (Chr cn) = ch_snd $ n_pair (Chr cn) p0

iszero :: Chur -> (a->a->a)
iszero (Chr cn) = cn (\h -> false) true

unchr :: Chur -> ((a -> a) -> (a -> a))
unchr (Chr cn) = cn

ch_sum (Chr cn) = (\r -> iszero (Chr cn) zer (cn suc (r (pre (Chr cn)))))

So far so good, but how do I apply y to sum? e.g.

n3 = ic 3
y ch_sum n3

causes a type mismatch:

<interactive>:168:3:
     Couldn't match type ‘(Chur -> Chur) -> Chur’ with ‘Chur’
     Expected type: ((Chur -> Chur) -> Chur) -> (Chur -> Chur) -> Chur
     Actual type: Chur -> (Chur -> Chur) -> Chur
     In the first argument of ‘y’, namely ‘ch_sum’
     In the expression: y ch_sum n3

<interactive>:168:10:
   Couldn't match expected type ‘Chur -> Chur’ with actual type ‘Chur’
   In the second argument of ‘y’, namely ‘n3’
   In the expression: y ch_sum n3

Y Combinator in Haskell provides the definition of y combinator, but doesn't explain how to use it.

@chepner Why is that a duplicate? This question (which I linked to), provides the definition of y combinator, but doesn't explain how to use it. — dimid
– dimid, Commented Apr 24, 2016 at 18:16
@dimid See this answer to the proposed duplicate. You can't type the Y combinator. — chepner
– chepner, Commented Apr 24, 2016 at 18:27
@chepner So, then obviously this won't typecheck and work? :) — Anton Trunov
– Anton Trunov, Commented Apr 24, 2016 at 18:31
@chepner Yeah, I know you need to use certain tricks, such as unsafeCoerce, but that's not the issue. The issue is that question provides the definition of y combinator, but doesn't explain how to use it, which is why i"ve asked this question. — dimid
– dimid, Commented Apr 24, 2016 at 18:42

Anton Trunov · Accepted Answer · 2016-04-24 18:19:55Z

3

I've introduced the function add (which obviously adds two Church numerals) to simplify the ch_sum's definition:

add :: Chur -> Chur -> Chur
add (Chr cn1) (Chr cn2) = Chr (\h -> cn1 h . cn2 h)

To create a recursive function using a fixed-point combinator, you need to write it as it was an ordinary recursive function (in a language with recursion), but as a last step add the explicit "self" argument as the first function's argument (r in this case) and instead of a recursive call you just call "self" (r). So ch_sum can be written as

ch_sum :: (Chur -> Chur) -> Chur -> Chur
ch_sum = \r n -> iszero n zer $ add n (r $ pre n)

A couple tests in ghci:

λ> let n3 = ic 3
λ> ci (y ch_sum n3)
6
λ> let n10 = ic 10
λ> ci (y ch_sum n10)
55

answered Apr 24, 2016 at 18:19

Anton Trunov

15.5k2 gold badges30 silver badges50 bronze badges

Sign up to request clarification or add additional context in comments.

5 Comments

dimid Over a year ago

Thanks, I think it's a bit clearer (at least for me) to define addition using the successor: ch_add (Chr cn1) (Chr cn2) = cn1 suc (Chr cn2)

Anton Trunov Over a year ago

Yes, you're right. That would be a cleaner approach (from several points of view): once we defined zer and suc (and maybe some other "primitives", like Church pairs, ...) we shouldn't use anything except those for building other arithmetic functions. By the way, add (Chr cn1) arg2 = cn1 suc arg2 is another way to write the addition function (not in principal, it just avoids unfolding/folding of the second argument).

Anton Trunov Over a year ago

Also, it's possible to implement Church numerals without the RankNTypes extension, but then you will have to use an implementation akin to the version in my answer, because otherwise it won't typecheck.

dimid Over a year ago

Interesting, do you mean an implementation like this? stackoverflow.com/a/6464164/165753

Anton Trunov Over a year ago

Yes, but higher-order ranks give you much more in expressiveness.

Collectives™ on Stack Overflow

Using the y combinator in haskell

1 Answer 1

5 Comments

Your Answer

Linked

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

5 Comments

Your Answer

Sign up or log in

Post as a guest

Linked

Related