Saturday, August 2, 2008

Combinators in Haskell

In this article, instead of continuing along my path of shoving Prolog (predicate logic) into Haskell, I'll take a break from that and shove Haskell into Haskell. This turn comes by way of my recent professional experience working with Prolog — I found myself oftentimes needing to write some purely functional code, but I found the Prolog semantics getting in my way, so, borrowing some of the ideas from my previous professional programming experiences with Mercury and Dylan (when Harlequin was still a going concern, and had picked up the Dylan ball that Apple, then CMU, dropped, making a really sweet Dylan programming environment), I implemented a set of libraries for Prolog, including basic ZF-set operations, propositional logic syntax, list/set/bag utilities, and the combinator logic of Schönfinkel.
"geophf!" You exclaim, horrified, "you don't really use combinators to write working production code, do you?"

Well, yes, and I also proposed a new one in addition to the ones covered by Smullyan in To Mock a Mockingbird, and have studied the make-up of the "void" combinator of Unlambda, so I'm one of those kinds of programmers.

In short, when I was working with Prolog, I shoe-horned a Haskell interpreter into to be able to write map and fold when I wished to write map and fold. Since Prolog has DCGs (Definite Clause Grammars), I lived a monad-free and worry-free life. Ah, yes, those were the days.

That was quite a trip down memory lane. Looking back, I marvel at my fortune, not only have I professionally programmed in those languages (and VisualWorks Smalltalk; that was fun when I presented the boss a solution in two weeks that he was expecting in two months — he was so impressed that he bought the VisualWorks system for the contract, made me mentor a junior programmer on Smalltalk (Chris Choe, a good guy to work with), and had me teach a brown bag course at work on Smalltalk, but I digress, again), but it looks like Haskell is now part of our solution at my current place of work.

Life is good.

Of course, it would be so much better if I had access to the primitive combinators in Haskell (did Miranda allow that kind of low-level access, I wonder). I mean, why should one write out 'const', a whole FIVE characters, when one simply wishes to use the K combinator. I felt that very pain all too recently. I had that freedom using my combinator library when I was working on Prolog ... goodness, even MITRE fabricated the Curry Chip.

So, I could not put it off any longer, I pulled out my dog-eared copy of Mockingbird and wrote the CL module, as I didn't see one in the Haskell standard library. It went surprisingly quickly and easily. There were a few snags, Prolog, being dynamically-typed, allowed me to define the reoccuring combinators of L, M, and U (definitions of the combinators are available in my combinator library or tabled form or as graphical notation (which includes a very nice write up of propositional logic in CL)), but Haskell's type system complains of an occur-check error. I have the hack to define the Y combinator ...
fix f = let x = f x in x

... but I'm having difficulty hacking the other self-applying combinators; any suggestions on how to implement those? I'm particularly interested in implementing Turings' universal combinator ...
Uxy = y(xxy)

... because of its interesting properties I'd like to explore.

Anyway, here's the ones I do have.

> module Smullyan where

It was pointed out to me in the comments that if you make the ((->) a) type a Monad, then some of the combinators simplify to monadic operators.

> import Monad
> import Control.Monad.Instances

These are some of the combinators presented in Smullyan's To Mock a Mockingbird. Some have direct Haskell equivalents, e.g.: Iid, Kconst, Cflip, B(.), but then that just makes my job easier here. I also admit a preference to the Schönfinkel combinators over the renamed Haskell equivalents, so here is the library.

We will not be defining combinators here that cause an occurs-check of the type system, e.g. L, M, U, but we can define some interesting ones, such as O and Y by using work-arounds.

If we wish to start with λI, then its basis is formed from the J and I combinators.
> -- identity (I have no idea to which species belongs the 'identity' bird)
> i :: a -> a
> i = id

> -- jay: jabcd = ab(adc)
> j :: (a -> b -> b) -> a -> b -> a -> b
> j a b c d = a b (a d c)

