{-# LANGUAGE DeriveDataTypeable
, DeriveGeneric
, FlexibleInstances
, FlexibleContexts
, MultiParamTypeClasses #-}
import Unbound.Generics.LocallyNameless
import Unbound.Generics.LocallyNameless.Internal.Fold
import GHC.Generics (Generic)
import Data.Typeable (Typeable)
-- | Names for expressions
type Nm = Name Exp
-- | Expressions
data Exp = Var Nm -- ^ variables
| Lam (Bind Nm Exp) -- ^ lambdas bind a variable within a body expression
| App Exp Exp -- ^ application
deriving (Show, Generic, Typeable)
-- Automatically construct alpha equiv, free vars, and binding operations.
instance Alpha Exp
-- semi-automatically implement capture avoiding substitution
instance Subst Exp Exp where
-- `isvar` identifies the variable case in your AST.
isvar (Var x) = Just (SubstName x)
isvar _ = Nothing
import Unbound.Generics.LocallyNameless.Unsafe
:type unsafeUnbind
import IHaskell.Display
showExp = ppExp "λ" "."
printExp = putStrLn . showExp
dispExp e = html $ "<code>"++ppExp "λ" "." e++"</code>"
displayExp = display . dispExp
ppExp _ _ (Var x) = show x
ppExp l d (Lam bnd) = l ++ show x ++ d ++ ppExp l d t
where (x, t) = unsafeUnbind bnd
ppExp l d (App t s) = ppt t ++ " " ++ pps s
where
ppt t@(Lam{}) = paren (ppExp l d t)
ppt t = ppExp l d t
pps s@(Var{}) = ppExp l d s
pps s = paren (ppExp l d s)
paren s = "("++s++")"
:type printExp
:type dispExp
:type displayExp
-- call-by-value evaluation
-- evaluation takes an expression and returns a value while using a source of fresh names
eval (Var x) = fail $ "unbound variable " ++ show x
eval e@(Lam _) = return e
eval (App e1 e2) = do
v1 <- eval e1
v2 <- eval e2
case v1 of
(Lam bnd) -> do
-- open the lambda by picking a fresh name for the bound variable x in body
(x, body) <- unbind bnd
eval (subst x v2 body)
_ -> fail "application of non-lambda"
:type eval
x = s2n "x"
y = s2n "y"
z = s2n "z"
e = Lam $ bind x (Lam $ bind y (App (Var y) (Var x)))
lam x = Lam . bind x
:type lam
lam x (Var x)
lam y (Var y)
dispExp $ lam x (Var x)
dispExp $ lam y (Var y)
lam x (Var x) `aeq` lam y (Var y)
Lam (<x> Var 0@0)
Lam (<y> Var 0@0)
λx.x
λy.y
True
e
dispExp e
Lam (<x> Lam (<y> App (Var 0@0) (Var 1@0)))
λx.λy.y x
dispExp (App (App e e) e)
dispExp $ runFreshM $ eval (App (App e e) e)
(λx.λy.y x) (λx.λy.y x) (λx.λy.y x)
λy.y (λx.λy.y x)
tmId = lam x (Var x)
tm1 = App tmId tmId `App` App tmId tmId
tm2 = lam y $ App tmId tmId `App` App tmId tmId
dispExp tmId
dispExp $ runFreshM $ eval tmId
dispExp tm1
dispExp $ runFreshM $ eval tm1
dispExp tm2
dispExp $ runFreshM $ eval tm2
λx.x
λx.x
(λx.x) (λx.x) ((λx.x) (λx.x))
λx.x
λy.(λx.x) (λx.x) ((λx.x) (λx.x))
λy.(λx.x) (λx.x) ((λx.x) (λx.x))
:type fv
:type toListOf
fv' e = toListOf fv e :: [Nm]
:type fv'
fv' tmId
fv' (Var x)
fv' (Var x `App` Var y)
fv' (lam x . lam y $ (Var x `App` Var y) `App` Var z)
[]
[x]
[x,y]
[z]
-- reduce all the way (may diverge)
red (App e1 e2) = do
e1' <- red e1
e2' <- red e2
case e1' of
Lam bnd -> do
(x, e1'') <- unbind bnd
return $ subst x e2' e1''
_ -> return $ App e1' e2'
red (Lam bnd) = do
(x, e) <- unbind bnd
e' <- red e
case e of
App e1 (Var y) | y == x && x `notElem` fv' e1 -> return e1
_ -> return $ lam x e'
red (Var x) = return $ Var x
:type red
tm2
dispExp $ runFreshM $ eval tm2
dispExp $ runFreshM $ red tm2
Lam (<y> App (App (Lam (<x> Var 0@0)) (Lam (<x> Var 0@0))) (App (Lam (<x> Var 0@0)) (Lam (<x> Var 0@0))))
λy.(λx.x) (λx.x) ((λx.x) (λx.x))
λy.λx5.x5
import Control.Applicative
-- single step reduction
step e@(App e1 e2) = beta e
<|> (App <$> step e1 <*> pure e2)
<|> (App <$> pure e1 <*> step e2)
step (Lam bnd) = do (x, e) <- unbind bnd
lam x <$> step e
step (Var x) = empty
beta (App (Lam bnd) e2) = do (x, e1) <- unbind bnd
return $ subst x e2 e1
beta _ = empty
:type step
:type beta
omega = lam x $ Var x `App` Var x
tmOmega = App omega omega -- well known diverging term
dispExp omega
dispExp tmOmega
λx.x x
(λx.x x) (λx.x x)
:type runFreshMT . step $ tmOmega
map dispExp . runFreshMT . step $ tmOmega
(λx.x x) (λx.x x)
:type runFreshMT . step $ tm1
map dispExp . runFreshMT . step $ tm1
(λx.x) ((λx.x) (λx.x))
(λx.x) (λx.x) (λx.x)
:type runFreshMT . step $ tm2
map dispExp . runFreshMT . step $ tm2
λy.(λx.x) ((λx.x) (λx.x))
λy.(λx.x) (λx.x) (λx.x)
tm10 = (App (lam x $ Var x) (lam y $ Var y) `App` App (lam x $ Var x) (lam z $ Var z))
list1 :: [Exp]
list1 = runFreshMT . step $ tm10
list2 :: [[Exp]]
list2 = map (runFreshMT . step) list1
dispExp tm10
putStrLn "list1:"
map dispExp list1
putStrLn "list2:"
map (map dispExp) list2
(λx.x) (λy.y) ((λx.x) (λz.z))
list1:
(λy.y) ((λx.x) (λz.z))
(λx.x) (λy.y) (λz.z)
list2:
(λx.x) (λz.z)
(λy.y) (λz.z)
(λy.y) (λz.z)
import Data.Tree hiding (drawTree)
import Data.Tree.View
redTree e = Node e (map redTree . runFreshMT . step $ e)
:type showTree . fmap showExp
drawTreeExp = showTree . fmap showExp
putStrLn $ drawTreeExp $ redTree (App (lam x $ Var x) (lam y $ Var y) `App` App (lam x $ Var x) (lam z $ Var z))
(λx.x) (λy.y) ((λx.x) (λz.z)) ├╴(λy.y) ((λx.x) (λz.z)) │ ├╴(λx.x) (λz.z) │ │ └╴λz.z │ └╴(λy.y) (λz.z) │ └╴λz.z └╴(λx.x) (λy.y) (λz.z) └╴(λy.y) (λz.z) └╴λz.z