Last active
February 14, 2016 05:37
-
-
Save izgzhen/a621ee6621f2443289f1 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
data Expr = EApp Expr Expr | |
| EAbs String Expr | |
| EVar String | |
| EInt Int | |
deriving (Show) | |
-- (λx.x x) (λx.x x) | |
unterminating = EApp (EAbs "x" (EApp (EVar "x") (EVar "x"))) (EAbs "x" (EApp (EVar "x") (EVar "x"))) | |
-- (λy.1) ((λx.x x) (λx.x x)) | |
expr = EApp (EAbs "y" (EInt 1)) unterminating | |
{- | |
The problem is: what leads to the laziness that promises the termination of above expression? | |
-} | |
interpret :: Expr -> Expr | |
interpret (EInt i) = EInt i | |
interpret (EVar x) = error $ "unbound " ++ x | |
interpret (EApp (EAbs x body) e) = subst x e body | |
interpret (EApp e1 e2) = EApp (interpret e1) (interpret e2) | |
interpret (EAbs x body) = EAbs x body | |
interpret' :: Expr -> Expr | |
interpret' expr = | |
let expr' = interpret expr | |
in if isNormalForm expr' then expr' | |
else interpret' expr' | |
subst :: String -> Expr -> Expr -> Expr | |
subst x e (EInt i) = EInt i | |
subst x e (EVar x') | |
| x == x' = e | |
| otherwise = EVar x' | |
subst x e (EApp e1 e2) = EApp (subst x e e1) (subst x e e2) | |
subst x e (EAbs x' body) | |
| x == x' = EAbs x body | |
| otherwise = EAbs x (subst x e body) | |
isNormalForm :: Expr -> Bool | |
isNormalForm (EInt _) = True | |
isNormalForm (EAbs _ _) = True | |
isNormalForm (EVar _) = True | |
isNormalForm (EApp _ _) = False | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
In line 21, even if we wrote
subst x (interpret e) body
, theexpr
will still terminate. But this is due to the laziness of Haskell. If we write the same thing in ML, it will not terminate.So maybe we could say, the laziness of Haskell doesn't contribute to the laziness of target language, if we can always find a way to write the interpreter such that whether host language is Haskell or ML, the laziness of target language is the same.