src/Lambda.hs

   1 {-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
   2 {-# LANGUAGE PatternSynonyms #-}
   3
   4 -- |
   5 -- Module      :  Lambda
   6 -- Copyright   :  Tomáš Musil 2014
   7 -- License     :  BSD-3
   8 --
   9 -- Maintainer  :  tomik.musil@gmail.com
  10 -- Stability   :  experimental
  11 --
  12 -- This is a toy λ-calculus implementation.
  13
  14 module Lambda
  15   ( -- * Types
  16     VarName
  17   , Term(..)
  18     -- * Parsing terms
  19   , parseTerm
  20   , tRead
  21     -- * Reduction
  22   , reduce
  23   ) where
  24
  25
  26 import Data.Text as T
  27 import Data.Attoparsec.Text
  28 import Control.Applicative
  29 import Control.Monad.State
  30
  31 -- $setup
  32 -- >>> import Test.QuickCheck
  33 -- >>> import Control.Applicative
  34 -- >>> let aTerm 0 = pure $ Var "x"
  35 -- >>> let aTerm n = oneof [pure (Var "x"), liftA (Lambda "x") $ aTerm (n - 1), liftA2 App (aTerm (n `div` 2)) (aTerm (n `div` 2))]
  36 -- >>> instance Arbitrary Term where arbitrary = sized aTerm
  37
  38 type VarName = String
  39
  40 -- |
  41 -- >>> print $ Lambda "x" (Var "x")
  42 -- (λx.x)
  43
  44 data Term = Var VarName | Lambda VarName Term | App Term Term deriving (Eq)
  45
  46 pattern RedEx x t s = App (Lambda x t) s
  47 pattern AppApp a b c = App a (App b c)
  48 pattern EmLambda x y t = Lambda x (Lambda y t)
  49
  50
  51 instance Show Term where
  52   show (Var x) = x
  53   show (EmLambda x y t) = show (Lambda (x ++ " " ++ y) t)
  54   show (Lambda x t) = "(λ" ++ x ++ "." ++ show t ++ ")"
  55   show (AppApp a b c) = show a ++ " " ++ braced (App b c)
  56   show (App t r) = show t ++ " " ++ show r
  57
  58 braced :: Term -> String
  59 braced t = "(" ++ show t ++ ")"
  60
  61 -- |
  62 -- prop> t == tRead (show (t :: Term))
  63
  64 tRead :: String -> Term
  65 tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
  66     (Right t) -> t
  67     (Left e) -> error e
  68
  69 parseVar :: Parser Term
  70 parseVar = do
  71   x <- many1 letter
  72   return $! Var x
  73
  74 parseLambda :: Parser Term
  75 parseLambda = do
  76   char '\\' <|> char 'λ'
  77   vars <- sepBy1 parseVar (char ' ')
  78   char '.'
  79   t <- parseTerm
  80   return $! createLambda vars t
  81
  82 createLambda :: [Term] -> Term -> Term
  83 createLambda (Var x : vs) t = Lambda x $ createLambda vs t
  84 createLambda [] t = t
  85 createLambda _ _ = error "createLambda failed"
  86
  87 parseApp :: Parser Term
  88 parseApp = do
  89   aps <- sepBy1 (parseBraces <|> parseLambda <|> parseVar) (char ' ')
  90   return $! createApp aps
  91
  92 createApp :: [Term] -> Term
  93 createApp [t] = t
  94 createApp (t:ts:tss) = createApp (App t ts : tss)
  95 createApp [] = error "empty createApp"
  96
  97 parseBraces :: Parser Term
  98 parseBraces = do
  99   char '('
 100   t <- parseTerm
 101   char ')'
 102   return t
 103
 104 parseTerm :: Parser Term
 105 parseTerm = parseApp <|>
 106             parseBraces <|>
 107             parseLambda <|>
 108             parseVar
 109
 110 -------------------------------------------------
 111
 112 isFreeIn :: VarName -> Term -> Bool
 113 isFreeIn x (Var v) = x == v
 114 isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
 115 isFreeIn x (Lambda v t) = x /= v && x `isFreeIn` t
 116
 117 rename :: Term -> Term
 118 rename (Lambda x t) = Lambda n (substitute x (Var n) t)
 119   where n = rnm x
 120         rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
 121 rename _ = error "TODO vymyslet reprezentaci, kde pujde udelat fce, ktera bere jen Lambdy"
 122
 123 substitute :: VarName -> Term -> Term -> Term
 124 substitute a b (Var x) = if x == a then b else Var x
 125 substitute a b (Lambda x t)
 126   | x == a = Lambda x t
 127   | x `isFreeIn` b = substitute a b $ rename (Lambda x t)
 128   | otherwise = Lambda x (substitute a b t)
 129 substitute a b (App t u) = App (substitute a b t) (substitute a b u)
 130
 131 -- | Reduce λ-term
 132 --
 133 -- >>> reduce $ tRead "(\\x.x x) (g f)"
 134 -- g f (g f)
 135
 136 reduce :: Term -> Term
 137 reduce (Var x) = Var x
 138 reduce (Lambda x t) = Lambda x (reduce t)
 139 reduce (App t u) = app (reduce t) u
 140   where app (Lambda x v) w = reduce $ substitute x w v
 141         app a b = App a (reduce b)
 142
 143 data Strategy = Eager | Lazy
 144
 145 reduceStep :: (Monad m) => Term -> m Term
 146 reduceStep (RedEx x s t) = return $ substitute x t s
 147 reduceStep t = return $ t
 148
 149 traversPost :: (Monad m) => (Term -> m Term) -> Term -> m Term
 150 traversPost f (App t u) = do
 151   nt <- traversPost f t
 152   nu <- traversPost f u
 153   f (App nt nu)
 154 traversPost f (Lambda x t) = f . Lambda x =<< traversPost f t
 155 traversPost f (Var x) = f (Var x)
 156
 157 printT :: Term -> IO Term
 158 printT t = do
 159   print t
 160   return t
 161
 162 toNormalForm :: Strategy -> Int -> Term -> Maybe Term
 163 toNormalForm Eager n = flip evalStateT 0 . traversPost (short n >=> cnt >=> reduceStep)
 164
 165 cnt :: (Monad m) => Term -> StateT Int m Term
 166 cnt t@(RedEx _ _ _) = do
 167   modify (+ 1)
 168   return t
 169 cnt t = return t
 170
 171 short :: Int -> Term -> StateT Int Maybe Term
 172 short max t = do
 173   n <- get
 174   if n == max
 175     then lift Nothing
 176     else return t