{ "cells": [ { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [ { "data": { "text/html": [ "
\"++ppExp \"λ\" \".\" e++\"
\"\n",
"displayExp = display . dispExp\n",
"\n",
"ppExp _ _ (Var x) = show x\n",
"ppExp l d (Lam bnd) = l ++ show x ++ d ++ ppExp l d t\n",
" where (x, t) = unsafeUnbind bnd\n",
"ppExp l d (App t s) = ppt t ++ \" \" ++ pps s\n",
" where\n",
" ppt t@(Lam{}) = paren (ppExp l d t)\n",
" ppt t = ppExp l d t\n",
" pps s@(Var{}) = ppExp l d s\n",
" pps s = paren (ppExp l d s)\n",
"\n",
"paren s = \"(\"++s++\")\""
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"printExp :: Exp -> IO ()"
],
"text/plain": [
"printExp :: Exp -> IO ()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"dispExp :: Exp -> DisplayData"
],
"text/plain": [
"dispExp :: Exp -> DisplayData"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"displayExp :: Exp -> IO Display"
],
"text/plain": [
"displayExp :: Exp -> IO Display"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
":type printExp\n",
":type dispExp\n",
":type displayExp"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"eval :: forall (m :: * -> *). Fresh m => Exp -> m Exp"
],
"text/plain": [
"eval :: forall (m :: * -> *). Fresh m => Exp -> m Exp"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"-- call-by-value evaluation\n",
"-- evaluation takes an expression and returns a value while using a source of fresh names\n",
"eval (Var x) = fail $ \"unbound variable \" ++ show x\n",
"eval e@(Lam _) = return e\n",
"eval (App e1 e2) = do\n",
" v1 <- eval e1\n",
" v2 <- eval e2\n",
" case v1 of\n",
" (Lam bnd) -> do\n",
" -- open the lambda by picking a fresh name for the bound variable x in body\n",
" (x, body) <- unbind bnd\n",
" eval (subst x v2 body)\n",
" _ -> fail \"application of non-lambda\"\n",
" \n",
":type eval"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [],
"source": [
"x = s2n \"x\"\n",
"y = s2n \"y\"\n",
"z = s2n \"z\"\n",
"e = Lam $ bind x (Lam $ bind y (App (Var y) (Var x)))"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"lam :: Nm -> Exp -> Exp"
],
"text/plain": [
"lam :: Nm -> Exp -> Exp"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"lam x = Lam . bind x\n",
":type lam"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Lam (λx.x
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"λy.y
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
"True"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"lam x (Var x)\n",
"lam y (Var y)\n",
"\n",
"dispExp $ lam x (Var x)\n",
"dispExp $ lam y (Var y)\n",
"\n",
"lam x (Var x) `aeq` lam y (Var y)"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Lam (λx.λy.y x
"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"e\n",
"dispExp e"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"(λx.λy.y x) (λx.λy.y x) (λx.λy.y x)
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"λy.y (λx.λy.y x)
"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"dispExp (App (App e e) e)\n",
"dispExp $ runFreshM $ eval (App (App e e) e)"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [],
"source": [
"tmId = lam x (Var x)\n",
"tm1 = App tmId tmId `App` App tmId tmId\n",
"tm2 = lam y $ App tmId tmId `App` App tmId tmId"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"λx.x
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"λx.x
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"(λx.x) (λx.x) ((λx.x) (λx.x))
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"λx.x
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"λy.(λx.x) (λx.x) ((λx.x) (λx.x))
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"λy.(λx.x) (λx.x) ((λx.x) (λx.x))
"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"dispExp tmId\n",
"dispExp $ runFreshM $ eval tmId\n",
"dispExp tm1\n",
"dispExp $ runFreshM $ eval tm1\n",
"dispExp tm2\n",
"dispExp $ runFreshM $ eval tm2"
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"fv :: forall a b (f :: * -> *). (Alpha a, Typeable b, Contravariant f, Applicative f) => (Name b -> f (Name b)) -> a -> f a"
],
"text/plain": [
"fv :: forall a b (f :: * -> *). (Alpha a, Typeable b, Contravariant f, Applicative f) => (Name b -> f (Name b)) -> a -> f a"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"toListOf :: forall s a. Fold s a -> s -> [a]"
],
"text/plain": [
"toListOf :: forall s a. Fold s a -> s -> [a]"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"fv' :: forall s. Alpha s => s -> [Nm]"
],
"text/plain": [
"fv' :: forall s. Alpha s => s -> [Nm]"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
":type fv\n",
":type toListOf\n",
"fv' e = toListOf fv e :: [Nm]\n",
":type fv'"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"[]"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
"[x]"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
"[x,y]"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
"[z]"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"fv' tmId\n",
"fv' (Var x)\n",
"fv' (Var x `App` Var y)\n",
"fv' (lam x . lam y $ (Var x `App` Var y) `App` Var z)"
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"red :: forall (m :: * -> *). Fresh m => Exp -> m Exp"
],
"text/plain": [
"red :: forall (m :: * -> *). Fresh m => Exp -> m Exp"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"-- reduce all the way (may diverge)\n",
"red (App e1 e2) = do\n",
" e1' <- red e1\n",
" e2' <- red e2\n",
" case e1' of\n",
" Lam bnd -> do\n",
" (x, e1'') <- unbind bnd\n",
" return $ subst x e2' e1''\n",
" _ -> return $ App e1' e2'\n",
"red (Lam bnd) = do\n",
" (x, e) <- unbind bnd\n",
" e' <- red e\n",
" case e of\n",
" App e1 (Var y) | y == x && x `notElem` fv' e1 -> return e1\n",
" _ -> return $ lam x e'\n",
"red (Var x) = return $ Var x\n",
"\n",
":type red"
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Lam (λy.(λx.x) (λx.x) ((λx.x) (λx.x))
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"λy.λx5.x5
"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"tm2\n",
"dispExp $ runFreshM $ eval tm2\n",
"dispExp $ runFreshM $ red tm2"
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"step :: forall (f :: * -> *). (Alternative f, Fresh f) => Exp -> f Exp"
],
"text/plain": [
"step :: forall (f :: * -> *). (Alternative f, Fresh f) => Exp -> f Exp"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"beta :: forall (m :: * -> *). (Fresh m, Alternative m) => Exp -> m Exp"
],
"text/plain": [
"beta :: forall (m :: * -> *). (Fresh m, Alternative m) => Exp -> m Exp"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"import Control.Applicative \n",
"\n",
"-- single step reduction\n",
"step e@(App e1 e2) = beta e\n",
" <|> (App <$> step e1 <*> pure e2)\n",
" <|> (App <$> pure e1 <*> step e2)\n",
"step (Lam bnd) = do (x, e) <- unbind bnd\n",
" lam x <$> step e\n",
"step (Var x) = empty\n",
"\n",
"\n",
"beta (App (Lam bnd) e2) = do (x, e1) <- unbind bnd\n",
" return $ subst x e2 e1\n",
"beta _ = empty\n",
"\n",
"\n",
":type step\n",
":type beta"
]
},