{- Compositional explanation of types and algorithmic debugging of type errors author: Olaf Chitil created: 22.02.2001 Part of the code is derived from Mark Jones' Typing Haskell in Haskell `Typing Haskell in Haskell' is Copyright (c) Mark P Jones, and the Oregon Graduate Institute of Science and Technology, 1999-2000, All rights reserved, and is distributed as free software under the following license. Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: - Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. - Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. - Neither name of the copyright holders nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND THE CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR THE CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -} module Main where import List (nub, (\\), intersect, union, partition) import Maybe (catMaybes,isNothing) import Char (isAlpha,digitToInt) import Monad (MonadPlus(..),msum,when) -- import Debug.Trace (trace) ----------------------------------------------------------------------------- -- Conversion to String: ----------------------------------------------------------------------------- maxIdLength :: Int maxIdLength = 15 subWidth :: Int subWidth = 30 fixWidth :: String -> String fixWidth s | l < subWidth = s ++ replicate (subWidth-l) ' ' | otherwise = take (subWidth-6) s ++ " ... " where l = length s test :: Bool -> String -> String test b s = if b then s else "" pparens :: Bool -> String -> String pparens True x = '(': x ++ ")" pparens False x = x ppContext :: Int -> [Pred] -> String ppContext _ [] = "" ppContext n preds = "\nContext:" ++ replicate n ' ' ++ ppPreds preds ppStep :: Bool {- with fragment -} -> Bool {- with children -} -> Typing -> [Typing] -> String ppStep f c tyg tygs = (if not f && not c then ppSTyping tyg else ppTyping f tyg) ++ test (c && (not . null $ tygs)) ("\n because" ++ ppTypings f tygs) ppTypings :: Bool {- with fragment -} -> [Typing] -> String ppTypings _ tygs@(TyExpr _ _ : _) = test qual ("\nContext: " ++ concatMap (fixWidth . ppPreds . preds) tygs) ++ "\nExpression: " ++ concatMap (fixWidth . ppExpr False . exp) tygs ++ "\nType: " ++ concatMap (fixWidth . ppType False . ty) tygs ++ ppMonoEnvs 5 (map env tygs) where exp (TyExpr e _) = e preds (TyExpr _ (p :=> _)) = p ty (TyExpr _ (_ :=> (_,t))) = t env (TyExpr _ (_ :=> (e,_))) = e qual = not . null . concatMap preds $ tygs ppTypings f tygs@(TyAlt _ _ : _) = test f ("\nEquation: " ++ concatMap (fixWidth . ppAlt . alt) tygs) ++ test qual ("\nContext: " ++ concatMap (fixWidth . ppPreds . preds) tygs) ++ ppMonoEnvs 4 (map env tygs) where alt (TyAlt a _) = a preds (TyAlt _ (p :=> _)) = p env (TyAlt _ (_ :=> e)) = e qual = not . null . concatMap preds $ tygs ppTypings f tygs@(TyDef _ _ : _) = test f ("\nDefinition: " ++ concatMap (fixWidth . ppDef . def) tygs) ++ test qual ("\nContext: " ++ concatMap (fixWidth . ppPreds . preds) tygs) ++ ppMonoEnvs 5 (map env tygs) where def (TyDef a _) = a preds (TyDef _ (p :=> _)) = p env (TyDef _ (_ :=> e)) = e qual = not . null . concatMap preds $ tygs ppTypings f tygs@(TyBindGroup _ _ : _) = test f ("\nDefinitions: " ++ concatMap (fixWidth . ppBindGroup . bg) tygs) ++ test qual ("\nContext: " ++ concatMap (fixWidth . ppPreds . preds) tygs) ++ ppPolyEnvs 8 (map penv tygs) ++ ppMonoEnvs 8 (map env tygs) where bg (TyBindGroup b _) = b preds (TyBindGroup _ (p :=> _)) = p env (TyBindGroup _ (_ :=> (e,_))) = e penv (TyBindGroup _ (_ :=> (_,p))) = p qual = not . null . concatMap preds $ tygs ppTypings _ _ = error "ppTypings" ppEnv2 :: Int -> Int -> Int -> [(String,String)] -> String ppEnv2 l ind _ xs = concatMap line xs where line (i,t) = '\n' : replicate ind ' ' ++ fixLength l i ++ " " ++ t ppMonoEnvs :: Int -> [MonoEnv] -> String ppMonoEnvs l envs | all null envs = "" | otherwise = "\nwith " ++ drop 6 (ppEnv2 l 5 maxIdLength (map line ids)) where ids = foldr union [] . map dom $ envs line i = (i,concatMap (fixWidth . ppMType i) envs) ppMType i env = case find i env of Just ty -> ppType False ty Nothing -> "" ppPolyEnvs :: Int -> [PolyEnv] -> String ppPolyEnvs l envs | all null envs = "" | otherwise = "\nDefining " ++ drop 10 (ppEnv2 l 9 maxIdLength (map line ids)) where ids = foldr union [] . map dom $ envs line i = (i,concatMap (fixWidth . ppMType i) envs) ppMType i env = case find i env of Just (Tree (TyPolyVar polyTy) _) -> ppPolyType polyTy Nothing -> "" ppSContextS :: [Pred] -> String ppSContextS preds = test (not . null $ preds) (ppPreds preds ++ " =>") ppSTyping :: Typing -> String ppSTyping (TyExpr expr (preds :=> (monoEnv,ty))) = ppSContextS preds ++ "\n" ++ fixLength l e ++ " :: " ++ ppType False ty ++ ppSMonoEnv l monoEnv where l = 10 `max` length e e = ppExpr False expr ppSTyping (TyAlt _ (preds :=> monoEnv)) = ppSContextS preds ++ ppSMonoEnv 10 monoEnv ppSTyping (TyDef _ (preds :=> monoEnv)) = ppSContextS preds ++ ppSMonoEnv 10 monoEnv ppSTyping (TyBindGroup _ (preds :=> (monoEnv,polyEnv))) = ppSContextS preds ++ ppSPolyEnv 10 polyEnv ++ ppSMonoEnv 10 monoEnv ppSTyping tyg = ppTyping False tyg ppTyping :: Bool {- with fragment -} -> Typing -> String ppTyping _ (TyExpr expr (preds :=> (monoEnv,ty))) = ppContext 4 preds ++ "\nExpression: " ++ ppExpr False expr ++ "\nType: " ++ ppType False ty ++ ppMonoEnv monoEnv ppTyping f (TyAlt alt (preds :=> monoEnv)) = test f ("\nEquation: " ++ ppAlt alt) ++ ppContext 2 preds ++ ppMonoEnv monoEnv ppTyping f (TyDef def (preds :=> monoEnv)) = test f ("\nDefinition: " ++ ppDef def) ++ ppContext 4 preds ++ ppMonoEnv monoEnv ppTyping f (TyBindGroup bg (preds :=> (monoEnv,polyEnv))) = test f ("\nDefinitions: " ++ ppBindGroup bg) ++ ppContext 5 preds ++ ppPolyEnv polyEnv ++ ppMonoEnv monoEnv ppTyping f (TyProgram _ polyEnv) = "\nWhole Program" ++ test f (ppPolyEnv polyEnv) ppTyping _ (TyPolyVar (preds :=> (monoEnv,t))) = "\nPolyVar: " ++ ppContext 1 preds ++ "\nType: " ++ ppType False t ++ ppMonoEnv monoEnv ppTyping _ (TyUExpr msg expr) = "\nError: " ++ msg ++ ("\nin expression: " ++ ppExpr False expr) ppTyping _ (TyUAlt msg alt) = "\nError: " ++ msg ++ ("\nin equation: " ++ ppAlt alt) ppTyping _ (TyUDef msg def) = "\nError: " ++ msg ++ ("\nin definition: " ++ ppDef def) ppTyping _ (TyUBindGroup msg bg) = "\nError: " ++ msg ++ ("\nin definitions: " ++ ppBindGroup bg) ppTyping _ (TyUProgram msg _) = "\nError: " ++ msg ++ ("\nin whole program.") ppKind :: Bool -> Kind -> String ppKind _ Star = "*" ppKind b (Kfun k1 k2) = pparens b (ppKind (not b) k1 ++ "->" ++ ppKind False k2) ppPreds :: [Pred] -> String ppPreds [] = "" ppPreds preds = foldr1 (\x xs -> x ++ ", " ++ xs) . map ppPred $ preds ppPred :: Pred -> String ppPred (IsIn classId ty) = classId ++ " " ++ ppType True ty ppType :: Bool -> Type -> String ppType _ (TVar (Tyvar i _)) = i ppType _ (TCon (Tycon i _)) = i ppType _ (TAp (TCon (Tycon "[]" _)) t) = '[' : ppType False t ++ "]" ppType b (TAp (TAp (TCon (Tycon "(->)" _)) t1) t2) = pparens b $ ppType (not b) t1 ++ "->" ++ ppType False t2 ppType b (TAp t1 t2) = pparens b $ ppType True t1 ++ ' ' : ppType True t2 ppType _ (TGen n) = show n ppPolyType :: Qual (MonoEnv,Type) -> String ppPolyType (preds :=> (monoEnv,t)) = test (not . null $ preds) (ppPreds preds ++ " => ") ++ ppType False t ++ test (not . null $ monoEnv) (" | " ++ (foldr1 (\t s -> t ++ ", " ++ s) . map (\(i :>: t) -> i ++ " :: " ++ ppType False t) $ monoEnv)) ppSPolyEnv :: Int -> PolyEnv -> String ppSPolyEnv l env = ppSEnv l (map pair env) where pair (i :>: Tree (TyPolyVar polyTy) _) = (i,ppPolyType polyTy) ppPolyEnv :: PolyEnv -> String ppPolyEnv env = "\nDefining " ++ drop 10 (ppEnv 9 maxIdLength (map pair env)) where pair (i :>: Tree (TyPolyVar polyTy) _) = (i,ppPolyType polyTy) ppSMonoEnv :: Int -> MonoEnv -> String ppSMonoEnv l env = ppSEnv l (map pair env) where pair (i :>: t) = (i,ppType False t) ppMonoEnv :: MonoEnv -> String ppMonoEnv env | null env = "" | otherwise = "\nwith " ++ drop 6 (ppEnv 5 maxIdLength (map pair env)) where pair (i :>: t) = (i,ppType False t) ppSEnv :: Int -> [(String,String)] -> String ppSEnv l xs = concatMap line xs where line (i,t) = '\n' : fixLength l i ++ " :: " ++ t ppEnv :: Int -> Int -> [(String,String)] -> String ppEnv ind idl xs = concatMap line xs where line (i,t) = '\n' : replicate ind ' ' ++ fixLength l i ++ " " ++ t l = idl `min` (foldr max 0 . map length . map fst $ xs) fixLength :: Int -> String -> String fixLength l xs | l > length xs = xs ++ replicate (l - length xs) ' ' | otherwise = take l xs ppLiteral :: Literal -> String ppLiteral (LitInt i) = show i ppLiteral (LitChar c) = [c] ppExpr :: Bool -> Expr -> String ppExpr _ (Var i) | not (isAlpha (head i)) = '(' : i ++ ")" ppExpr _ (Var i) = i ppExpr _ (Lit l) = ppLiteral l ppExpr _ (Const i) | not (isAlpha (head i)) && head i /= '[' && head i /= '(' = '(' : i ++ ")" ppExpr _ (Const i) = i ppExpr b (Ap (Ap (Const i) e1) e2) | not (isAlpha (head i)) = pparens b $ ppExpr True e1 ++ ' ' : i ++ ' ' : ppExpr True e2 ppExpr b (Ap (Ap (Var i) e1) e2) | not (isAlpha (head i)) = pparens b $ ppExpr True e1 ++ ' ' : i ++ ' ' : ppExpr True e2 ppExpr b (Ap e1 e2) = pparens b $ ppExpr True e1 ++ ' ' : ppExpr True e2 ppAlt :: Alt -> String ppAlt (e1,e2) = ppExpr False e1 ++ " = " ++ ppExpr False e2 ppDef :: Def -> String ppDef (alt:_) = ppAlt alt ++ " ..." ppBindGroup :: BindGroup -> String ppBindGroup (BG defs) = concatMap showVar boundVars where showVar i = i ++ " " boundVars = nub . concatMap defVars $ defs ppProgram :: Program -> String ppProgram prog = concatMap ppBindGroup prog ppDef2 :: Def -> String ppDef2 alts = concatMap (('\n':) . ppAlt) alts ppBindGroup2 :: BindGroup -> String ppBindGroup2 (BG defs) = concatMap (('\n':) . ppDef2) defs ppProgram2 :: Program -> String ppProgram2 prog = concatMap ppBindGroup2 prog ----------------------------------------------------------------------------- -- Tree: ----------------------------------------------------------------------------- data Tree a = Tree a [Tree a] instance Types a => Types (Tree a) where -- work only on root element apply s (Tree e ts) = Tree (apply s e) ts tv (Tree s _) = tv s data TreeCont a = Empty | TreeCont a [Tree a] (TreeCont a) [Tree a] treeElem :: Tree a -> a treeElem (Tree e _) = e -- dirty trick: instance Eq a => Eq (Tree a) where Tree x _ == Tree y _ = x == y instance Eq (TreeCont a) where _ == _ = True type TreePos a = (Tree a,TreeCont a) -- produce all children TreePoss children :: TreePos a -> [TreePos a] children (Tree x ts,cont) = map pick [0..(length ts - 1)] where pick n = (t,TreeCont x lts cont rts) where (lts,t:rts) = splitAt n ts -- parent and sibling TreePoss parentSibs :: TreePos a -> ([TreePos a],Maybe (TreePos a),[TreePos a]) parentSibs (_,Empty) = ([],Nothing,[]) parentSibs (t,TreeCont x lts cont rts) = (map (build . addRts) . splits $ lts ,Just (Tree x (lts++t:rts),cont) ,map (build . addLts) . splits $ rts) where splits :: [a] -> [([a],a,[a])] splits [] = [] splits (z:zs) = ([],z,zs) : map (\(us,v,ws)->(z:us,v,ws)) (splits zs) addRts (ys,v,ws) = (ys,v,ws++t:rts) addLts (ys,v,ws) = (lts++t:ys,v,ws) build (ys,v,ws) = (v,TreeCont x ys cont ws) printStep :: Bool {- with fragment -} -> Bool {- with children -} -> Bool {- only show poly vars -} -> TreePos Typing -> IO () printStep f c v tp@((Tree e _),_) = do putStrLn $ ppStep f c (rename e) (map (rename . (\(Tree tyg _,_) -> tyg)) children) where children = getChildren v tp walkTree :: Tree Typing -> IO () walkTree tree = walk True True True [] [] (tree,Empty) walk :: Bool {- with fragment -} -> Bool {- with children -} -> Bool {- only show poly vars -} -> Oracle -> [(Oracle,TreePos Typing)] -> TreePos Typing -> IO () walk f c v oracle history tp@((Tree e _),_) = do putStr "\n" when errorLocated (putStr (if v then "\nERROR LOCATED! Wrong definition of:" else "\nERROR LOCATED! Wrong program fragment:")) printStep f c v tp if errorLocated && v then do putStr "\nSwitch to detailed level of program fragments." walk f c False oracle ((oracle,tp):history) (algNo False oracle tp) else do putStr (if f || c then "> " else "Is(are) intended type(s) an instance? (y/n) ") choose where errorLocated = sourceOfError v oracle tp children = getChildren v tp choose = do i <- getChar case i of '?' -> do putStrLn $ "\nManual navigation:" ++ "\nu - up\nd - down\nl - left\nr - right" ++ "\nb - back (undo)\ns - start" ++ "\nnAlgorithmic debugging:" ++ "\ny - intended type is an instance" ++ "\nn - intended type is not an instance" ++ "\nY - not sure about instance, continue as if it is" ++ "\nN - not sure about instance, continue as if it is not" ++ "\na - amnesia; forget all y/n answers" ++ "\nnToggles:\nf - (don't) show program fragment" ++ "\nc - (don't) show children" ++ "\nv - show only polymorphic variables" ++ "\n\nq - quit" walk f c v oracle history tp 'b' -> if null history then walk f c v oracle history tp else walk f c v oracle' history' tp' where (oracle',tp'):history' = history 's' -> if null history then walk f c v oracle history tp else walk f c v oracle' [] tp' where (oracle',tp') = last history 'f' -> do putStrLn (if f then "\nDon't show program fragment." else "\nShow program fragment.") walk (not f) c v oracle history tp 'c' -> do putStrLn (if c then "\nDon't show children." else "\nShow children.") walk f (not c) v oracle history tp 'v' -> do putStrLn (if v then "\nShow all typings." else "\nShow only typings of polymorphic variables.") walk f c (not v) oracle history tp 'q' -> return () 'u' -> ifPossible $ goUp v tp 'd' -> ifPossible $ goDown v tp 'l' -> ifPossible $ goLeft v tp 'r' -> ifPossible $ goRight v tp 'y' -> let oracle' = addToOracle (e,True) oracle in walk f c v oracle' ((oracle',tp):history) (algYes v oracle' tp) 'n' -> let oracle' = addToOracle (e,False) oracle in walk f c v oracle' ((oracle',tp):history) (algNo v oracle' tp) 'Y' -> walk f c v oracle ((oracle,tp):history) (algYes v oracle tp) 'N' -> walk f c v oracle ((oracle,tp):history) (algNo v oracle tp) 'a' -> do putStrLn "\nAmnesia: forget all y/n answers." walk f c v [] history tp _ -> let n = digitToInt i in if i >= '1' && i <= '9' && n <= length children then walk f c v oracle ((oracle,tp):history) (children!!(n-1)) else choose ifPossible :: Maybe (TreePos Typing) -> IO () ifPossible (Just tp') = walk f c v oracle ((oracle,tp):history) tp' ifPossible Nothing = choose getChildren :: Bool {- only polyvars -} -> TreePos Typing -> [TreePos Typing] getChildren True = polyChildren getChildren False = children goLeft :: Bool {- only polyvars -} -> TreePos Typing -> Maybe (TreePos Typing) goLeft True tp = polyLeft tp goLeft False (t,TreeCont ec (l@(_:_)) cont' r) = Just (last l,TreeCont ec (init l) cont' (t:r)) goLeft _ _ = Nothing goRight :: Bool {- only polyvars -} -> TreePos Typing -> Maybe (TreePos Typing) goRight True tp = polyRight tp goRight False (t,TreeCont ec l cont' (t':ts')) = Just (t',TreeCont ec (l++[t]) cont' ts') goRight _ _ = Nothing goDown :: Bool {- only polyvars -} -> TreePos Typing -> Maybe (TreePos Typing) goDown True tp = polyDown tp goDown False (Tree e (t:ts),cont) = Just (t,TreeCont e [] cont ts) goDown _ _ = Nothing goUp :: Bool {- only polyvars -} -> TreePos Typing -> Maybe (TreePos Typing) goUp True tp = polyUp tp goUp False (t,TreeCont ec left contcont right) = Just (Tree ec (left++[t]++right), contcont) goUp _ _ = Nothing goNotTrueChild :: Bool {- only polyvars -} -> Oracle -> TreePos Typing -> Maybe (TreePos Typing) goNotTrueChild v oracle tp = if null notTrue then Nothing else Just (head notTrue) where children = getChildren v tp notTrue = filter (\tp -> lookupOracle tp oracle /= Just True) children algNo :: Bool {- only polyvars -} -> Oracle -> TreePos Typing -> TreePos Typing algNo v oracle tp = case goNotTrueChild v oracle tp of Just tp' -> algNext v oracle tp' Nothing -> tp algYes :: Bool {- only polyvars -} -> Oracle -> TreePos Typing -> TreePos Typing algYes v oracle tp = case goRight v tp of Just tp' -> algNext v oracle tp' Nothing -> case goUp v tp of Just tp' -> algNext v oracle tp' Nothing -> error "altNext: impossible" algNext :: Bool {- only polyvars -} -> Oracle -> TreePos Typing -> TreePos Typing algNext v oracle tp = case lookupOracle tp oracle of Nothing -> tp Just True -> algYes v oracle tp Just False -> algNo v oracle tp sourceOfError :: Bool {- only polyvars -} -> Oracle -> TreePos Typing -> Bool sourceOfError v oracle tp = lookupOracle tp oracle == Just False && isNothing (goNotTrueChild v oracle tp) ----------------------------------------------------------------------------- -- Oracle: ----------------------------------------------------------------------------- type Oracle = [(Typing,Bool)] -- answers to y/n questions addToOracle :: (Typing,Bool) -> Oracle -> Oracle addToOracle (tyg,b) oracle = (tyg,b):oracle lookupOracle :: TreePos Typing -> Oracle -> Maybe Bool lookupOracle (Tree (TyExpr (Var _) _) [],_) _ = Just True -- simple var lookupOracle (Tree tyg _,_) oracle | untypable tyg = Just False | otherwise = lookup tyg oracle ----------------------------------------------------------------------------- -- Polymorphic variable children: ----------------------------------------------------------------------------- polySelfChildren ::TreePos Typing -> [TreePos Typing] polySelfChildren = go . (:[]) polyChildren :: TreePos Typing -> [TreePos Typing] polyChildren = go . children -- recursively search for poly vars go :: [TreePos Typing] -> [TreePos Typing] go [] = [] go (tp@(Tree (TyExpr (Var _) _) (_:_),_) : tps) = tp : go tps go (tp : tps) = go (children tp ++ go tps) polyParentSibs :: TreePos Typing -> ([TreePos Typing],Maybe (TreePos Typing),[TreePos Typing]) polyParentSibs tp = case mtp of Nothing -> ps Just (Tree (TyExpr (Var _) _) (_:_),_) -> ps Just (Tree tyg _,_) | untypable tyg -> ps Just tp' -> let (ltps',mtp',rtps') = polyParentSibs tp' in (ltps'++ltps,mtp',rtps++rtps') where ps@(ltps,mtp,rtps) = parentSibs tp polyUp :: TreePos Typing -> Maybe (TreePos Typing) polyUp tp = mtp where (_,mtp,_) = polyParentSibs tp polyDown :: TreePos Typing -> Maybe (TreePos Typing) polyDown tp = if null tps then Nothing else Just (head tps) where tps = polyChildren tp polyLeft :: TreePos Typing -> Maybe (TreePos Typing) polyLeft tp = if null polyLtps then Nothing else Just (last polyLtps) where polyLtps = concatMap polySelfChildren ltps (ltps,_,_) = polyParentSibs tp polyRight :: TreePos Typing -> Maybe (TreePos Typing) polyRight tp = if null polyRtps then Nothing else Just (head polyRtps) where polyRtps = concatMap polySelfChildren rtps (_,_,rtps) = polyParentSibs tp ----------------------------------------------------------------------------- -- Derivation: ----------------------------------------------------------------------------- data Typing = TyExpr Expr (Qual (MonoEnv,Type)) | TyAlt Alt (Qual MonoEnv) | TyDef Def (Qual MonoEnv) | TyBindGroup BindGroup (Qual (MonoEnv, PolyEnv)) | TyPolyVar (Qual (MonoEnv,Type)) | TyProgram Program PolyEnv | TyUExpr String Expr -- String is error message | TyUAlt String Alt | TyUDef String Def | TyUBindGroup String BindGroup | TyUProgram String Program instance Eq Typing where TyExpr e1 q1 == TyExpr e2 q2 = e1 == e2 && q1 == q2 TyAlt _ m1 == TyAlt _ m2 = m1 == m2 TyDef _ m1 == TyDef _ m2 = m1 == m2 TyAlt _ m1 == TyDef _ m2 = m1 == m2 TyDef _ m1 == TyAlt _ m2 = m1 == m2 TyBindGroup _ q1 == TyBindGroup _ q2 = q1 == q2 TyPolyVar q1 == TyPolyVar q2 = q1 == q2 TyProgram _ e1 == TyProgram _ e2 = e1 == e2 TyUExpr s1 e1 == TyUExpr s2 e2 = s1 == s2 && e1 == e2 TyUAlt s1 e1 == TyUAlt s2 e2 = s1 == s2 && e1 == e2 TyUDef s1 e1 == TyUDef s2 e2 = s1 == s2 && e1 == e2 TyUBindGroup s1 e1 == TyUBindGroup s2 e2 = s1 == s2 && e1 == e2 TyUProgram s1 e1 == TyUProgram s2 e2 = s1 == s2 && e1 == e2 _ == _ = False instance Types Typing where apply s (TyExpr e qEnvTy) = TyExpr e (apply s qEnvTy) apply s (TyAlt alt qEnv) = TyAlt alt (apply s qEnv) apply s (TyDef def qEnv) = TyDef def (apply s qEnv) apply s (TyBindGroup bg qEnvPolyEnv) = TyBindGroup bg (apply s qEnvPolyEnv) apply s (TyPolyVar qEnvTy) = TyPolyVar (apply s qEnvTy) apply s (TyProgram prog qEnvPolyEnv) = TyProgram prog (apply s qEnvPolyEnv) apply _ other = other tv (TyExpr _ qEnvTy) = tv qEnvTy tv (TyAlt _ qEnv) = tv qEnv tv (TyDef _ qEnv) = tv qEnv tv (TyBindGroup _ qEnvPolyEnv) = tv qEnvPolyEnv tv (TyPolyVar qEnvTy) = tv qEnvTy tv (TyProgram _ qEnvPolyEnv) = tv qEnvPolyEnv tv _ = [] rename :: Types t => t -> t {- Rename all free type variables to a,b,c,... -} rename ty = apply freeSubst ty where freeTyVars = tv ty freeKinds = map kind freeTyVars newTyVars = map TVar $ zipWith Tyvar (map (:[]) ['a'..]) freeKinds freeSubst = zip freeTyVars newTyVars untypable :: Typing -> Bool untypable (TyUExpr _ _) = True untypable (TyUAlt _ _) = True untypable (TyUDef _ _) = True untypable (TyUBindGroup _ _) = True untypable (TyUProgram _ _) = True untypable _ = False type Derivation = Tree Typing ----------------------------------------------------------------------------- -- Id: Error Monad ----------------------------------------------------------------------------- data Error a = Correct a | Wrong String instance Monad Error where return = Correct (Correct a) >>= f = f a (Wrong s) >>= _ = Wrong s fail = Wrong instance MonadPlus Error where mzero = Wrong "mzero" (Wrong _) `mplus` y = y x `mplus` _ = x error2TI :: Error a -> TI String a error2TI (Correct x) = return x error2TI (Wrong msg) = errorMsg msg ----------------------------------------------------------------------------- -- Id: Identifiers ----------------------------------------------------------------------------- type Id = String enumId :: Int -> Id enumId n = "v" ++ show n ----------------------------------------------------------------------------- -- Kind: Kinds ----------------------------------------------------------------------------- data Kind = Star | Kfun Kind Kind deriving (Eq,Show) ----------------------------------------------------------------------------- -- Type: Types ----------------------------------------------------------------------------- data Type = TVar Tyvar | TCon Tycon | TAp Type Type | TGen Int deriving (Eq,Show) data Tyvar = Tyvar Id Kind deriving (Eq,Show) data Tycon = Tycon Id Kind deriving (Eq,Show) tUnit :: Type tUnit = TCon (Tycon "()" Star) tChar :: Type tChar = TCon (Tycon "Char" Star) tInt :: Type tInt = TCon (Tycon "Int" Star) tInteger :: Type tInteger = TCon (Tycon "Integer" Star) tFloat :: Type tFloat = TCon (Tycon "Float" Star) tDouble :: Type tDouble = TCon (Tycon "Double" Star) tList :: Type tList = TCon (Tycon "[]" (Kfun Star Star)) tArrow :: Type tArrow = TCon (Tycon "(->)" (Kfun Star (Kfun Star Star))) tTuple2 :: Type tTuple2 = TCon (Tycon "(,)" (Kfun Star (Kfun Star Star))) tString :: Type tString = list tChar infixr 4 `fn` fn :: Type -> Type -> Type a `fn` b = TAp (TAp tArrow a) b list :: Type -> Type list t = TAp tList t pair :: Type -> Type -> Type pair a b = TAp (TAp tTuple2 a) b class HasKind t where kind :: t -> Kind instance HasKind Tyvar where kind (Tyvar _ k) = k instance HasKind Tycon where kind (Tycon _ k) = k instance HasKind Type where kind (TCon tc) = kind tc kind (TVar u) = kind u kind (TAp t _) = case (kind t) of (Kfun _ k) -> k ----------------------------------------------------------------------------- -- Subst: Substitutions ----------------------------------------------------------------------------- type Subst = [(Tyvar, Type)] nullSubst :: Subst nullSubst = [] (+->) :: Tyvar -> Type -> Subst u +-> t = [(u, t)] class Types t where apply :: Subst -> t -> t tv :: t -> [Tyvar] instance Types Type where apply s (TVar u) = case lookup u s of Just t -> t Nothing -> TVar u apply s (TAp l r) = TAp (apply s l) (apply s r) apply _ t = t tv (TVar u) = [u] tv (TAp l r) = tv l `union` tv r tv _ = [] instance Types a => Types [a] where apply s = map (apply s) tv = nub . concat . map tv instance (Types a, Types b) => Types (a,b) where apply s (x,y) = (apply s x, apply s y) tv (x,y) = nub (tv x ++ tv y) infixr 4 @@ (@@) :: Subst -> Subst -> Subst s1 @@ s2 = [ (u, apply s1 t) | (u,t) <- s2 ] ++ s1 merge :: Monad m => Subst -> Subst -> m Subst merge s1 s2 = if agree then return (s1++s2) else fail "merge fails" where agree = all (\v -> apply s1 (TVar v) == apply s2 (TVar v)) (map fst s1 `intersect` map fst s2) ----------------------------------------------------------------------------- -- Unify: Unification ----------------------------------------------------------------------------- mgu :: Monad m => Type -> Type -> m Subst varBind :: Monad m => Tyvar -> Type -> m Subst mgu (TAp l r) (TAp l' r') = do s1 <- mgu l l' s2 <- mgu (apply s1 r) (apply s1 r') return (s2 @@ s1) mgu (TVar u) t = varBind u t mgu t (TVar u) = varBind u t mgu (TCon tc1) (TCon tc2) | tc1==tc2 = return nullSubst mgu (TGen x) (TGen y) = if x /= y then error "TGen" else return nullSubst mgu _ _ = fail "different type constructors cannot be unified" varBind u t | t == TVar u = return nullSubst | u `elem` tv t = fail "unification would lead to infinite type" | kind u == kind t = return (u +-> t) | otherwise = fail "kinds of types do not agree" match :: Monad m => Type -> Type -> m Subst match (TAp l r) (TAp l' r') = do sl <- match l l' sr <- match r r' merge sl sr match (TVar u) t | kind u == kind t = return (u +-> t) match (TCon tc1) (TCon tc2) | tc1==tc2 = return nullSubst match _ _ = fail "types do not match" multiAssumptionEnv :: [MonoEnv] -> Env [Type] multiAssumptionEnv ass = let vars = nub . concatMap dom $ ass in map combineTypes vars where combineTypes :: Id -> Assump [Type] combineTypes i = let scs = catMaybes . map (find i) $ ass in i :>: scs unifyMonoEnvs :: [Qual MonoEnv] -> Error (Qual MonoEnv) unifyMonoEnvs qEnvs = do (env,s) <- unifyMonoEnvs' envs return ((nub . apply s . concat $ contexts) :=> env) where (contexts,envs) = unzip . map (\(pred :=> env)->(pred,env)) $ qEnvs unifyMonoEnvs' :: [MonoEnv] -> Error (MonoEnv,Subst) unifyMonoEnvs' ass = unifyMultiAssumptionEnv (multiAssumptionEnv ass) unifyMultiAssumptionEnv :: Env [Type] -> Error (MonoEnv,Subst) unifyMultiAssumptionEnv [] = return ([],nullSubst) unifyMultiAssumptionEnv ((i :>: scs) : as) = do (sc,s) <- unifyTypes scs (as',s') <- unifyMultiAssumptionEnv (apply s as) return (apply s' (i :>: sc) : as',s'@@s) unifyTypings :: [Qual (MonoEnv,Type)] -> Error (Qual (MonoEnv,Type)) unifyTypings qEnvTys = do (t,s) <- unifyTypes ts (monoEnv,s2) <- unifyMonoEnvs' (apply s monoEnvs) return ((nub . apply (s2@@s) $ concat contexts) :=> (monoEnv,apply s2 t)) where (contexts,monoEnvs,ts) = unzip3 . map (\(preds :=> (monoEnv,ty)) -> (preds,monoEnv,ty)) $ qEnvTys unify2Types :: Type -> Type -> Error (Type,Subst) unify2Types t1 t2 = do unifier <- mgu t1 t2 return (apply unifier t1,unifier) unifyTypes :: [Type] -> Error (Type,Subst) unifyTypes = unifySeq unify2Types unifySeq :: Types a => (a -> a -> Error (a,Subst)) -> [a] -> Error (a,Subst) unifySeq _ [] = error "unifySeq of empty list" unifySeq _ [x] = return (x,nullSubst) unifySeq unify (x:y:ys) = do (z,s) <- unify x y (z',s') <- unifySeq unify (z : map (apply s) ys) return (z',s'@@s) ----------------------------------------------------------------------------- -- Pred: Predicates ----------------------------------------------------------------------------- data Qual t = [Pred] :=> t deriving Eq data Pred = IsIn Id Type deriving Eq type Context = [Pred] instance Types t => Types (Qual t) where apply s (ps :=> t) = apply s ps :=> apply s t tv (ps :=> t) = tv ps `union` tv t instance Types Pred where apply s (IsIn c t) = IsIn c (apply s t) tv (IsIn _ t) = tv t mguPred, matchPred :: Monad m => Pred -> Pred -> m Subst mguPred = lift mgu matchPred = lift match lift :: Monad m => (Type -> Type -> m a) -> Pred -> Pred -> m a lift m (IsIn i t) (IsIn i' t') | i == i' = m t t' | otherwise = fail "classes differ" type Class = ([Id], [Inst]) -- superclasses and instances type Inst = Qual Pred ----------------------------------------------------------------------------- data ClassEnv = ClassEnv { classes :: Id -> Error Class, defaults :: [Type] } super :: ClassEnv -> Id -> [Id] super ce i = case classes ce i of Correct (is, _) -> is insts :: ClassEnv -> Id -> [Inst] insts ce i = case classes ce i of Correct (_, its) -> its correct :: Error a -> Bool correct (Correct _) = True correct (Wrong _) = False modify :: ClassEnv -> Id -> Class -> ClassEnv modify ce i c = ce{classes = \j -> if i==j then return c else classes ce j} initialEnv :: ClassEnv initialEnv = ClassEnv { classes = \_ -> fail "class not defined", defaults = [tInteger, tDouble] } type EnvTransformer = ClassEnv -> Error ClassEnv infixr 5 <:> (<:>) :: EnvTransformer -> EnvTransformer -> EnvTransformer f <:> g = \ce -> do ce' <- f ce g ce' addClass :: Id -> [Id] -> EnvTransformer addClass i is ce | correct (classes ce i) = fail "class already defined" | any (not . correct . classes ce) is = fail "superclass not defined" | otherwise = return (modify ce i (is, [])) addPreludeClasses :: EnvTransformer addPreludeClasses = addCoreClasses <:> addNumClasses addCoreClasses :: EnvTransformer addCoreClasses = addClass "Eq" [] <:> addClass "Ord" ["Eq"] <:> addClass "Show" [] <:> addClass "Read" [] <:> addClass "Bounded" [] <:> addClass "Enum" [] <:> addClass "Functor" [] <:> addClass "Monad" [] addNumClasses :: EnvTransformer addNumClasses = addClass "Num" ["Eq", "Show"] <:> addClass "Real" ["Num", "Ord"] <:> addClass "Fractional" ["Num"] <:> addClass "Integral" ["Real", "Enum"] <:> addClass "RealFrac" ["Real", "Fractional"] <:> addClass "Floating" ["Fractional"] <:> addClass "RealFloat" ["RealFrac", "Floating"] addInst :: [Pred] -> Pred -> EnvTransformer addInst ps p@(IsIn i _) ce | not (correct (classes ce i)) = fail "no class for instance" | any (overlap p) qs = fail "overlapping instance" | otherwise = return (modify ce i c) where its = insts ce i qs = [ q | (_ :=> q) <- its ] c = (super ce i, (ps:=>p) : its) overlap :: Pred -> Pred -> Bool overlap p q = correct (mguPred p q) exampleInsts :: EnvTransformer exampleInsts = addPreludeClasses <:> addInst [] (IsIn "Ord" tUnit) <:> addInst [] (IsIn "Ord" tChar) <:> addInst [] (IsIn "Ord" tInt) <:> addInst [IsIn "Ord" (TVar (Tyvar "a" Star)), IsIn "Ord" (TVar (Tyvar "b" Star))] (IsIn "Ord" (pair (TVar (Tyvar "a" Star)) (TVar (Tyvar "b" Star)))) ----------------------------------------------------------------------------- bySuper :: ClassEnv -> Pred -> [Pred] bySuper ce p@(IsIn i t) = p : concat [ bySuper ce (IsIn i' t) | i' <- super ce i ] byInst :: MonadPlus m => ClassEnv -> Pred -> m [Pred] byInst ce p@(IsIn i _) = msum [ tryInst it | it <- insts ce i ] where tryInst (ps :=> h) = do u <- matchPred h p return (map (apply u) ps) entail :: ClassEnv -> [Pred] -> Pred -> Bool entail ce ps p = any (p `elem`) (map (bySuper ce) ps) || case byInst ce p of Wrong _ -> False Correct qs -> all (entail ce ps) qs ----------------------------------------------------------------------------- inHnf :: Pred -> Bool inHnf (IsIn _ t) = hnf t where hnf (TVar _) = True hnf (TCon _) = False hnf (TAp t _) = hnf t toHnfs :: Monad m => ClassEnv -> [Pred] -> m [Pred] toHnfs ce ps = do pss <- mapM (toHnf ce) ps return (concat pss) toHnf :: Monad m => ClassEnv -> Pred -> m [Pred] toHnf ce p | inHnf p = return [p] | otherwise = case byInst ce p of Nothing -> fail "context reduction" Just ps -> toHnfs ce ps simplify :: ClassEnv -> [Pred] -> [Pred] simplify ce = loop [] where loop rs [] = rs loop rs (p:ps) | entail ce (rs++ps) p = loop rs ps | otherwise = loop (p:rs) ps reduce :: [Pred] -> TI String [Pred] reduce ps = do ce <- getClassEnv qs <- error2TI $ toHnfs ce ps return (simplify ce qs) scEntail :: ClassEnv -> [Pred] -> Pred -> Bool scEntail ce ps p = any (p `elem`) (map (bySuper ce) ps) ----------------------------------------------------------------------------- -- Environments: ----------------------------------------------------------------------------- data Assump t = Id :>: t deriving (Eq,Show) type Env t = [Assump t] type MonoEnv = Env Type type PolyEnv = Env Derivation instance Types t => Types (Assump t) where apply s (i :>: sc) = i :>: (apply s sc) tv (_ :>: sc) = tv sc dom :: Env t -> [Id] dom as = [ i | (i :>: _) <- as] without :: Env t -> [Id] -> Env t without as is = [ a | a@(i:>:_) <- as, i `notElem` is] find :: Id -> Env t -> Maybe t find i as = headMaybe [ sc | (i':>:sc) <- as, i==i' ] headMaybe :: [a] -> Maybe a headMaybe [] = Nothing headMaybe (x:_) = Just x ----------------------------------------------------------------------------- -- TIMonad: Type inference monad ----------------------------------------------------------------------------- newtype TI a b = TI (ClassEnv -> Int -> Either a (Int, b)) instance Monad (TI a) where return x = TI (\_ n -> Right (n,x)) TI c >>= f = TI (\ce n -> case c ce n of Right (m,x) -> let TI fx = f x in fx ce m Left x -> Left x) runTI :: ClassEnv -> TI Derivation Derivation -> Derivation runTI ce (TI c) = case c ce 0 of Right (_,result) -> result Left result -> result newTVar :: Kind -> TI a Type newTVar k = TI (\_ n -> let v = Tyvar (enumId n) k in Right (n+1, TVar v)) getClassEnv :: TI a ClassEnv getClassEnv = TI (\ce n -> Right (n,ce)) errorMsg :: String -> TI String a errorMsg msg = TI (\_ _ -> Left msg) errorDer :: Derivation -> TI Derivation a errorDer x = TI (\_ _ -> Left x) updateError :: (b -> c) -> TI b a -> TI c a updateError f (TI g) = TI (\ce n -> case g ce n of Left b -> Left (f b) Right a -> Right a) ----------------------------------------------------------------------------- -- TIMain: Type Inference Algorithm ----------------------------------------------------------------------------- ----------------------------------------------------------------------------- -- Lit: Literals ----------------------------------------------------------------------------- data Literal = LitInt Integer | LitChar Char deriving Eq tiLit :: Literal -> TI Derivation Derivation tiLit l@(LitChar _) = return $ Tree (TyExpr (Lit l) ([] :=> ([],tChar))) [] tiLit l@(LitInt _) = do tvar <- newTVar Star return $ Tree (TyExpr (Lit l) ([IsIn "Num" tvar] :=> ([],tvar))) [] ----------------------------------------------------------------------------- data Expr = Var Id | Lit Literal | Const Id | Ap Expr Expr | Let BindGroup Expr deriving Eq infixl `Ap` substNewTyVars :: Typing -> TI a Typing substNewTyVars ty = do let freeTyVars = tv ty freeKinds = map kind freeTyVars freeNew <- mapM newTVar freeKinds let freeSubst = zip freeTyVars freeNew return $ apply freeSubst ty tiExpr :: PolyEnv -> Expr -> TI Derivation Derivation tiExpr polyEnv e@(Var i) = case find i polyEnv of Just (Tree typing trees) -> do TyPolyVar predMonoEnvTy <- substNewTyVars typing return $ Tree (TyExpr e predMonoEnvTy) trees Nothing -> do t <- newTVar Star return $ Tree (TyExpr e ([] :=> ([i :>: t],t))) [] tiExpr polyEnv e@(Const i) = case find i polyEnv of Just (Tree typing _) -> do TyPolyVar predMonoEnvTy <- substNewTyVars typing return $ Tree (TyExpr e predMonoEnvTy) [] Nothing -> error "undefined data constructor" tiExpr _ (Lit l) = tiLit l tiExpr polyEnv e@(Ap e1 e2) = do d1@(Tree (TyExpr _ qty1) _) <- tiExpr polyEnv e1 d2@(Tree (TyExpr _ (pred2 :=> (monoEnv2,ty2))) _) <- tiExpr polyEnv e2 t <- newTVar Star case unifyTypings [qty1,pred2 :=> (monoEnv2,ty2 `fn` t)] of Correct (preds :=> (monoEnv,TAp (TAp _ _) tyRes)) -> return $ Tree (TyExpr e (preds :=> (monoEnv,tyRes))) [d1,d2] Wrong msg -> errorDer $ Tree (TyUExpr msg e) [d1,d2] tiExpr polyEnv e@(Let bg e1) = do d1@(Tree (TyBindGroup _ (predBg :=> (usedEnvBg,defEnvBg))) _) <- tiBindGroup polyEnv bg d2@(Tree (TyExpr _ qtyE1@(_ :=> (_,tyE1))) _) <- tiExpr (defEnvBg ++ polyEnv) e1 case unifyTypings [predBg :=> (usedEnvBg,tyE1),qtyE1] of Correct qEnvTy -> return $ Tree (TyExpr e qEnvTy) [d1,d2] Wrong msg -> errorDer $ Tree (TyUExpr msg e) [d1,d2] ----------------------------------------------------------------------------- type Alt = (Expr, Expr) tiAlt :: PolyEnv -> Alt -> TI Derivation Derivation tiAlt polyEnv (lhs,rhs) = do let localVars = vars lhs \\ (defVars lhs) let polyEnv' = polyEnv `without` localVars d1@(Tree (TyExpr _ qTyLhs) _) <- tiExpr polyEnv' lhs d2@(Tree (TyExpr _ qTyRhs) _) <- tiExpr polyEnv' rhs case unifyTypings [qTyLhs,qTyRhs] of Correct (preds :=> (usedEnv,_)) -> return $ Tree (TyAlt (lhs,rhs) (preds :=> (usedEnv `without` localVars))) [d1,d2] Wrong msg -> errorDer $ Tree (TyUAlt msg (lhs,rhs)) [d1,d2] type Def = [Alt] tiDef :: PolyEnv -> Def -> TI Derivation Derivation tiDef polyEnv alts = do derivations <- mapM (tiAlt polyEnv) alts let qUsedEnvs = map getQEnv $ derivations case unifyMonoEnvs qUsedEnvs of Correct (preds :=> usedEnv) -> return $ Tree (TyDef alts (preds :=> usedEnv)) derivations Wrong msg -> errorDer $ Tree (TyUDef msg alts) derivations where getQEnv (Tree (TyAlt _ qEnv) _ ) = qEnv vars :: Expr {-Pat-} -> [Id] vars (Var i) = [i] vars (Lit _) = [] vars (Const _) = [] vars (Ap e1 e2) = vars e1 ++ vars e2 vars (Let _ _) = error "vars: pattern" class Define a where defVars :: a -> [Id] instance Define Expr {- lhs of function def -} where defVars (Var f) = [f] defVars (Ap f _) = defVars f defVars _ = error "defVars: not a pattern" instance Define a => Define (a,b) where defVars (a,_) = defVars a instance Define a => Define [a] where defVars = concatMap defVars ----------------------------------------------------------------------------- -- Defaulting: ----------------------------------------------------------------------------- split :: [Tyvar] -> [Tyvar] -> [Pred] -> TI String ([Pred], [Pred]) split fs gs ps = do ce <- getClassEnv ps' <- reduce ps let (ds, rs) = partition (all (`elem` fs) . tv) ps' rs' <- error2TI $ defaultedPreds ce (fs++gs) rs return (ds, rs \\ rs') type Ambiguity = (Tyvar, [Pred]) ambiguities :: ClassEnv -> [Tyvar] -> [Pred] -> [Ambiguity] ambiguities _ vs ps = [ (v, filter (elem v . tv) ps) | v <- tv ps \\ vs ] numClasses :: [Id] numClasses = ["Num", "Integral", "Floating", "Fractional", "Real", "RealFloat", "RealFrac"] stdClasses :: [Id] stdClasses = ["Eq", "Ord", "Show", "Read", "Bounded", "Enum", "Ix", "Functor", "Monad", "MonadPlus"] ++ numClasses candidates :: ClassEnv -> Ambiguity -> [Type] candidates ce (v, qs) = [ t' | let is = [ i | IsIn i _ <- qs ] ts = [ t | IsIn _ t <- qs ], all ((TVar v)==) ts, any (`elem` numClasses) is, all (`elem` stdClasses) is, t' <- defaults ce, all (entail ce []) [ IsIn i t' | i <- is ] ] withDefaults :: Monad m => ([Ambiguity] -> [Type] -> a) -> ClassEnv -> [Tyvar] -> [Pred] -> m a withDefaults f ce vs ps | any null tss = fail "cannot resolve ambiguity" | otherwise = return (f vps (map head tss)) where vps = ambiguities ce vs ps tss = map (candidates ce) vps defaultedPreds :: Monad m => ClassEnv -> [Tyvar] -> [Pred] -> m [Pred] defaultedPreds = withDefaults (\vps _ -> concat (map snd vps)) defaultSubst :: [Tyvar] -> [Pred] -> PolyEnv -> TI String PolyEnv defaultSubst vs ps env = do ce <- getClassEnv s <- withDefaults (\vps ts -> zip (map fst vps) ts) ce vs ps return $ apply s env ----------------------------------------------------------------------------- -- BindGroup ----------------------------------------------------------------------------- newtype BindGroup = BG [Def] deriving Eq tiBindGroup :: PolyEnv -> BindGroup -> TI Derivation Derivation tiBindGroup polyEnv bg@(BG defs) = do let boundVars = nub . concatMap defVars $ defs derivations <- mapM (tiDef (polyEnv `without` boundVars)) defs let qEnvs = map getQEnv derivations case unifyMonoEnvs qEnvs of Wrong msg -> errorDer $ Tree (TyUBindGroup msg bg) derivations Correct (defsPreds :=> occEnv) -> do let (defsEnv,usedEnv) = partition (\(x :>: _) -> x `elem` boundVars) occEnv usedEnvTyVars = tv usedEnv defsTyVars = [tv ty | (_ :>: ty) <- defsEnv] (ds,rs) <- updateError (\s -> (Tree (TyUBindGroup s bg) derivations)) (split usedEnvTyVars (foldr1 intersect defsTyVars) defsPreds) let (deferredPreds,retainedPreds) | restricted bg = (ds++rs,[]) | otherwise = (ds,rs) return $ Tree (TyBindGroup bg (deferredPreds :=> (usedEnv ,[ f :>: Tree (TyPolyVar (retainedPreds :=> (reduceMonoEnv (tv ty) usedEnv,ty))) derivations | f :>: ty <- defsEnv ]))) derivations where getQEnv (Tree (TyDef _ qEnv) _) = qEnv restricted :: BindGroup -> Bool restricted (BG defs) = any simple defs where simple = isVar . fst . head isVar (Var _) = True isVar _ = False reduceMonoEnv :: [Tyvar] -> MonoEnv -> MonoEnv -- Remove unnecessary variables from a monomorphic environment reduceMonoEnv ids monoEnv = filter (hasTyVarsFrom ids) monoEnv where hasTyVarsFrom :: [Tyvar] -> Assump Type -> Bool hasTyVarsFrom ids a = not . null $ ids `intersect` tv a tiSeq :: (PolyEnv -> term -> TI a Derivation) -> PolyEnv -> [term] -> TI a [Derivation] tiSeq _ _ [] = return $ [] tiSeq ti polyEnv (bs:bss) = do d1@(Tree (TyBindGroup _ (_ :=> (_, polyEnv'))) _) <- ti polyEnv bs derivations <- tiSeq ti (polyEnv' ++ polyEnv) bss return $ d1:derivations ----------------------------------------------------------------------------- -- TIProg: Type Inference for Whole Programs ----------------------------------------------------------------------------- type Program = [BindGroup] tiProgram :: PolyEnv -> Program -> Derivation tiProgram polyEnv bgs = runTI ((\(Correct x) -> x) (exampleInsts initialEnv)) $ do derivations <- tiSeq tiBindGroup polyEnv bgs let (preds,defEnv) = case unzip (map getPredsDefEnv derivations) of (predss,defEnvs) -> (concat predss,concat defEnvs) remainingPreds <- updateError (\s -> (Tree (TyUProgram s bgs) derivations)) (reduce preds) defEnv' <- updateError (\s -> (Tree (TyUProgram s bgs) derivations)) (defaultSubst [] remainingPreds defEnv) return $ Tree (TyProgram bgs defEnv') derivations where getPredsDefEnv (Tree (TyBindGroup _ (preds :=> ([],polyEnv))) _) = (preds,polyEnv) ----------------------------------------------------------------------------- -- Main: ----------------------------------------------------------------------------- inter :: Program -> IO () inter prog = do putStr "\n\n1 Free navigation through the graph" putStr "\n2 Algorithmic debugging" putStr "\nq Quit" putStr "\nSelect (1 or 2 or q): " c <- getChar case c of '1' -> do putStrLn "\nPress ? for help" walk True True False [] [] (tiProgram env prog,Empty) inter prog '2' -> do putStrLn "\nPress ? for help" let tree = tiProgram env prog printStep False False True (tree,Empty) walk False False True [] [] (algNo True [] (tree,Empty)) inter prog 'q' -> return () _ -> inter prog main :: IO () main = do putStr "\n\nTypeIlluminator Version 13.09.01\nwritten by Olaf Chitil\n\n" putStrLn . concatMap (\(n,p) -> "\n\n" ++ show n ++ ppProgram2 p) . zip [(1::Int)..] $ progs putStr ("\nPlease choose an example program (1-" ++ show numProgs ++ ") ") c <- getChar let i = digitToInt c if c > '0' && c <= '9' && i <= numProgs then inter (progs !! (i-1)) else main where numProgs = length progs progs = [progStart,prog2,prog3,progClass1,progClass2] ----------------------------------------------------------------------------- -- Tests: ----------------------------------------------------------------------------- tyVarA :: Type tyVarA = TVar (Tyvar "a" Star) tyVarB :: Type tyVarB = TVar (Tyvar "b" Star) tyVarC :: Type tyVarC = TVar (Tyvar "c" Star) tIO :: Type tIO = TCon (Tycon "IO" (Kfun Star Star)) tBool :: Type tBool = TCon (Tycon "Bool" Star) consNil :: Expr consNil = Const "[]" consCons :: Expr consCons = Const ":" global :: Type -> Tree Typing global t = Tree (TyPolyVar ([] :=> ([],t))) [] globalPreds :: [Pred] -> Type -> Tree Typing globalPreds preds t = Tree (TyPolyVar (preds :=> ([],t))) [] env :: PolyEnv env = ["[]" :>: global (TAp tList tyVarA) ,":" :>: global (tyVarA `fn` (TAp tList tyVarA) `fn` (TAp tList tyVarA)) ,"False" :>: global tBool ,"True" :>: global tBool ,"()" :>: global tUnit ,"." :>: global ((tyVarA `fn` tyVarB) `fn` (tyVarC `fn` tyVarA) `fn` (tyVarC `fn` tyVarB)) ,"print" :>: globalPreds [IsIn "Show" tyVarA] (tyVarA `fn` TAp tIO tUnit) ,"putStr" :>: global (tString `fn` TAp tIO tUnit) ,"show" :>: globalPreds [IsIn "Show" tyVarA] (tyVarA `fn` tString) ,"div" :>: globalPreds [IsIn "Integral" tyVarA] (tyVarA `fn` tyVarA `fn` tyVarA) ,"map" :>: global ((tyVarA `fn` tyVarB) `fn` TAp tList tyVarA `fn` TAp tList tyVarA) ,"++" :>: global (TAp tList tyVarA `fn` TAp tList tyVarA `fn` TAp tList tyVarA) ,"toUpper" :>: global (tChar `fn` tChar) ,":" :>: global (tyVarA `fn` TAp tList tyVarA `fn` TAp tList tyVarA) ,"[]" :>: global (TAp tList tyVarA) ] defStart :: Def defStart = [(Var "start" `Ap` Var "xs" `Ap` Var "ys" ,((Var ".") `Ap` (Var "map" `Ap` Var "toUpper") `Ap` (Var "++")) `Ap` Var "xs" `Ap` Var "ys")] progStart :: [BindGroup] progStart = [BG [defStart]] defReverse :: Def defReverse = [(Ap (Var "reverse") consNil, consNil) ,(Ap (Var "reverse") (Ap (Ap consCons (Var "x")) (Var "xs")) ,Ap (Ap (Var "++") (Ap (Var "reverse") (Var "xs"))) (Var "x"))] defLast :: Def defLast = [(Ap (Var "last") (Var "xs"), Ap (Var "head") (Ap (Var "reverse") (Var "xs")))] defInit :: Def defInit = [(Ap (Var "init") (Var "xs"), Ap (Var "reverse") (Ap (Var "tail") (Ap (Var "reverse") (Var "xs"))))] defRotateR :: Def defRotateR = [(Ap (Var "rotateR") (Var "xs"), Ap (Ap consCons (Ap (Var "last") (Var "xs"))) (Ap (Var "init") (Var "xs")))] defHead :: Def defHead = [(Ap (Var "head") (Ap (Ap consCons (Var "x")) (Var "xs")) ,Var "x")] defTail :: Def defTail = [(Ap (Var "tail") (Ap (Ap consCons (Var "x")) (Var "xs")) ,Var "xs")] prog2 :: Program prog2 = [BG [defHead], BG [defTail], BG [defReverse], BG [defLast], BG [defInit], BG [defRotateR]] prog3 :: Program prog3 = [BG [defReverse]] defClass1 :: Def defClass1 = [(Var "class1" ,((Var ".") `Ap` (Var "print") `Ap` (Var "div")) `Ap` (Lit (LitInt 42)))] progClass1 :: [BindGroup] progClass1 = [BG [defClass1]] defClass2 :: Def defClass2 = [(Var "class2" ,((Var ".") `Ap` ((Var ".") `Ap` (Var "putStr") `Ap` (Var "show")) `Ap` ((Var "div") `Ap` (Lit (LitInt 42)))) `Ap` (Lit (LitInt 2)))] progClass2 :: [BindGroup] progClass2 = [BG [defClass2]] -----------------------------------------------------------------------------