nv <- newVar
instantiate $ substituteS (Map.singleton v nv) t
+generalize :: TypeEnv -> Type -> TypeScheme
+generalize e t = foldr TSForAll (TScheme t) vars
+ where
+ vars = Set.toList $ freeVarsT t Set.\\ Set.unions (map freeVarsS $ Map.elems e)
+
unify :: Type -> Type -> TI Substitution
unify (TypeVar a) t = varBind a t
unify t (TypeVar a) = varBind a t
let e' = Map.insert x (TScheme tv) e
(s, t) <- ti e' y
return (s, TypeFunction (substituteT s tv) t)
-
+ti e (NTTerm (App a b)) = do
+ tv <- newVar
+ (s1, t1) <- ti e a
+ (s2, t2) <- ti (Map.map (substituteS s1) e) b
+ s3 <- unify (substituteT s2 t1) (TypeFunction t2 tv)
+ return (s3 `composeSub` s2 `composeSub` s1, substituteT s3 tv)
+ti e (NTTerm (Let x a b)) = do
+ (s1, t1) <- ti e a
+ let t' = generalize (Map.map (substituteS s1) e) t1
+ e' = Map.insert x t' e
+ (s2, t2) <- ti (Map.map (substituteS s1) e') b
+ return (s1 `composeSub` s2, t2)
+
+
algW :: TypedTerm -> TI Type
algW t = do
(s, u) <- ti Map.empty t
module HM.Parser
( tRead
- , parseTerm
+ , parseTypedTerm
) where
import Data.Char (isAsciiLower, isAsciiUpper)
instance Show TypedTerm where
show (NTTerm t) = show t
- show (TTerm t tp) = braced $ show t ++ " :: " ++ show tp
+ show (TTerm (Var x) tp) = x ++ " :: " ++ show tp
+ show (TTerm t tp) = braced (show t) ++ " :: " ++ show tp
instance Show Type where
show (Primitive t) = t
parseTerm :: Parser Term
parseTerm = parseLet <|>
parseApp <|>
+ parseBraces parseTerm <|>
parseVar <|>
parseLambda
parseTermNoApp :: Parser Term
-parseTermNoApp = parseLet <|>
+parseTermNoApp = parseBraces parseTerm <|>
+ parseLet <|>
parseVar <|>
parseLambda
parseTypedTermNoApp :: Parser TypedTerm
-parseTypedTermNoApp = parseBraces parseTypedTerm <|>
- parseTypeAndTerm parseTermNoApp <|>
+parseTypedTermNoApp = parseTypeAndTerm parseTermNoApp <|>
+ parseBraces parseTypedTerm <|>
(NTTerm <$> parseTermNoApp)
parseTypedTerm :: Parser TypedTerm
-parseTypedTerm = parseBraces parseTypedTerm <|>
- parseTypeAndTerm parseTerm <|>
+parseTypedTerm = parseTypeAndTerm parseTerm <|>
+ parseBraces parseTypedTerm <|>
(NTTerm <$> parseTerm)
parseType :: Parser Type