Source

simple-lambda / Data / Lambda / Simple.hs

Full commit
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}
import Control.Applicative

import Control.Monad.Trans.State
import Control.Monad.Trans.Reader
import Control.Monad.Trans.Class

import qualified Data.Map as Map
import           Data.Map   (Map)
import Text.Printf
-- import Text.PrettyPrint.HughesPJ

import Data.Data     (Data)
import Data.Typeable (Typeable)
import Data.String
import Data.Generics.Uniplate.Data
import Debug.Trace
import System.IO

----------------------------------------------------------------
-- Data types for lambda calculus
----------------------------------------------------------------

-- | Variable name with optional tag
data Var = Free String 
         | Bound Int
         deriving (Eq,Ord,Typeable,Data,Show)



-- | Simple lambda calculus
data Term v = Variable v
            | Lam      v        (Term v)
            | Apply    (Term v) (Term v)
            deriving (Typeable,Data,Show)



----------------------------------------------------------------
-- Pretty printing
----------------------------------------------------------------

-- | Dictionary with symbol 
data PrettyLambda = PrettyLambda { lambdaChar  :: Char   -- ^ Character for lambda symbol
                                 , lambdaArrow :: String
                                 }
                    
-- | Lambda expression with haskell syntax
prettyHaskell :: PrettyLambda 
prettyHaskell = PrettyLambda '\\' " -> "

-- | Lambda expression with unicode syntax
prettyUnicode :: PrettyLambda
prettyUnicode = PrettyLambda 'λ' " → "



-- | Pretty print lambda expression
pretty :: ShowVar v => PrettyLambda -> Term v -> String
pretty _ (Variable v) = showVar v
pretty d (Apply  a b) = printf "(%s %s)" (pretty d a) (pretty d b)
pretty d t@(Lam  _ _) = '(' : lambdaChar d : lamWorker d "" t ++ ")"

-- Special case currying
lamWorker d pre (Lam v t) = pre ++ showVar v ++ lamWorker d " " t
lamWorker d _    t        = lambdaArrow d ++ pretty d t

-- | Pretty printing wrapper
newtype P v = P (Term v)

instance ShowVar v => Show (P v) where 
  show (P t) = pretty prettyHaskell t

-- | Unicode pretty printing wrapper
newtype U v = U (Term v)

instance ShowVar v => Show (U v) where
  show (U t) = pretty prettyUnicode t


-- | Pretty printing for variables
class ShowVar v where
  showVar :: v -> String

instance ShowVar [Char] where
  showVar = id

instance ShowVar Var where
  showVar (Free  s) = s
  showVar (Bound n) = printf "x{%i}" n


  
----------------------------------------------------------------
-- Construction
----------------------------------------------------------------

-- | Lambda abstraction
lam :: String -> Term String -> Term String
lam v t = Lam v t

-- | Apply 
(#) :: Term v -> Term v -> Term v
(#) = Apply

-- Convenience
instance IsString Var where
  fromString = Free
instance IsString v => IsString (Term v) where
  fromString = Variable . fromString



----------------------------------------------------------------
-- Transformation
----------------------------------------------------------------

type Bounder = ReaderT (Map String Var) (State Int)

-- Get fresh variable
freshVar :: Bounder Var
freshVar = do
  n <- lift get
  lift $ put (n+1)
  return $ Bound n

-- Rename variable
rename :: String -> Bounder Var
rename s = do
  m <- ask
  case Map.lookup s m of
    Just v  -> return v
    Nothing -> return (Free s)
    
-- Bind all variables
bindVarsM :: Term String -> Bounder (Term Var)
bindVarsM (Variable v)  = Variable <$> rename v
bindVarsM (Apply t1 t2) = Apply <$> bindVarsM t1 <*> bindVarsM t2
bindVarsM (Lam nm t) = do
  var <- freshVar
  withReaderT (Map.insert nm var) $ 
    Lam var <$> bindVarsM t

-- | Bind all variables and ensure no bound variables share same name
bindVars :: Term String -> Term Var
bindVars t = flip evalState 0 
           $ flip runReaderT Map.empty  
           $ bindVarsM t

-- | Substitute variable with term
substitute :: (ShowVar v, Eq v) => v -> Term v -> Term v -> Term v
substitute v t (Variable v') | v == v'   = t
                             | otherwise = Variable v'
substitute v t (Lam nm term) = 
  -- traceShow ("lambda", Lam nm term) $
  Lam nm (substitute v t term)
substitute v t (Apply t1 t2) = 
  -- traceShow ("apply", Apply t1 t2) $
  Apply (substitute v t t1) (substitute v t t2)


-- | Simplify lambda expression
simplify :: Term Var -> Term Var
-- Substitution rule
simplify (Apply (Lam v t) t') = simplify $ substitute v t' t
-- Walk down the tree
simplify (Lam v t)     = Lam v (simplify t)
simplify (Apply t1 t2) = case Apply (simplify t1) (simplify t2) of
                           Apply (Lam v t) t' -> simplify $ substitute v t' t
                           t -> t
simplify v             = v


rule :: Term Var -> Term Var
rule (Apply (Lam v t) t') = substitute v t' t
rule t = t

names :: String -> [String]
names ch = [ a:b | b <- [] : names ch 
                 , a <- ch
                 ]


nice :: Term Var -> Term String
nice = worker (names ['a'..'z']) (Map.empty) 
  where
    worker _ m (Variable v)  = Variable $ m Map.! v
    worker s m (Apply t1 t2) = Apply (worker s m t1) (worker s m t2)
    worker (nm:s) m (Lam v t) = 
      Lam nm $ worker s (Map.insert v nm m) t


ap :: Term String
ap = lam "x" (lam "y" ("x" # "y"))

boob :: Term String
boob = lam "f" (lam "g" (lam "x" ("f" # ("g" # "x"))))

b = bindVars boob
q = bindVars (boob # ap)