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?