{ "cells": [ { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [ { "data": { "text/html": [ "
Unused LANGUAGE pragma
Found:
{-# LANGUAGE DeriveDataTypeable, DeriveGeneric, FlexibleInstances,\n", " FlexibleContexts, MultiParamTypeClasses #-}
Why Not:
{-# LANGUAGE FlexibleInstances, FlexibleContexts,\n", " MultiParamTypeClasses #-}
" ], "text/plain": [ "Line 1: Unused LANGUAGE pragma\n", "Found:\n", "{-# LANGUAGE DeriveDataTypeable, DeriveGeneric, FlexibleInstances,\n", " FlexibleContexts, MultiParamTypeClasses #-}\n", "Why not:\n", "{-# LANGUAGE FlexibleInstances, FlexibleContexts,\n", " MultiParamTypeClasses #-}" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "{-# LANGUAGE DeriveDataTypeable\n", " , DeriveGeneric\n", " , FlexibleInstances\n", " , FlexibleContexts\n", " , MultiParamTypeClasses #-}\n", "\n", "import Unbound.Generics.LocallyNameless\n", "import Unbound.Generics.LocallyNameless.Internal.Fold\n", "\n", "import GHC.Generics (Generic)\n", "import Data.Typeable (Typeable)" ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [], "source": [ "-- | Names for expressions\n", "type Nm = Name Exp\n", "\n", "\n", "-- | Expressions\n", "data Exp = Var Nm -- ^ variables\n", " | Lam (Bind Nm Exp) -- ^ lambdas bind a variable within a body expression\n", " | App Exp Exp -- ^ application\n", " deriving (Show, Generic, Typeable)\n", "\n", "-- Automatically construct alpha equiv, free vars, and binding operations.\n", "instance Alpha Exp\n", "\n", "-- semi-automatically implement capture avoiding substitution\n", "instance Subst Exp Exp where\n", " -- `isvar` identifies the variable case in your AST.\n", " isvar (Var x) = Just (SubstName x)\n", " isvar _ = Nothing" ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [ { "data": { "text/html": [ "unsafeUnbind :: forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)" ], "text/plain": [ "unsafeUnbind :: forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "import Unbound.Generics.LocallyNameless.Unsafe\n", ":type unsafeUnbind" ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, "outputs": [ { "data": { "text/html": [ "
Redundant bracket
Found:
(Lam{})
Why Not:
Lam{}
Redundant bracket
Found:
(Var{})
Why Not:
Var{}
" ], "text/plain": [ "Line 13: Redundant bracket\n", "Found:\n", "(Lam{})\n", "Why not:\n", "Lam{}Line 15: Redundant bracket\n", "Found:\n", "(Var{})\n", "Why not:\n", "Var{}" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "import IHaskell.Display\n", "\n", "showExp = ppExp \"λ\" \".\"\n", "printExp = putStrLn . showExp\n", "dispExp e = 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 ( Var 0@0)" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "Lam ( Var 0@0)" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "λ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 ( Lam ( App (Var 0@0) (Var 1@0)))" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/html": [ "λ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 ( App (App (Lam ( Var 0@0)) (Lam ( Var 0@0))) (App (Lam ( Var 0@0)) (Lam ( Var 0@0))))" ] }, "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.λ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": [ "
Redundant bracket
Found:
(App (lam x \\$ Var x) (lam y \\$ Var y) `App`\n", " App (lam x \\$ Var x) (lam z \\$ Var z))
Why Not:
App (lam x \\$ Var x) (lam y \\$ Var y) `App`\n", " App (lam x \\$ Var x) (lam z \\$ Var z)
" ], "text/plain": [ "Line 1: Redundant bracket\n", "Found:\n", "(App (lam x $ Var x) (lam y $ Var y) `App`\n", " App (lam x $ Var x) (lam z $ Var z))\n", "Why not:\n", "App (lam x $ Var x) (lam y $ Var y) `App`\n", " App (lam x $ Var x) (lam z $ Var z)" ] }, "metadata": {}, "output_type": "display_data" }, { "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 }