User:Jan jelo/Lambda to SKI

This is a converter in Haskell converts lambda calculus into SKI combinators.

main = do
 print $ convert $ omega
 -- ((s i) i)
 print $ convert $ turing
 -- (((s i) i) ((s (k (s i))) ((s ((s (k s)) ((s (k k)) ((s i) i)))) (k i))))
omega = Lam"x"(App(Var"x")(Var"x"))
turing = App omega (Lam"f"(Lam"x"(App(Var"x")(App(App(Var"f")(Var"f"))(Var"x")))))

data Lam
 = Var String
 | Lam String Lam
 | App Lam Lam
data Term
 = Var_ String
 | Lam_ String Term
 | App_ Term Term
 | S_ | K_ | I_
 deriving Show
data SKI
 = S | K | I
 | APP SKI SKI
instance Show SKI where
 show S = "s"
 show K = "k"
 show I = "i"
 show(APP x y) = "("++show x++" "++show y++")"
toTerm lam = case lam of
 Var x -> Var_ x
 Lam para body -> Lam_ para $ toTerm body
 App f x -> App_ (toTerm f) (toTerm x)
toSKI ski = case ski of
 S_ -> S
 K_ -> K
 I_ -> I
 App_ a b -> APP (toSKI a) (toSKI b)

isFreeIn x (Var_ y) = x==y
isFreeIn x (Lam_ para body) =
 if x==para then False
 else isFreeIn x body
isFreeIn x (App_ a b) =
 (isFreeIn x a)||(isFreeIn x b)
isFreeIn x S_ = False
isFreeIn x K_ = False
isFreeIn x I_ = False
convert = toSKI . convert_ . toTerm
convert_ S_ = S_;convert_ K_ = K_;convert_ I_ = I_
convert_ (Var_ x) = Var_ x
convert_ (App_ a b) = App_ (convert_ a) (convert_ b)
convert_ (Lam_ para body) =
 if isFreeIn para body then
  case body of
   Var_ para -> I_
   App_ a b -> App_(App_ S_ (convert_ $ Lam_ para a))(convert_ $ Lam_ para b)
   Lam_ p b -> convert_ $ Lam_ para(convert_ $ Lam_ p b)
 else App_ K_ $ convert_ body

by User:Jan jelo