
{
"cell_type": "code",
"execution_count": 19,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"λx.x x
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"(λx.x x) (λx.x x)
"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"omega = lam x $ Var x `App` Var x \n",
"tmOmega = App omega omega -- well known diverging term\n",
"\n",
"dispExp omega\n",
"dispExp tmOmega"
]
},
{
"cell_type": "code",
"execution_count": 20,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"runFreshMT . step $ tmOmega :: forall (m :: * -> *). MonadPlus m => m Exp"
],
"text/plain": [
"runFreshMT . step $ tmOmega :: forall (m :: * -> *). MonadPlus m => m Exp"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"(λx.x x) (λx.x x)
"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
":type runFreshMT . step $ tmOmega\n",
"map dispExp . runFreshMT . step $ tmOmega"
]
},
{
"cell_type": "code",
"execution_count": 21,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"runFreshMT . step $ tm1 :: forall (m :: * -> *). MonadPlus m => m Exp"
],
"text/plain": [
"runFreshMT . step $ tm1 :: forall (m :: * -> *). MonadPlus m => m Exp"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"(λx.x) ((λx.x) (λx.x))
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"(λx.x) (λx.x) (λx.x)
"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
":type runFreshMT . step $ tm1\n",
"map dispExp . runFreshMT . step $ tm1"
]
},
{
"cell_type": "code",
"execution_count": 22,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"runFreshMT . step $ tm2 :: forall (m :: * -> *). MonadPlus m => m Exp"
],
"text/plain": [
"runFreshMT . step $ tm2 :: forall (m :: * -> *). MonadPlus m => m Exp"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"λy.(λx.x) ((λx.x) (λx.x))
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"λy.(λx.x) (λx.x) (λx.x)
"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
":type runFreshMT . step $ tm2\n",
"map dispExp . runFreshMT . step $ tm2"
]
},
{
"cell_type": "code",
"execution_count": 23,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"(λx.x) (λy.y) ((λx.x) (λz.z))
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
"list1:"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"(λy.y) ((λx.x) (λz.z))
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"(λx.x) (λy.y) (λz.z)
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
"list2:"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"(λx.x) (λz.z)
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"(λy.y) (λz.z)
"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"(λy.y) (λz.z)
"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"tm10 = (App (lam x $ Var x) (lam y $ Var y) `App` App (lam x $ Var x) (lam z $ Var z))\n",
"\n",
"list1 :: [Exp]\n",
"list1 = runFreshMT . step $ tm10\n",
"list2 :: [[Exp]]\n",
"list2 = map (runFreshMT . step) list1\n",
"\n",
"dispExp tm10\n",
"putStrLn \"list1:\"\n",
"map dispExp list1\n",
"putStrLn \"list2:\"\n",
"map (map dispExp) list2"
]
},
{
"cell_type": "code",
"execution_count": 24,
"metadata": {},
"outputs": [],
"source": [
"import Data.Tree hiding (drawTree)\n",
"import Data.Tree.View\n",
"\n",
"redTree e = Node e (map redTree . runFreshMT . step $ e)"
]
},
{
"cell_type": "code",
"execution_count": 25,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"showTree . fmap showExp :: Tree Exp -> String"
],
"text/plain": [
"showTree . fmap showExp :: Tree Exp -> String"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
":type showTree . fmap showExp\n",
"drawTreeExp = showTree . fmap showExp"
]
},
{
"cell_type": "code",
"execution_count": 26,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"(λx.x) (λy.y) ((λx.x) (λz.z))\n",
" ├╴(λy.y) ((λx.x) (λz.z))\n",
" │ ├╴(λx.x) (λz.z)\n",
" │ │ └╴λz.z\n",
" │ └╴(λy.y) (λz.z)\n",
" │ └╴λz.z\n",
" └╴(λx.x) (λy.y) (λz.z)\n",
" └╴(λy.y) (λz.z)\n",
" └╴λz.z"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"putStrLn $ drawTreeExp $ redTree (App (lam x $ Var x) (lam y $ Var y) `App` App (lam x $ Var x) (lam z $ Var z))"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Haskell",
"language": "haskell",
"name": "haskell"
},
"language_info": {
"codemirror_mode": "ihaskell",
"file_extension": ".hs",
"name": "haskell",
"pygments_lexer": "Haskell",
"version": "8.6.5"
}
},
"nbformat": 4,
"nbformat_minor": 4
}