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

>importMonad

>importControl.Monad.Instances

These are some of the combinators presented in Smullyan's

*To Mock a Mockingbird*. Some have direct Haskell equivalents, e.g.:

`I`

≡ `id`,

`K`

≡ `const`,

`C`

≡ `flip`,

`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 `Q`_{1}

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 ::Monadm ⇒ 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 ::Monadm ⇒ 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 =letx = f xinx

> -- 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?
## 10 comments:

w = join

s = ap

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

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). :)

@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).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?

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

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

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

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

Post a Comment