[alternative type inference implementation based on THIH mail@stefanwehr.de**20050520112805] { hunk ./KindInference.hs 77 -instance Substitution a b c => Substitution a b (d, c) where - applySubst s (x, y) = (x, applySubst s y) +--instance Substitution a b c => Substitution a b (d, c) where +-- applySubst s (x, y) = (x, applySubst s y) hunk ./KindInference.hs 80 -instance Kinds a => Kinds (b, a) where - vars (x, y) = vars y +--instance Kinds a => Kinds (b, a) where +-- vars (x, y) = vars y hunk ./ParseSyntax.hs 15 +import qualified Map hunk ./ParseSyntax.hs 265 + +instance Types a => Types (Map.Map k a) where + freeTypeVars m = freeTypeVars (Map.elems m) + fixedTypeVars m = fixedTypeVars (Map.elems m) hunk ./Pretty.hs 57 +--instance (Pretty a, Pretty b) => Pretty (a, b) where +-- ppr (a,b) = parens (ppr a <> comma <+> ppr b) hunk ./Substitution.hs 38 +instance (Substitution a b c, Substitution a b d) + => Substitution a b (c, d) where + applySubst s (c, d) = (applySubst s c, applySubst s d) + hunk ./Symtab.hs 107 --- we return a Type instead of a TypeVarId here, because it eliminates --- the risk of instantiating a type scheme "the wrong way round" (replacing --- the fresh vars with the quantified vars). - addfile ./TypeInference.hs.old hunk ./TypeInference.hs.old 1 +module TypeInference where + +import Control.Monad.State +import Control.Monad.Error +import qualified Map +import AbstractSyntax +import Substitution +import Error +import Pretty +import Symtab + +type InstanceEnv = [ConstraintScheme] +type TypeEnv = Map.Map ValId TypeScheme + +lookupTyEnv :: ValId -> TypeEnv -> Maybe TypeScheme +lookupTyEnv = Map.lookup + +extendTyEnv :: ValId -> TypeScheme -> TypeEnv -> TypeEnv +extendTyEnv = Map.insert + +extendTyEnv' :: [(ValId, TypeScheme)] -> TypeEnv -> TypeEnv +extendTyEnv' assocs env = + foldr (\ (k,v) e -> extendTyEnv k v e) env assocs + +data TIState = TIState { ti_thetaProgram :: InstanceEnv } + +emptyTIState = TIState { ti_thetaProgram = [] } + +type TI = StateT TIState ST + +liftST :: ST a -> TI a +liftST x = lift x + +runTI :: InstanceEnv -> TI a -> ST a +runTI ie ti = evalStateT ti (emptyTIState { ti_thetaProgram = ie }) + +splitConstraints :: [Constraint] -> ([ClassConstraint], [EqConstraint]) +splitConstraints = undefined + +--catchTI :: TI a -> [FailureCause] -> (FailureCause -> TI a) -> TI a +--catchTI st causes handler = mkCatchFailure catchST st causes handler + +type TIResult = (([ClassConstraint], [EqConstraint]), TypeSubst, Type) + +tiExp :: TypeEnv -> Exp -> TI TIResult + +tiExp env (Var id) = + let scheme = case lookupTyEnv id env of + Just x -> x + Nothing -> + phasefail ("variable `" ++ showPpr id ++ + "' not contained in value environment") + quants = tyscheme_quants scheme + (constrs, ty) = case tyscheme_qtype scheme of + UnconstrainedType t -> ([], t) + ConstrainedType cs t -> (cs, t) + in do (constrs', _) <- liftST $ instantiate quants constrs + (ty', _) <- liftST $ instantiate quants ty + return (splitConstraints constrs', nullSubst, ty') + +tiExp env (App e1 e2) = + do ((theta1, u1), t1, tau1) <- tiExp env e1 + ((theta2, u2), t2, tau2) <- tiExp (applySubst t1 env) e2 + thetaP <- gets ti_thetaProgram + alpha <- liftST $ freshTypeVar KindStar + -- FIXME: unification missing + (u, r) <- (undefined :: TI ([EqConstraint], TypeSubst)) + let resTheta = applySubst r $ (applySubst t2 theta1) ++ theta2 + resSubst = r `composeSubst` t2 `composeSubst` t1 + resType = applySubst r alpha + return ((resTheta, u), resSubst, resType) + +tiExp env (Lam vars e) = + do (alphas, schemes) <- freshTyVars (length vars) + (ctx, t, tau) <- tiExp (extendTyEnv' (zip vars schemes) env) e + return (ctx, t, tyApps (applySubst t alphas) tau) + +tiExp env (Let binds exp) = tiExp env (Letrec binds exp) + +tiExp env (Letrec binds exp) = + do group <- toBindGroup binds + (subst, types) <- tiBindGroup env group + (ctx, subst', tau) <- tiExp (applySubst subst (extendTyEnv' types env)) + exp + return (ctx, subst' `composeSubst` subst, tau) + + +tiImpls :: TypeEnv -> [ImplBind] -> TI (TypeSubst, [(ValId, TypeScheme)]) +tiImpls env binds = + do (alphas, schemes) <- freshTyVars (length binds) + let ids = map fst binds + exps = map snd binds + env' = extendTyEnv' (zip ids schemes) env + res <- mapM (tiExp env') exps + let (ctx, ts, taus) = unzip3 res + (thetas, us) = unzip ctx + let t = case foldM mergeSubst nullSubst ts of + Left err -> phasefail ("type error: " ++ err) + Right x -> x + theta = concat thetas + u = concat us + sigmas = map (generalize (applySubst t env') theta u) taus + return (t, (zip ids sigmas)) + +tiExpl :: TypeEnv -> [ExplBind] -> TI TypeSubst +tiExpl = undefined + +tiBindGroup :: TypeEnv -> BindGroup -> TI (TypeSubst, [(ValId, TypeScheme)]) +tiBindGroup env (BindGroup es iss) = + let explTypes = [(id,ty) | (id,ty,exp) <- es] + env' = extendTyEnv' explTypes env + in do (subst, implTypes) <- tiIss env' iss + let env'' = applySubst subst (extendTyEnv' implTypes env') + subst' <- tiExpl env'' es + return (subst' `composeSubst` subst, explTypes ++ implTypes) + where tiIss _ [] = return (nullSubst, []) + tiIss env (i:is) = + do (subst, types) <- tiImpls env i + let env' = applySubst subst (extendTyEnv' types env) + (subst', types') <- tiIss env' iss + return (subst' `composeSubst` subst, types ++ types') + +type ExplBind = (ValId, TypeScheme, Exp) +type ImplBind = (ValId, Exp) +data BindGroup = BindGroup [ExplBind] [[ImplBind]] + +toBindGroup :: [ValBind] -> TI BindGroup +-- FIXME +toBindGroup binds = + do is <- mapM toImpl binds + return $ BindGroup [] [is] + where toImpl (ValBind _ (Just _) _ _) = + phasefail "explicitly typed bindings not supported atm" + toImpl (ValBind id Nothing args exp) = + return (id, Lam args exp) + + +-- FIXME: use split in generalization!! +generalize :: TypeEnv -> [ClassConstraint] -> [EqConstraint] -> Type + -> TypeScheme +generalize = undefined + +toScheme :: Type -> TypeScheme +toScheme t = TypeScheme [] (UnconstrainedType t) + +freshTyVars n = + do alphas <- liftST $ mapM freshTypeVar + (take n $ repeat KindStar) + return (alphas, map toScheme alphas) }