From f0e0d82a7776f965a32e5d2bb93aae349a6c2b72 Mon Sep 17 00:00:00 2001 From: Vitor Coimbra de Oliveira Date: Sat, 24 Sep 2016 22:30:03 -0300 Subject: [PATCH] Fix let inferece (attempts to fix #72 and #82). Adds the offending functions to test.ml. --- 006_hindley_milner.md | 50 +++++++------- CONTRIBUTORS.md | 1 + chapter7/poly_constraints/poly.cabal | 3 +- chapter7/poly_constraints/src/Infer.hs | 96 ++++++++++++-------------- chapter7/poly_constraints/test.ml | 18 +++-- 5 files changed, 86 insertions(+), 82 deletions(-) diff --git a/006_hindley_milner.md b/006_hindley_milner.md index 7955011..b32ad0e 100644 --- a/006_hindley_milner.md +++ b/006_hindley_milner.md @@ -109,7 +109,7 @@ Polymorphism We will add an additional constructs to our language that will admit a new form of *polymorphism* for our language. Polymorphism is the property of a term to simultaneously admit several distinct types for the same function -implementation. +implementation. For instance the polymorphic signature for the identity function maps an input of type $\alpha$ @@ -123,7 +123,7 @@ $$ Now instead of having to duplicate the functionality for every possible type (i.e. implementing idInt, idBool, ...) we our type system admits any -instantiation that is subsumed by the polymorphic type signature. +instantiation that is subsumed by the polymorphic type signature. $$ \begin{aligned} @@ -425,13 +425,13 @@ $$ \tau_1 \sim \tau_1' : \theta_1 \andalso [\theta_1] \tau_2 \sim [\theta_1] \tau_2' : \theta_2 }{ \tau_1 \tau_2 \sim \tau_1' \tau_2' : \theta_2 \circ \theta_1 -} +} & \quad \trule{Uni-Con} \\ \\ \infrule{ \tau_1 \sim \tau_1' : \theta_1 \andalso [\theta_1] \tau_2 \sim [\theta_1] \tau_2' : \theta_2 }{ \tau_1 \rightarrow \tau_2 \sim \tau_1' \rightarrow \tau_2' : \theta_2 \circ \theta_1 -} +} & \quad \trule{Uni-Arrow} \\ \\ \end{array} $$ @@ -560,9 +560,9 @@ By contrast, binding ``f`` in a lambda will result in a type error. ```haskell Poly> (\f -> let g = (f True) in (f 3)) (\x -> x) -Cannot unify types: +Cannot unify types: Bool -with +with Int ``` @@ -572,7 +572,7 @@ Typing Rules ------------ And finally with all the typing machinery in place, we can write down the typing -rules for our simple little polymorphic lambda calculus. +rules for our simple little polymorphic lambda calculus. ```haskell infer :: TypeEnv -> Expr -> Infer (Subst, Type) @@ -691,8 +691,8 @@ $$ **T-App** For applications, the first argument must be a lambda expression or return a -lambda expression, so know it must be of form ``t1 -> t2`` but the output type -is not determined except by the confluence of the two values. We infer both +lambda expression, so we know it must be of form ``t1 -> t2`` but the output +type is not determined except by the confluence of the two values. We infer both types, apply the constraints from the first argument over the result second inferred type and then unify the two types with the excepted form of the entire application expression. @@ -760,9 +760,9 @@ ops = Map.fromList [ $$ \begin{array}{cl} -(+) &: \t{Int} \rightarrow \t{Int} \rightarrow \t{Int} \\ -(\times) &: \t{Int} \rightarrow \t{Int} \rightarrow \t{Int} \\ -(-) &: \t{Int} \rightarrow \t{Int} \rightarrow \t{Int} \\ +(+) &: \t{Int} \rightarrow \t{Int} \rightarrow \t{Int} \\ +(\times) &: \t{Int} \rightarrow \t{Int} \rightarrow \t{Int} \\ +(-) &: \t{Int} \rightarrow \t{Int} \rightarrow \t{Int} \\ (=) &: \t{Int} \rightarrow \t{Int} \rightarrow \t{Bool} \\ \end{array} $$ @@ -786,7 +786,7 @@ Constraint Generation The previous implementation of Hindley Milner is simple, but has this odd property of intermingling two separate processes: constraint solving and traversal. Let's discuss another implementation of the inference algorithm that -does not do this. +does not do this. In the *constraint generation* approach, constraints are generated by bottom-up traversal, added to a ordered container, canonicalized, solved, and then @@ -841,7 +841,7 @@ Typing The typing rules are identical, except they now can be written down in a much less noisy way that isn't threading so much state. All of the details are taken care of under the hood and encoded in specific combinators manipulating the -state of our Infer monad in a way that lets focus on the domain logic. +state of our Infer monad in a way that lets us focus on the domain logic. ```haskell infer :: Expr -> Infer Type @@ -993,7 +993,7 @@ By applying **Uni-Arrow** we can then deduce the following set of substitutions. 1. ``a ~ Int`` 2. ``b ~ Int`` 3. ``c ~ Int`` -4. ``d ~ Int`` +4. ``d ~ Int`` 5. ``e ~ Int`` Substituting this solution back over the type yields the inferred type: @@ -1033,7 +1033,7 @@ So we get this type: compose :: forall c d e. (d -> e) -> (c -> d) -> c -> e ``` -If desired, we can rename the variables in alphabetical order to get: +If desired, we can rename the variables in alphabetical order to get: ```haskell compose :: forall a b c. (a -> b) -> (c -> a) -> c -> b @@ -1086,7 +1086,7 @@ eval env expr = case expr of VInt b' <- eval env b return $ (binop op) a' b' - Lam x body -> + Lam x body -> return (VClosure x body env) App fun arg -> do @@ -1338,9 +1338,9 @@ Also programs that are also not well-typed are now rejected outright as well. ```haskell Poly> 1 + True -Cannot unify types: +Cannot unify types: Bool -with +with Int ``` @@ -1356,15 +1356,15 @@ instance both ``fact`` and ``fib`` functions uses the fixpoint to compute Fibonacci numbers or factorials. ```haskell -let fact = fix (\fact -> \n -> - if (n == 0) - then 1 +let fact = fix (\fact -> \n -> + if (n == 0) + then 1 else (n * (fact (n-1)))); -let rec fib n = - if (n == 0) +let rec fib n = + if (n == 0) then 0 - else if (n==1) + else if (n==1) then 1 else ((fib (n-1)) + (fib (n-2))); ``` diff --git a/CONTRIBUTORS.md b/CONTRIBUTORS.md index 0501c08..4d5a33e 100644 --- a/CONTRIBUTORS.md +++ b/CONTRIBUTORS.md @@ -15,3 +15,4 @@ Contributors * Christian Sievers * Franklin Chen * Jake Taylor +* Vitor Coimbra diff --git a/chapter7/poly_constraints/poly.cabal b/chapter7/poly_constraints/poly.cabal index 6256e6a..ddd193b 100644 --- a/chapter7/poly_constraints/poly.cabal +++ b/chapter7/poly_constraints/poly.cabal @@ -9,7 +9,7 @@ extra-source-files: README.md cabal-version: >=1.10 executable poly - build-depends: + build-depends: base >= 4.6 && <4.9 , pretty >= 1.1 && <1.2 , parsec >= 3.1 && <3.2 @@ -20,6 +20,7 @@ executable poly , repline >= 0.1.2.0 other-modules: + Env Eval Infer Lexer diff --git a/chapter7/poly_constraints/src/Infer.hs b/chapter7/poly_constraints/src/Infer.hs index 30e1673..0d27259 100644 --- a/chapter7/poly_constraints/src/Infer.hs +++ b/chapter7/poly_constraints/src/Infer.hs @@ -16,7 +16,7 @@ import Syntax import Control.Monad.Except import Control.Monad.State -import Control.Monad.RWS +import Control.Monad.Reader import Control.Monad.Identity import Data.List (nub) @@ -28,12 +28,12 @@ import qualified Data.Set as Set ------------------------------------------------------------------------------- -- | Inference monad -type Infer a = (RWST +type Infer a = (ReaderT Env -- Typing environment - [Constraint] -- Generated constraints - InferState -- Inference state + (StateT -- Inference state + InferState (Except -- Inference errors - TypeError) + TypeError)) a) -- Result -- | Inference state @@ -95,8 +95,8 @@ data TypeError ------------------------------------------------------------------------------- -- | Run the inference monad -runInfer :: Env -> Infer Type -> Either TypeError (Type, [Constraint]) -runInfer env m = runExcept $ evalRWST m env initInfer +runInfer :: Env -> Infer (Type, [Constraint]) -> Either TypeError (Type, [Constraint]) +runInfer env m = runExcept $ evalStateT (runReaderT m env) initInfer -- | Solve for the toplevel type of an expression in a given environment inferExpr :: Env -> Expr -> Either TypeError Scheme @@ -112,7 +112,7 @@ constraintsExpr env ex = case runInfer env (infer ex) of Left err -> Left err Right (ty, cs) -> case runSolve cs of Left err -> Left err - Right subst -> Right $ (cs, subst, ty, sc) + Right subst -> Right (cs, subst, ty, sc) where sc = closeOver $ apply subst ty @@ -120,10 +120,6 @@ constraintsExpr env ex = case runInfer env (infer ex) of closeOver :: Type -> Scheme closeOver = normalize . generalize Env.empty --- | Unify two types -uni :: Type -> Type -> Infer () -uni t1 t2 = tell [(t1, t2)] - -- | Extend type environment inEnv :: (Name, Scheme) -> Infer a -> Infer a inEnv (x, sc) m = do @@ -150,7 +146,7 @@ fresh = do instantiate :: Scheme -> Infer Type instantiate (Forall as t) = do - as' <- mapM (\_ -> fresh) as + as' <- mapM (const fresh) as let s = Subst $ Map.fromList $ zip as as' return $ apply s t @@ -158,66 +154,64 @@ generalize :: Env -> Type -> Scheme generalize env t = Forall as t where as = Set.toList $ ftv t `Set.difference` ftv env -ops :: Map.Map Binop Type -ops = Map.fromList [ - (Add, (typeInt `TArr` (typeInt `TArr` typeInt))) - , (Mul, (typeInt `TArr` (typeInt `TArr` typeInt))) - , (Sub, (typeInt `TArr` (typeInt `TArr` typeInt))) - , (Eql, (typeInt `TArr` (typeInt `TArr` typeBool))) - ] +ops :: Binop -> Type +ops Add = typeInt `TArr` (typeInt `TArr` typeInt) +ops Mul = typeInt `TArr` (typeInt `TArr` typeInt) +ops Sub = typeInt `TArr` (typeInt `TArr` typeInt) +ops Eql = typeInt `TArr` (typeInt `TArr` typeBool) -infer :: Expr -> Infer Type +infer :: Expr -> Infer (Type, [Constraint]) infer expr = case expr of - Lit (LInt _) -> return $ typeInt - Lit (LBool _) -> return $ typeBool + Lit (LInt _) -> return (typeInt, []) + Lit (LBool _) -> return (typeBool, []) - Var x -> lookupEnv x + Var x -> do + t <- lookupEnv x + return (t, []) Lam x e -> do tv <- fresh - t <- inEnv (x, Forall [] tv) (infer e) - return (tv `TArr` t) + (t, c) <- inEnv (x, Forall [] tv) (infer e) + return (tv `TArr` t, c) App e1 e2 -> do - t1 <- infer e1 - t2 <- infer e2 + (t1, c1) <- infer e1 + (t2, c2) <- infer e2 tv <- fresh - uni t1 (t2 `TArr` tv) - return tv + return (tv, c1 ++ c2 ++ [(t1, t2 `TArr` tv)]) Let x e1 e2 -> do env <- ask - t1 <- infer e1 - let sc = generalize env t1 - t2 <- inEnv (x, sc) (infer e2) - return t2 + (t1, c1) <- infer e1 + case runSolve c1 of + Left err -> throwError err + Right sub -> do + let sc = generalize (apply sub env) (apply sub t1) + (t2, c2) <- inEnv (x, sc) $ local (apply sub) (infer e2) + return (t2, c1 ++ c2) Fix e1 -> do - t1 <- infer e1 + (t1, c1) <- infer e1 tv <- fresh - uni (tv `TArr` tv) t1 - return tv + return (tv, c1 ++ [(tv `TArr` tv, t1)]) Op op e1 e2 -> do - t1 <- infer e1 - t2 <- infer e2 + (t1, c1) <- infer e1 + (t2, c2) <- infer e2 tv <- fresh let u1 = t1 `TArr` (t2 `TArr` tv) - u2 = ops Map.! op - uni u1 u2 - return tv + u2 = ops op + return (tv, c1 ++ c2 ++ [(u1, u2)]) If cond tr fl -> do - t1 <- infer cond - t2 <- infer tr - t3 <- infer fl - uni t1 typeBool - uni t2 t3 - return t2 + (t1, c1) <- infer cond + (t2, c2) <- infer tr + (t3, c3) <- infer fl + return (t2, c1 ++ c2 ++ c3 ++ [(t1, typeBool), (t2, t3)]) inferTop :: Env -> [(String, Expr)] -> Either TypeError Env inferTop env [] = Right env -inferTop env ((name, ex):xs) = case (inferExpr env ex) of +inferTop env ((name, ex):xs) = case inferExpr env ex of Left err -> Left err Right ty -> inferTop (extend env (name, ty)) xs @@ -276,12 +270,12 @@ solver (su, cs) = [] -> return su ((t1, t2): cs0) -> do su1 <- unifies t1 t2 - solver (su1 `compose` su, (apply su1 cs0)) + solver (su1 `compose` su, apply su1 cs0) bind :: TVar -> Type -> Solve Subst bind a t | t == TVar a = return emptySubst | occursCheck a t = throwError $ InfiniteType a t - | otherwise = return $ (Subst $ Map.singleton a t) + | otherwise = return (Subst $ Map.singleton a t) occursCheck :: Substitutable a => TVar -> a -> Bool occursCheck a t = a `Set.member` ftv t diff --git a/chapter7/poly_constraints/test.ml b/chapter7/poly_constraints/test.ml index 72f3802..6785f2a 100644 --- a/chapter7/poly_constraints/test.ml +++ b/chapter7/poly_constraints/test.ml @@ -47,7 +47,7 @@ let sub m n = (n pred) m; let unbool n = n True False; let unchurch n = n (\i -> i + 1) 0; -let rec church n = +let rec church n = if (n == 0) then zero else \f x -> f (church (n-1) f x); @@ -77,10 +77,10 @@ let indx xs n = head (n tail xs); let fact = fix (\fact -> \n -> if (n == 0) then 1 else (n * (fact (n-1)))); -let rec fib n = - if (n == 0) +let rec fib n = + if (n == 0) then 0 - else if (n==1) + else if (n==1) then 1 else ((fib (n-1)) + (fib (n-2))); @@ -97,6 +97,14 @@ let self = (\x -> x) (\x -> x); let innerlet = \x -> (let y = \z -> z in y); let innerletrec = \x -> (let rec y = \z -> z in y); +-- Issue #72 +let f = let add = \a b -> a + b in add; + +-- Issue #82 +let y = \y -> (let f = \x -> if x then True else False in const (f y) y); +let id x = x; +let foo x = let y = id x in y + 1; + -- Fresh variables let wtf = \a b c d e e' f g h i j k l m n o o' o'' o''' p q r r' s t u u' v w x y z -> q u i c k b r o w n f o' x j u' m p s o'' v e r' t h e' l a z y d o''' g; @@ -105,7 +113,7 @@ let wtf = \a b c d e e' f g h i j k l m n o o' o'' o''' p q r r' s t u u' v w x let notbool x = if x then False else True; let eqzero x = if (x == 0) then True else False; -let rec until p f x = +let rec until p f x = if (p x) then x else (until p f (f x));