TypeIlluminator (empty) → 0.0
raw patch · 4 files changed
+1666/−0 lines, 4 filesdep +basedep +haskell98setup-changed
Dependencies added: base, haskell98
Files
- LICENSE +31/−0
- Setup.hs +5/−0
- TypeIlluminator.cabal +22/−0
- TypeIlluminator.hs +1608/−0
+ LICENSE view
@@ -0,0 +1,31 @@+Copyright (c) 2007,2008 Spencer Janssen+Copyright (c) 2007,2008 Don Stewart++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++2. 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.++3. Neither the name of the author nor the names of his contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS OR 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.
+ Setup.hs view
@@ -0,0 +1,5 @@+#!/usr/bin/runhaskell++import Distribution.Simple++main = defaultMainWithHooks defaultUserHooks
+ TypeIlluminator.cabal view
@@ -0,0 +1,22 @@+name: TypeIlluminator+version: 0.0+synopsis: TypeIlluminator is a prototype tool exploring debugging of type errors/+description: TypeIlluminator is a prototype tool implementing the ideas presented in the paper+ Compositional Explanation of Types and Algorithmic Debugging of Type Errors.+ It constructs the type explanation graph for programs written in a simple+ Haskell-like language and enables free navigation through the graph+ in various ways and algorithmic debugging.+category: Compilers/Interpreters+license: BSD3+license-file: LICENSE+author: Olaf Chitil+maintainer: Olaf Chitil <O.Chitil@kent.ac.uk>+homepage: http://www.cs.kent.ac.uk/people/staff/oc/TypeIlluminator/+build-depends: base, haskell98+build-type: Simple++executable: typeilluminator+main-is: TypeIlluminator.hs++ghc-options: -O2 -Wall -optl-Wl,-s+ghc-prof-options: -prof -auto-all
+ TypeIlluminator.hs view
@@ -0,0 +1,1608 @@+{-+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]]+++-----------------------------------------------------------------------------+++