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
  30 -- $setup
  31 -- >>> import Test.QuickCheck
  32 -- >>> import Control.Applicative
  33 -- >>> let aTerm 0 = pure $ Var "x"
  34 -- >>> let aTerm n = oneof [pure (Var "x"), liftA (Lambda "x") $ aTerm (n - 1), liftA2 App (aTerm (n `div` 2)) (aTerm (n `div` 2))]
  35 -- >>> instance Arbitrary Term where arbitrary = sized aTerm
  36
  37 type VarName = String
  38
  39 -- |
  40 -- >>> print $ Lambda "x" (Var "x")
  41 -- (λx.x)
  42
  43 data Term = Var VarName | Lambda VarName Term | App Term Term deriving (Eq)
  44
  45 -- pattern RedEx x t s = App (Lambda x t) s
  46 pattern AppApp a b c = App a (App b c)
  47 pattern EmLambda x y t = Lambda x (Lambda y t)
  48
  49
  50 instance Show Term where
  51   show (Var x) = x
  52   show (EmLambda x y t) = show (Lambda (x ++ " " ++ y) t)
  53   show (Lambda x t) = "(λ" ++ x ++ "." ++ show t ++ ")"
  54   show (AppApp a b c) = show a ++ " " ++ braced (App b c)
  55   show (App t r) = show t ++ " " ++ show r
  56
  57 braced :: Term -> String
  58 braced t = "(" ++ show t ++ ")"
  59
  60 -- |
  61 -- prop> t == tRead (show (t :: Term))
  62
  63 tRead :: String -> Term
  64 tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
  65     (Right t) -> t
  66     (Left e) -> error e
  67
  68 parseVar :: Parser Term
  69 parseVar = do
  70   x <- many1 letter
  71   return $! Var x
  72
  73 parseLambda :: Parser Term
  74 parseLambda = do
  75   char '\\' <|> char 'λ'
  76   vars <- sepBy1 parseVar (char ' ')
  77   char '.'
  78   t <- parseTerm
  79   return $! createLambda vars t
  80
  81 createLambda :: [Term] -> Term -> Term
  82 createLambda (Var x : vs) t = Lambda x $ createLambda vs t
  83 createLambda [] t = t
  84 createLambda _ _ = error "createLambda failed"
  85
  86 parseApp :: Parser Term
  87 parseApp = do
  88   aps <- sepBy1 (parseBraces <|> parseLambda <|> parseVar) (char ' ')
  89   return $! createApp aps
  90
  91 createApp :: [Term] -> Term
  92 createApp [t] = t
  93 createApp (t:ts:tss) = createApp (App t ts : tss)
  94 createApp [] = error "empty createApp"
  95
  96 parseBraces :: Parser Term
  97 parseBraces = do
  98   char '('
  99   t <- parseTerm
 100   char ')'
 101   return t
 102
 103 parseTerm :: Parser Term
 104 parseTerm = parseApp <|>
 105             parseBraces <|>
 106             parseLambda <|>
 107             parseVar
 108
 109 -------------------------------------------------
 110
 111 isFreeIn :: VarName -> Term -> Bool
 112 isFreeIn x (Var v) = x == v
 113 isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
 114 isFreeIn x (Lambda v t) = x /= v && x `isFreeIn` t
 115
 116 rename :: Term -> Term
 117 rename (Lambda x t) = Lambda n (substitute x (Var n) t)
 118   where n = rnm x
 119         rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
 120 rename _ = error "TODO vymyslet reprezentaci, kde pujde udelat fce, ktera bere jen Lambdy"
 121
 122 substitute :: VarName -> Term -> Term -> Term
 123 substitute a b (Var x) = if x == a then b else Var x
 124 substitute a b (Lambda x t)
 125   | x == a = Lambda x t
 126   | x `isFreeIn` b = substitute a b $ rename (Lambda x t)
 127   | otherwise = Lambda x (substitute a b t)
 128 substitute a b (App t u) = App (substitute a b t) (substitute a b u)
 129
 130 reduce :: Term -> Term
 131 reduce (Var x) = Var x
 132 reduce (Lambda x t) = Lambda x (reduce t)
 133 reduce (App t u) = app (reduce t) u
 134   where app (Lambda x v) w = reduce $ substitute x w v
 135         app a b = App a (reduce b)