I actually spent quite a stretch of time building the other combinators from the JI-basis, e.g., the T combinator is JII, the Q1 combinator is JI, etc. When I attempted to define the K combinator, I ran into a brick wall for some time, until I reread the section in Mockingbird about how the noble basis has no way to define that abhorred combinator. Since that time I've fallen from grace and have used λK, but I've always wondered since if a complete logic could be reasonably expressed in λI, and if so, how would that logic be implemented? I haven't come across any papers that address these questions.

Musing again, let's define the basis of λK which is founded on the S and K combinators.
> -- starling: sfgx = fx(gx)
> s :: Monad m ⇒ m (a → b) → m a → m b
> s = ap

> -- kestrel: kab = a
> k :: a -> b -> a
> k = const

... okay, that wasn't too hard, so, SKK should be I, right?

--- :t (s k k) :: a -> a ... oh, yeah!

let's continue with some of the other combinators:
> -- bluebird: bfgx = f(gx)
> b :: (b -> c) -> (a -> b) -> a -> c
> b = (.)

> -- cardinal: cfgx = gfx
> c :: (a -> b -> c) -> b -> a -> c
> c = flip

Now we start defining combinators in terms of simpler combinators. Although, we could have started doing that once we've defined S and K, as all other combinators can be derived from those two.
> -- dove: dfghx = fg(hx)
> d :: (d -> b -> c) -> d -> (a -> b) -> a -> c
> d = b b

> -- thrush: txf = fx
> t :: a -> (a -> b) -> b
> t = c i

> -- vireo (pairing/list): vabf = fab
> -- e.g. v 1 [2] (:) -> [1,2]
> v :: a -> b -> (a -> b -> b) -> b
> v = b c t

> -- robin: rxfy = fyx
> r :: a -> (b -> a -> c) -> b -> c
> r = b b t

> -- owl: ofg = g(fg)
> o :: ((a -> b) -> a) -> (a -> b) -> b
> o = s i

> -- queer: qfgx = g(fx)
> q :: (a -> b) -> (b -> c) -> a -> c
> q = c b

-- mockingbird: mf = ff
m = s i i

... ah, well, it was worth a try ...
> -- warbler: wfx = fxx
> w :: Monad m ⇒ m (m a) → m a
> w = join

> -- eagle: eabcde = ab(cde)
> e :: (a -> b -> c) -> a -> (d -> e -> b) -> d -> e -> c
> e = b (b b b)

With the above definitions, we can now type-check that my JI-basis is correct: the type of I already checks, and the type of J should be equivalent to B(BC)(W(BCE))), ...
:t (b (b c) (w (b c e)))
(b (b c) (w (b c e))) :: (d -> e -> e) -> d -> e -> d -> e

and it is ... yay!

-- lark (ascending): lfg = f(gg)
l = ((s ((s (k s)) k)) (k (s i i)))

l :: (a -> b) -> (c -> a) -> b
a b = a (b b)

... ah, well, another one bites the dust ...

but we can define Y, albeit with a let-trick, thanks to Dirk Thierbach, responding to the thread "State Monad Style" on comp.lang.haskell:
> fix :: (a -> a) -> a
> fix f = let x = f x in x

> -- sage/why: yf = f(yf)
> y :: (a -> a) -> a
> y = fix

So, there you go, 15 combinators to get you started; now you can program a functionally pure and mathematically sound version of Unlambda (which exists and is called Lazy-K, by the way) using your very own Haskell system.

After all, why should someone ever be forced to write \x -> x^2 when they have the option, and privilege, to write w (*) instead?

11 comments:

Daniel Wagner said...

w = join

Unknown said...

s = ap

geophf said...

@dmwit and matti, thank you! But I'm afraid I'm a bear with very little brain, and I don't see the equivalence:

:t w is (a -> a -> b) -> a -> b
:t join is (Monad m) => m (m a) -> m a

join [[1,2,3],[4,5]] is [1,2,3,4,5]
w [[1,2,3],[4,5]] is error

:t s is (a -> b -> c) -> (a -> b) -> a -> c
:t ap is (Monad m) => m (a -> b) -> m a -> m b

Would you both be so kind as to prove the equivalence that you propose?

