Tuesday, August 12, 2008

Combinatory Birds as Types

This post is composed nearly entirely of the work of readers responding to my previous post that dealt with combinatory logic combinators. That post implemented the Smullyan combinatory birds as functions. This is the obvious approach, as birds and λ-terms have a very simple and straightforward (obviously bidirectional) mapping. A few readers improved and explained some of my combinators (S and W) by using the ((->) a) Monad, and I rolled those improvements into the original post, but these improvements are still in the combinators-as-functions domain.

Two readers, ryani and david, provided implementations for two combinators that I've had difficulty with. I've implemented the "void" combinator from the Unlambda programming language (or as Smullyan calls it, the "hopelessly egocentric" bird) using only the S and K combinators. Haskell is (thankfully) not so restricted, so ryani implemented that combinator as a type and then as a class. The thrust of ryani's void-as-type implementation is as follows:
> {-# LANGUAGE RankNTypes #-}
> newtype Void = V { runV :: forall a. a -> Void }
> v :: Void
> v = V (\x -> v)
Simple and sweet! And, the ranked type resolves the type-circularity ("void x is of type void"). So, for example:
> :t runV v 0
runV v 0 :: Void
> :t runV v "hello"
runV v "hello" :: Void
> :t runV (runV v 0) "hello"
runV (runV v 0) "hello" :: Void
... etc ...
In my implementation, I represented that the "void" combinator is "enough" K combinators (where "enough" was more K combinators than applications); ryani takes that exact approach using a class-based implementation:
> class Voidable r where vc :: r
> instance Voidable () where vc = ()
> instance Voidable r => Voidable (a -> r) where vc = k vc
(so void is represented as the Haskell type and datum () (pron: "unit")) e.g.:
> vc "hello" :: ()
()
> vc "hello" 123 :: ()
()
> vc "hello" 123 (Just k) :: ()
()
As ryani points out, the type-checker supplies the correct number of K combinators to match the number of function applications. Neat!

I had left a question on how to implement the U, or Turing, combinator, and david demonstrated an implementation where the class of all combinatory birds were a type (with two free implementations of good-ole factorial, to boot):
> data Bird a = B (Bird a -> Bird a) | Value a

> app :: Bird a -> Bird a -> Bird a
> app (B f) x = f x

> lift :: (a -> a) -> Bird a
> lift f = B (\(Value x) -> Value (f x))

> unlift :: Bird a -> (a -> a)
> unlift f = \x -> case (f `app` Value x) of Value y -> y

> -- Uxy = y(xxy)
> u = B (\x -> B (\y -> y `app` (x `app` x `app` y)))

> -- sage1 = UU [geophf mumbles: "Sweet!"]
> sage1 = u `app` u

> -- Yx = x(Yx)
> sage2 = B (\x -> x `app` (sage2 `app` x))

> fix f = unlift (sage1 `app` B (\g -> lift (f (unlift g))))
> fix2 f = unlift (sage2 `app` B (\g -> lift (f (unlift g))))

> facR :: (Integer -> Integer) -> Integer -> Integer
> facR f n = if n == 1 then 1 else n * f (n - 1)

> fac = fix facR
> fac2 = fix2 facR
I'm sure both ryani and david would claim that the M combinator (where m x = x x), so useful in Smullyan for implementing several birds (such as the "void" combinator), is not hard to do in Haskell given the above implementations. Do you see how to do it? Wanna race?

3 comments:

David said...

(Hmm. This may turn out to be a double-post, in which case apologies; but for the moment there's no sign of the comment that I thought I just left.)

First I want to make sure that credit goes to the right place. 'My' implementation really was little more than a rehash of a post here: http://www.haskell.org/pipermail/haskell/2007-April/019320.html; certainly that's where the good ideas came from.

(Actually, it does seem to be rather easy to implement M following this scheme.)

Second, I should thank you for the original post. I'd seen a few recommendations for To Mock a Mockingbird, but it was your blog that persuaded me to buy it; and I very much enjoyed the book.

admin said...

so hard to read for newbie.
make sure to visiting my blog too :)

click >> 199.188.201.30

bandarq228 said...

dapatkan uang melimpah dengan waktu singkat hanya dengan bermain permainan dominoqq di asikbandarqq
buktikan sendiri dan daftarkan diri anda sekarang juga hanya di http://180.215.13.115