Lambda Calculus -> SKI Calculus

LambdaToSki.hs

{-# LANGUAGE DeriveFunctor, FlexibleInstances, UndecidableInstances #-}

{-
A fun exercise: read lambda calculus expressions and convert them to
pointfree form in the SKI-calculus (see http://www.madore.org/~david/programs/unlambda/#lambda_elim).
Parsing (and output via Show) are written using the conventions at
the link above:
  * Lambda-abstraction is written "^v.E" (equivalent to Haskell "\v -> E")
  * Application is written "`lr" (equivalent to "l r")
Also, note that the conversion function gives binding priority to the
innermost abstractions first, so that e.g. "^x.^x.x" is equivalent to
"^x.^y.y".

An example (computing the B combinator):

```
> ^f.^g.^x.`f`gx
=> ``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk`ki``s`kk`ki
```
-}

module LambdaToSki where

import Control.Applicative (Alternative(..))
import Control.Monad (guard)
import System.IO (hSetBuffering, stdout, BufferMode(..))

data Lam f = App f f
           | Abs Char f
           | Var Char
           deriving (Functor)

data Fix f = Fix { unFix :: f (Fix f) }

data Lam' = Lam' { unLam' :: Fix Lam }

instance Show (Lam String) where
  show e = case e of
    App l r -> '`' : l ++ r
    Abs v e' -> '^' : v : '.' : e'
    Var v -> [v]

data Ski f = S
           | K
           | I
           deriving (Functor)

instance Show (Ski f) where
  show S = "s"
  show K = "k"
  show I = "i"

data Sum f g a = InL (f a) | InR (g a)
  deriving (Show)

instance (Functor f, Functor g) => Functor (Sum f g) where
  fmap h x = case x of
               InL l -> InL (fmap h l)
               InR r -> InR (fmap h r)

data LamWithSki = LWS { unLWS :: Fix (Sum Lam Ski) }

instance Show LamWithSki where
  show (LWS (Fix (x))) = case x of
    InL lambda -> show $ fmap showLWS lambda
    InR ski -> show ski

var :: Char -> Lam'
var c =  Lam' (Fix (Var c))

app :: Lam' -> Lam' -> Lam'
app (Lam' l) (Lam' r) = Lam' (Fix (App l r))

abstr :: Char -> Lam' -> Lam'
abstr v (Lam' e) = Lam' (Fix (Abs v e))

mkLam :: f (Fix (Sum f g)) -> Fix (Sum f g)
mkLam = Fix . InL

mkSki :: g (Fix (Sum f g)) -> Fix (Sum f g)
mkSki = Fix . InR

mkApp :: Fix (Sum Lam Ski) -> Fix (Sum Lam Ski) -> Fix (Sum Lam Ski)
mkApp l r = mkLam (l `App`  r)

mkAbs :: Char -> Fix (Sum Lam Ski) -> Fix (Sum Lam Ski)
mkAbs v e = mkLam $ Abs v e

showLWS :: Fix (Sum Lam Ski) -> String
showLWS (Fix x) = case x of
  InL lambda -> case lambda of
               Var v -> [v]
               App l r -> '`' : showLWS l ++ showLWS r
               Abs v e -> '^' : v : '.' : showLWS e
  InR ski -> show ski

removeAndWrap :: Char -> Fix (Sum Lam Ski) -> Fix (Sum Lam Ski)
removeAndWrap v = unLWS . removePoint v . LWS

removePoint :: Char -> LamWithSki -> LamWithSki
removePoint v (LWS (Fix (InL l))) = LWS $ case l of
  Var v' | v == v'     -> mkSki I
         | otherwise   -> mkSki K `mkApp` mkLam l
  Abs v' e | v == v'   -> error "Bad term! (this should be impossible)"
           | otherwise -> mkSki K `mkApp` mkAbs v' (removeAndWrap v e)
  App e e'             -> (mkSki S `mkApp` removeAndWrap v e) `mkApp` removeAndWrap v e'
removePoint _ (LWS (Fix (InR s))) = LWS $ mkSki K `mkApp` mkSki s

lamToSum :: Lam' -> LamWithSki
lamToSum = LWS . foo . unLam'
  where foo :: Fix Lam -> Fix (Sum Lam Ski)
        foo (Fix x) = Fix . fmap foo . InL $ x

pointfree :: LamWithSki -> LamWithSki
pointfree (LWS (Fix (InL (Abs v e)))) = removePoint v (pointfree $ LWS e)
pointfree lws@(LWS (Fix (_))) = lws

-- Parsing

newtype Parser a = Parser { parse :: String -> Maybe (a, String) }

parse' :: Parser a -> String -> Maybe a
parse' p s = do (a, s') <- parse p s
                guard (null s')
                pure a

instance Functor Parser where
  fmap f p = Parser $ \s -> first f <$> parse p s
    where first g (x, y) = (g x, y)

instance Applicative Parser where
  pure x = Parser $ \s -> Just (x, s)
  pf <*> px = Parser $ \s -> do (f, s') <- parse pf s
                                parse (f <$> px) s'

join :: Parser (Parser a) -> Parser a
join pp = Parser $ \s -> uncurry parse =<< parse pp s

instance Monad Parser where
  x >>= f = join . fmap f $ x

instance Alternative Parser where
  empty = Parser (const Nothing)
  p <|> p' = Parser $ \s -> parse p s <|> parse p' s

char :: Char -> Parser Char
char c = Parser $ \s -> do (x:xs) <- pure s
                           guard (x == c)
                           pure (x, xs)

oneOf :: (Functor t, Foldable t) => t Char -> Parser Char
oneOf = foldr (<|>) empty . fmap char

spaces :: Parser ()
spaces = many (oneOf (" \n\t" :: String)) *> pure ()

token :: Parser a -> Parser a
token p = p <* spaces

lam :: Parser Lam'
lam = (var <$> parseVar) <|> parseAbstr <|> parseApp

parseVar :: Parser Char
parseVar = token . oneOf $ ['a'..'z'] ++ ['A'..'Z']

symbol :: Char -> Parser ()
symbol c = () <$ token (char c)

parseAbstr :: Parser Lam'
parseAbstr = do symbol '^'
                v <- parseVar
                symbol '.'
                body <- lam
                pure (abstr v body)

parseApp :: Parser Lam'
parseApp = do symbol '`'
              app <$> lam <*> lam

main :: IO ()
main = loop
  where loop = do
          hSetBuffering stdout NoBuffering
          putStr "> "
          term <- parse' lam <$> getLine
          putStrLn $ maybe "Failed to parse." (("=> " ++) . show . pointfree . lamToSum) term
          loop