Dan Doel said...

One example of a monad is (->) e, or if you like sections, (e ->). This means that:

join :: (e -> (e -> a)) -> e -> a

when specialized to that monad. Similarly:

ap :: (e -> (a -> b)) -> (e -> a) -> (e -> b)

From the types alone, one should expect the connection (similarly, return = const, fmap = (.)). The combinators are special cases of these monadic functions.

Also, no one who writes haskell has to write \x -> x^2. They can instead write (^2). :)

geophf said...

@dan doel, thanks for the explanation, clarifying the monadic definitions. I'll reformulate the module and repost.

Of course, I hope you read that I was being factious when I offered `w (*)`. ... I feel that sometimes conversations about CL get too serious too quickly, and a little light-hearted humour (or, in the case of Smullyan's Mockingbird, a great deal of light-hearted humour) goes a long way in enjoying combinators for what they are and what they aren't (what they are: fun and useful to play with; what they aren't: a panacea).

Unknown said...

Of course, lots of the birds from Mockingbird aren't typeable even in full System F + letrec; consider, as you mention, the void operator in unlambda:

v x = v

What is its type? Well, it's polymorphic in its argument, so you can start with forall t. t -> ?. But what is the inside type? It's the same as the rest, so you get "forall t0. t0 -> forall t1. t1 -> forall t2. t2 -> ..."

Now, the type system secretly does have fixed points, but you have to explicitly tell it you want it with wrapping and unwrapping methods. Try this on for size:

{-# LANGUAGE RankNTypes #-}
newtype Void = V { runV :: forall a. a -> Void }
v :: Void
v = V (\x -> v)

ghci> :t runV (runV v 0) "hello"
runV (runV v 0) "hello" :: Void

You can also use typeclasses to get somewhere with this, as well:

k = const
class Voidable r where vc :: r
instance Voidable () where vc = ()
instance Voidable r => Voidable (a -> r) where vc = k vc

ghci> vc "hello" 1300 "world" :: ()
()

This is akin to the "V as a large number of Ks" approach, except that the typechecker figures out how many Ks you need.

I thought about it for a bit and couldn't come up with a useful type for M or U, though. Perhaps with this to start out with, you can figure out something?

David said...

See this thread: http://www.haskell.org/pipermail/haskell/2007-April/019320.html

Here's a slight reformulation which I find more aesthetic:

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
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

Anonymous said...

Also, here's something fun/crazy I tried...

module B where
import Unsafe.Coerce (unsafeCoerce)

k = const
s x y z = x z $ y z
i = id -- could be "s k k"
c = (.)

-- here is the craziness
-- this is not the real type
-- for m, but it makes things
-- typecheck and work, somehow!
m :: (a -> b) -> b
m = s i (unsafeCoerce i)

-- sage
-- y = \f. m (\x. f (m x))
y f = m (c f m)

-- crazy!
fact = y (\f x y -> if y == 0 then x else f (x*y) (y-1)) 1

Unknown said...

I wonder what Haskell's "on" combinator corresponds to?

Snowball said...

@Chris Wong,

Haskell defines 'on' as

(*) `on` f = \x y -> f x * f y

Dropping the infix and lambda notation and renaming variables (let on = N), that becomes

Nabcd = a(bc)(bd)

In terms of the S and K basis combinators, one way to write this is

N = S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KS)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KS)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KK)))))(S(S(KS)(S(KK)(KK)))(S(KK)(SKK)))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KS)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KK)))))(S(S(KS)(S(KK)(KK)))(S(S(KS)(KK))(KK)))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))(S(KK)(KK)))))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KS)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KK)))))(S(S(KS)(S(KK)(KK)))(S(S(KS)(KK))(KK)))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))(S(KK)(KS)))))(S(S(KS)(S(KK)(KK)))(S(KK)(KK))))))(S(S(KS)(S(KK)(KK)))(S(KK)(KK)))))

Fun stuff!

gabedamien said...

Small note: in your description of the cardinal, you wrote `cfgx = gfx`, but I believe you mean `cfgx = fxg`.