TypeInference.hs revision 9db48b4604636bfdf03e60890fc094b7bec775dc
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder Author: Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder polymorphic type inference (with type classes) for terms
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder limitiations:
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder - no subtyping
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder - ignore anonymous downsets as classes
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder - an intersection class is a (flat) set of class names (without universe)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder - no mixfix analysis for types yet
d48085f765fca838c1d972d2123601997174583dChristian Maeder - use predicate types as in Wadler/Blott 1989 (ad-hoc polymorphism)?
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder - treat all arrows equal for unification and type inference
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder - and also ignore lazy annotations!
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder simply adapt the following
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder-- Part of `Typing Haskell in Haskell', version of November 23, 2000
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder-- Copyright (c) Mark P Jones and the Oregon Graduate Institute
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder-- of Science and Technology, 1999-2000
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder-- This program is distributed as Free Software under the terms
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder-- in the file "License" that is included in the distribution
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder-- of this software, copies of which may be obtained from:
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedermodule TypeInference where
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maederimport FiniteMap
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport List -- (nub, (\\), intersect, union, partition)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Monad(msum)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport MonadState
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederenumId :: Int -> Id
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederenumId n = Id[Token "v" nullPos, Token (show n) nullPos][][]
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaedertArrow = TCon (Tycon (Id [Token "->?" nullPos][][])
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Kfun star (Kfun star star)))
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedera `fn` b = TAp (TAp tArrow a) b
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederclass HasKind t where
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederinstance HasKind Tyvar where
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder kind (Tyvar _ k) = k
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederinstance HasKind Tycon where
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder kind (Tycon _ k) = k
df33a9af92444f63ad545da6bb326aac9284318eChristian Maederinstance HasKind Le.Type where
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder kind (TCon tc) = kind tc
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder kind (TVar u) = kind u
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder kind (TAp t _) = case (kind t) of
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder Kfun _ k -> k
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder Star _ -> error "wrong kind for TAp"
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder kind (TGen _) = error "no kind for TGen"
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder-----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- Subst: Substitutions
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder-----------------------------------------------------------------------------
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maedertype Subst = FiniteMap Tyvar Le.Type
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaedernullSubst :: Subst
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaedernullSubst = emptyFM
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder(+->) :: Tyvar -> Le.Type -> Subst
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederu +-> t = unitFM u t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederclass SubstApplicable t where
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian Maeder apply :: Subst -> t -> t
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder tv :: t -> [Tyvar]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance SubstApplicable Le.Type where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder apply s (TVar u) = case lookupFM s u of
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder Nothing -> TVar u
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder apply s (TAp l r) = TAp (apply s l) (apply s r)
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder apply _ t = t
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder tv (TVar u) = [u]
d48085f765fca838c1d972d2123601997174583dChristian Maeder tv (TAp l r) = tv l `union` tv r
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance SubstApplicable a => SubstApplicable [a] where
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder apply s = map (apply s)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder tv = nub . concat . map tv
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder(@@) :: Subst -> Subst -> Subst
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeders1 @@ s2 = plusFM (mapFM (const $ apply s1) s2) s1
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder-----------------------------------------------------------------------------
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder-- Unify: Unification
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder-----------------------------------------------------------------------------
df33a9af92444f63ad545da6bb326aac9284318eChristian Maedermgu, match :: Monad m => Le.Type -> Le.Type -> m Subst
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maedermgum :: Monad m => Bool -> Le.Type -> Le.Type -> m Subst
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maedermgu = mgum False
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maedermatch = mgum True
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maedermgum b (TAp l r) (TAp l' r') = do s1 <- mgum b l l'
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder s2 <- mgum b (apply s1 r)
df33a9af92444f63ad545da6bb326aac9284318eChristian Maeder (if b then r' else apply s1 r')
04a1ed0b360858b85de6f449b84df4eab81b3fc9Christian Maeder return (s2 @@ s1)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maedermgum _ (TVar u) t = varBind u t
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maedermgum b t (TVar u) = if b then fail
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder "a non-variable does not match a variable"
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder else varBind u t
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maedermgum _ (TCon tc1) (TCon tc2)
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder | tc1==tc2 = return nullSubst
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maedermgum b _ _ = fail ("types do not " ++ if b then "match" else "unify")
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedervarBind :: Monad m => Tyvar -> Le.Type -> m Subst
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian MaedervarBind u t | t == TVar u = return nullSubst
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder | u `elem` tv t = fail "occurs check fails"
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder | kind u /= kind t = fail "kinds do not match"
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder | otherwise = return (u +-> t)
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder-----------------------------------------------------------------------------
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder-- Pred: Predicates
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder-----------------------------------------------------------------------------
99f16a0f9ca757410960ff51a79b034503384fe2Christian Maederinstance SubstApplicable t => SubstApplicable (Qual t) where
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder apply s (ps :=> t) = apply s ps :=> apply s t
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder tv (ps :=> t) = tv ps `union` tv t
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maederinstance SubstApplicable Pred where
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder apply s (IsIn i t) = IsIn i (apply s t)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder tv (IsIn _ t) = tv t
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaedermguPred, matchPred :: Pred -> Pred -> Maybe Subst
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaedermguPred = liftToPred mgu
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaedermatchPred = liftToPred match
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederliftToPred :: Monad m => (Le.Type -> Le.Type -> m Subst)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder -> Pred -> Pred -> m Subst
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederliftToPred m (IsIn i t) (IsIn i' t')
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder | i == i' = m t t'
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder | otherwise = fail "classes differ"
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maederdefined :: Maybe a -> Bool
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maederdefined (Just _) = True
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maederdefined Nothing = False
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maedertype EnvTransformer = ClassEnv -> Maybe ClassEnv
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder(<:>) :: EnvTransformer -> EnvTransformer -> EnvTransformer
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder(f <:> g) ce = do ce' <- f ce
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederaddClass :: Id -> [Id] -> EnvTransformer
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederaddClass i is ce
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | i `elemFM` ce = fail "class already defined"
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder | not $ null $ is \\ keysFM ce = fail "superclass not defined"
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder | otherwise = return (addToFM ce i (is, []))
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederaddPreludeClasses :: EnvTransformer
37354e3ed68875fb527338105a610df481f98cb0Christian MaederaddPreludeClasses = addCoreClasses
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederaddCoreClasses :: EnvTransformer
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederaddCoreClasses = const Nothing
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederaddInst :: [Pred] -> Pred -> EnvTransformer
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederaddInst ps p@(IsIn i _) ce
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | not $ i `elemFM` ce = fail "no class for instance"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | any (overlap p) qs = fail "overlapping instance"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | otherwise = return (addToFM ce i c)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder where its = insts ce i
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder qs = [ q | (_ :=> q) <- its ]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder c = (super ce i, (ps:=>p) : its)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederoverlap :: Pred -> Pred -> Bool
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederoverlap p q = defined (mguPred p q)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaederexampleInsts :: EnvTransformer
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederexampleInsts = addPreludeClasses
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-----------------------------------------------------------------------------
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian MaederbySuper :: ClassEnv -> Pred -> [Pred]
09249711700a6acbc40a2e337688b434d7aafa28Christian MaederbySuper ce p@(IsIn i t)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder = p : concat [ bySuper ce (IsIn i' t) | i' <- super ce i ]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederbyInst :: ClassEnv -> Pred -> Maybe [Pred]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederbyInst ce p@(IsIn i _) = msum [ tryInst it | it <- insts ce i ]
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder where tryInst (ps :=> h) = do u <- matchPred h p
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just (map (apply u) ps)
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maederentail :: ClassEnv -> [Pred] -> Pred -> Bool
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maederentail ce ps p = any (p `elem`) (map (bySuper ce) ps) ||
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder case byInst ce p of
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder Nothing -> False
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder Just qs -> all (entail ce ps) qs
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder-----------------------------------------------------------------------------
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian MaederinHnf :: Pred -> Bool
d50ea352472823a62196db3cf11fae2af6866ab6Christian MaederinHnf (IsIn _ t) = hnf t
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder where hnf (TVar _) = True
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder hnf (TCon _) = False
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder hnf (TAp f _) = hnf f
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder hnf (TGen _) = error "no hnf for TGen"
09249711700a6acbc40a2e337688b434d7aafa28Christian MaedertoHnfs :: Monad m => ClassEnv -> [Pred] -> m [Pred]
d50ea352472823a62196db3cf11fae2af6866ab6Christian MaedertoHnfs ce ps = do pss <- mapM (toHnf ce) ps
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder return (concat pss)
d50ea352472823a62196db3cf11fae2af6866ab6Christian MaedertoHnf :: Monad m => ClassEnv -> Pred -> m [Pred]
d50ea352472823a62196db3cf11fae2af6866ab6Christian MaedertoHnf ce p | inHnf p = return [p]
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder | otherwise = case byInst ce p of
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder Nothing -> fail "context reduction"
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder Just ps -> toHnfs ce ps
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maedersimplify :: ClassEnv -> [Pred] -> [Pred]
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maedersimplify ce = loop []
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder where loop rs [] = rs
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder loop rs (p:ps) | entail ce (rs++ps) p = loop rs ps
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder | otherwise = loop (p:rs) ps
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maederreduce :: Monad m => ClassEnv -> [Pred] -> m [Pred]
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maederreduce ce ps = do qs <- toHnfs ce ps
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder return (simplify ce qs)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaederscEntail :: ClassEnv -> [Pred] -> Pred -> Bool
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederscEntail ce ps p = any (p `elem`) (map (bySuper ce) ps)
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder-----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- Scheme: Type schemes
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder-----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance SubstApplicable Scheme where
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder apply s (Scheme ks qt) = Scheme ks (apply s qt)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder tv (Scheme _ qt) = tv qt
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maederquantify :: [Tyvar] -> Qual Le.Type -> Scheme
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maederquantify vs qt = Scheme ks (apply (listToFM s) qt)
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder where vs' = [ v | v <- tv qt, v `elem` vs ]
b06572b54fcf9d6976cfff57da22672f996b4748Christian Maeder ks = map kind vs'
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder s = zip vs' (map TGen [0..])
09249711700a6acbc40a2e337688b434d7aafa28Christian MaedertoScheme :: Le.Type -> Scheme
09249711700a6acbc40a2e337688b434d7aafa28Christian MaedertoScheme t = Scheme [] ([] :=> t)
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder-----------------------------------------------------------------------------
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder-- TIMonad: Type inference monad
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder-----------------------------------------------------------------------------
b06572b54fcf9d6976cfff57da22672f996b4748Christian Maedernewtype TI a = TI {ti :: Subst -> Int -> (Subst, Int, a)}
09249711700a6acbc40a2e337688b434d7aafa28Christian Maederinstance Monad TI where
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder return x = TI (\s n -> (s,n,x))
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder TI f >>= g = TI (\s n -> case f s n of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (s',m,x) -> let TI gx = g x
84e7cfca5b97aef300acdaa8cf63a3572f9151c0Christian MaederrunTI :: Int -> TI a -> a
09249711700a6acbc40a2e337688b434d7aafa28Christian MaederrunTI n (TI f) = x where (_, _, x) = f nullSubst n
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian MaederfreshInst :: Scheme -> TIL (Qual Le.Type)
d50ea352472823a62196db3cf11fae2af6866ab6Christian MaederfreshInst (Scheme ks qt) = do ts <- mapM newTVar ks
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder return (inst ts qt)
30e50372105eacc129a413e390e06036735b69b2Christian Maederclass Instantiate t where
30e50372105eacc129a413e390e06036735b69b2Christian Maeder inst :: [Le.Type] -> t -> t
30e50372105eacc129a413e390e06036735b69b2Christian Maederinstance Instantiate Le.Type where
95a732a847b41efa43b43608fcfcbac3b18dbb4fChristian Maeder inst ts (TAp l r) = TAp (inst ts l) (inst ts r)
30e50372105eacc129a413e390e06036735b69b2Christian Maeder inst ts (TGen n) = ts !! n
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederinstance Instantiate a => Instantiate [a] where
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder inst ts = map (inst ts)
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maederinstance Instantiate t => Instantiate (Qual t) where
f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder inst ts (ps :=> t) = inst ts ps :=> inst ts t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Instantiate Pred where
f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder inst ts (IsIn c t) = IsIn c (inst ts t)
f7663514e02f6095198371a64e574c50e6ec857aChristian Maedertype TIL = StateT (Subst, Int) []
f7663514e02f6095198371a64e574c50e6ec857aChristian MaedernewTVar k = do (s, n) <- get
f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder put (s, n + 1)
f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder return $ TVar (Tyvar (enumId n) k)
f7663514e02f6095198371a64e574c50e6ec857aChristian MaedergetSubst :: TIL Subst
f7663514e02f6095198371a64e574c50e6ec857aChristian MaedergetSubst = gets fst
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maederunify t1 t2 = do s <- getSubst
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder u <- mgu (apply s t1) (apply s t2)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederextSubst :: Subst -> TIL ()
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian MaederextSubst s' = modify (\ (s, n) -> (s'@@s, n))
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedertiTerm :: ClassEnv -> Assumps -> As.Term -> TIL (Qual Le.Type, Le.Term)
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian MaedertiTerm _ as (TermToken t) = let i = simpleIdToId t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do sc@(Scheme ks qs) <- lift (lookUp as i)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ts <- mapM newTVar ks
966e627a1c06b302a06d59d08b8ab45905f3509cChristian Maeder return (inst ts qs, BaseName i sc ts)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedertiTerm ce as (ApplTerm f a _) =
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder do (q1 :=> t1, e1) <- tiTerm ce as f
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder (q2 :=> t2, e2) <- tiTerm ce as a
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder t3 <- newTVar star
f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder unify t1 (t2 `fn` t3)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder return ((q1 ++ q2) :=> t3, Application e1 e2)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- TIMain: Type Inference Algorithm
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-----------------------------------------------------------------------------
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder-- Infer: Basic definitions for type inference
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder-----------------------------------------------------------------------------
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maedertype Infer e t = ClassEnv -> Assumps -> e -> TI (Qual t)
5b2a749acd03ab4f09585251cf38b89bb012dbdcChristian Maeder-----------------------------------------------------------------------------
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder-- Pat: Patterns
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder-----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata Pat = PVar Id
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder | PCon Assumps [Pat]
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaedertiPat :: Pat -> TI (Qual Le.Type, Assumps)
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaedertiPat (PVar i) = do v <- newTVar star
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder return ([] :=> v, unitFM (toScheme v))
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaedertiPat PWildcard = do v <- newTVar star
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder return ([], [], v)
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaedertiPat (PAs i pat) = do (ps, as, t) <- tiPat pat
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder return (ps, (i:>:toScheme t):as, t)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedertiPat (PCon (_:>:sc) pats) = do (ps,as,ts) <- tiPats pats
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder t' <- newTVar star
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder (qs :=> t) <- freshInst sc
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder unify t (foldr fn t' ts)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder return (ps++qs, as, t')
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaedertiPats :: [Pat] -> TI (Qual [Le.Type], Assumps)
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaedertiPats pats = do psasts <- mapM tiPat pats
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder let ps = concat [ ps' | (ps',_,_) <- psasts ]
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder as = concat [ as' | (_,as',_) <- psasts ]
028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maeder ts = [ t | (_,_,t) <- psasts ]
aaf68b27b802d3b9bf39202fa781478dcab8fde5Christian Maeder return (ps, as, ts)
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder-----------------------------------------------------------------------------
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maederdata Expr = Var Id
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder | Const Assumps
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder | Ap Expr Expr
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder | Let BindGroup Expr
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaedertiExpr :: Infer Expr Le.Type
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaedertiExpr _ as (Var i) = do sc <- find i as
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder (ps :=> t) <- freshInst sc
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder return (ps, t)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaedertiExpr _ _ (Const (_:>:sc)) = do (ps :=> t) <- freshInst sc
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder return (ps, t)
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian MaedertiExpr ce as (Ap e f) = do (ps,te) <- tiExpr ce as e
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder (qs,tf) <- tiExpr ce as f
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder t <- newTVar star
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder unify (tf `fn` t) te
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder return (ps++qs, t)
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaedertiExpr ce as (Let bg e) = do (ps, as') <- tiBindGroup ce as bg
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder (qs, t) <- tiExpr ce (as' ++ as) e
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder return (ps ++ qs, t)
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder-----------------------------------------------------------------------------
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maedertype Alt = ([Pat], Expr)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedertiAlt :: Infer Alt Le.Type
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian MaedertiAlt ce as (pats, e) = do (ps, as', ts) <- tiPats pats
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder (qs,t) <- tiExpr ce (as'++as) e
8a6b503b50c0be589f12eb0d4ebeb4b4312fd491Christian Maeder return (ps++qs, foldr fn t ts)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedertiAlts :: ClassEnv -> [Assump] -> [Alt] -> Le.Type -> TI [Pred]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedertiAlts ce as alts t = do psts <- mapM (tiAlt ce as) alts
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mapM (unify t) (map snd psts)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder return (concat (map fst psts))
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-----------------------------------------------------------------------------
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maedersplit :: Monad m => ClassEnv -> [Tyvar] -> [Tyvar] -> [Pred]
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder -> m ([Pred], [Pred])
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedersplit ce fs gs ps = do ps' <- reduce ce ps
d92635f998347112e5d5803301c2abfe7832ab65Christian Maeder let (ds, rs) = partition (all (`elem` fs) . tv) ps'
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder rs' <- defaultedPreds ce (fs++gs) rs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return (ds, rs \\ rs')
da245da15da78363c896e44ea97a14ab1f83eb50Christian Maedertype Ambiguity = (Tyvar, [Pred])
32a2f5f00ff72c095b39629101043db4407974f9Christian Maederambiguities :: ClassEnv -> [Tyvar] -> [Pred] -> [Ambiguity]
32a2f5f00ff72c095b39629101043db4407974f9Christian Maederambiguities _ vs ps = [ (v, filter (elem v . tv) ps) | v <- tv ps \\ vs ]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedernumClasses :: [Id]
1090553a9231ceb536cb8007219c08be0c8c313dChristian MaedernumClasses = []
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederstdClasses :: [Id]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederstdClasses = []
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedercandidates :: ClassEnv -> Ambiguity -> [Le.Type]
75a89d93ae4550e5ed844a999ab3ce2ed40db9bcChristian Maedercandidates _ _ = []
011b7807145efa2af0c7470414a96e0133c26dbcChristian MaederwithDefaults :: Monad m => ([Ambiguity] -> [Le.Type] -> a)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder -> ClassEnv -> [Tyvar] -> [Pred] -> m a
011b7807145efa2af0c7470414a96e0133c26dbcChristian MaederwithDefaults f ce vs ps
011b7807145efa2af0c7470414a96e0133c26dbcChristian Maeder | any null tss = fail "cannot resolve ambiguity"
011b7807145efa2af0c7470414a96e0133c26dbcChristian Maeder | otherwise = return (f vps (map head tss))
011b7807145efa2af0c7470414a96e0133c26dbcChristian Maeder where vps = ambiguities ce vs ps
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder tss = map (candidates ce) vps
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederdefaultedPreds :: Monad m => ClassEnv -> [Tyvar] -> [Pred] -> m [Pred]
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaederdefaultedPreds = withDefaults (\vps _ -> concat (map snd vps))
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder-----------------------------------------------------------------------------
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maedertype Expl = (Id, Scheme, [Alt])
75a89d93ae4550e5ed844a999ab3ce2ed40db9bcChristian MaedertiExpl :: ClassEnv -> [Assump] -> Expl -> TI [Pred]
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaedertiExpl ce as (_, sc, alts)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder = do (qs :=> t) <- freshInst sc
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder ps <- tiAlts ce as alts t
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder s <- getSubst
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder let qs' = apply s qs
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder t' = apply s t
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder fs = tv (apply s as)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder gs = tv t' \\ fs
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder sc' = quantify gs (qs':=>t')
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder ps' = filter (not . entail ce qs') (apply s ps)
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder (ds,rs) <- split ce fs gs ps'
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder if sc /= sc' then
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder fail "signature too general"
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder else if not (null rs) then
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder fail "context too weak"
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder-----------------------------------------------------------------------------
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maedertype Impl = (Id, [Alt])
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maederrestricted :: [Impl] -> Bool
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maederrestricted bs = any simple bs
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder where simple (_, alts) = any (null . fst) alts
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaedertiImpls :: Infer [Impl] [Assump]
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaedertiImpls ce as bs = do ts <- mapM (\_ -> newTVar star) bs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let is = map fst bs
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder scs = map toScheme ts
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder as' = zipWith (:>:) is scs ++ as
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder altss = map snd bs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder pss <- sequence (zipWith (tiAlts ce as') altss ts)
fe021e3e6c51b77d25c48a4c246f73571de1c04dChristian Maeder s <- getSubst
fe021e3e6c51b77d25c48a4c246f73571de1c04dChristian Maeder let ps' = apply s (concat pss)
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder ts' = apply s ts
62fb92b09f732b770317b46a793b60b960d5f481Christian Maeder fs = tv (apply s as)
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder vss = map tv ts'
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder gs = foldr1 union vss \\ fs
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder (ds,rs) <- split ce fs (foldr1 intersect vss) ps'
43a582fe35884e2c6f455e7bfa34f0f4ef8dfe2eChristian Maeder if restricted bs then
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder let gs' = gs \\ tv rs
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder scs' = map (quantify gs' . ([]:=>)) ts'
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder in return (ds++rs, zipWith (:>:) is scs')
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder let scs' = map (quantify gs . (rs:=>)) ts'
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder in return (ds, zipWith (:>:) is scs')
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder-----------------------------------------------------------------------------
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maedertype BindGroup = ([Expl], [[Impl]])
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaedertiBindGroup :: Infer BindGroup [Assump]
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaedertiBindGroup ce as (es,iss) =
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder do let as' = [ v:>:sc | (v,sc,alts) <- es ]
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder (ps, as'') <- tiSeq tiImpls ce (as'++as) iss
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder qss <- mapM (tiExpl ce (as''++as'++as)) es
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder return (ps++concat qss, as''++as')
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian MaedertiSeq :: Infer bg [Assump] -> Infer [bg] [Assump]
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaedertiSeq _ _ _ [] = return ([],[])
2f6227e9ec96ca827cc40078916f18d54a075136Christian MaedertiSeq ti ce as (bs:bss) = do (ps,as') <- ti ce as bs
2f6227e9ec96ca827cc40078916f18d54a075136Christian Maeder (qs,as'') <- tiSeq ti ce (as'++as) bss
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder return (ps++qs, as''++as')
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder-----------------------------------------------------------------------------
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder-- TIProg: Type Inference for Whole Programs
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder-----------------------------------------------------------------------------
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maedertype Program = [BindGroup]
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaedertiProgram :: ClassEnv -> [Assump] -> Program -> [Assump]
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaedertiProgram ce as bgs = runTI $
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder do (ps, as') <- tiSeq tiBindGroup ce as bgs
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder s <- getSubst
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder rs <- reduce ce (apply s ps)
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder return (apply s as')
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder-----------------------------------------------------------------------------