SKI transform, how to program in a functional language

Question

I am facing the following Prolog code. The expression [X]>>Y stands for the lambda expression lambda X.Y. The code eliminates the lambda and gives a combinatory expression over S, K and I:

convert([X]>>Y,'I') :- X==Y, !.
convert([X]>>Y,apply('K',Y)) :- var(Y), !.
convert([X]>>([Y]>>Z),R) :-
     convert([Y]>>Z,H), convert([X]>>H,R).
convert([X]>>apply(Y,Z),apply(apply('S',S),T)) :-
     convert([X]>>Y,S), convert([X]>>Z,T).
convert([_]>>Y,apply('K',Y)).

Here is an example how it works:

 ?- convert([X]>>([Y]>>apply(Y,X)),R).
 R = apply(apply('S', apply(apply('S', apply('K', 'S')), 
  apply('K', 'I'))), apply(apply('S', apply('K', 'K')), 'I'))

Suppose I would like to code the same conversion in Haskell, ML, or the like. How can I do this? Can I use the lambda expressions available in the functional programming language directly? Or do I have to regress to some meta programming facilities?

Best Regards

P.S.: The code above is not the SKI conversion that leads to very short SKI expressions. Better code is possible that checks for occurence of the bound variable in the lambda expression body.

Answer 1

Your prolog code can be translated almost verbatim into a pattern matching of ML or Haskell. Of course you'd need to define your own ADT for lambda expressions. And for the most optimal set of combinators and conversion for that set I'd recommend to refer to http://www.amazon.com/Functional-Programming-International-Computer-Science/dp/0201192497

Answer 2

You can directly use lamdba expressions. In Haskell:

i x = x
k x = \y -> x
s x y z = x z $ y z

r = s (s (k s) (k i)) (s (k k) i)

-- r 3 (+5) -> 8

(note that I didn't know of SKI up to know, this snippet is a direct conversion of the definitions on Wikipedia into Haskell; it works, but do check if it's conceptually right)