+:: Scheme = Forall [TVar] Type
+:: Gamma :== 'Map'.Map String Scheme //map from Variables! to types
+:: Typing a :== StateT (Gamma, [TVar]) (Either SemError) a
+:: Substitution :== 'Map'.Map TVar Type
+:: Constraints :== [(Type, Type)]
+:: SemError
+ = ParseError Pos String
+ | UnifyError Pos Type Type
+ | InfiniteTypeError Pos Type
+ | FieldSelectorError Pos Type FieldSelector
+ | OperatorError Pos Op2 Type
+ | UndeclaredVariableError Pos String
+ | ArgumentMisMatchError Pos String
+ | SanityError Pos String
+ | Error String
+
+instance zero Gamma where
+ zero = 'Map'.newMap
+
+variableStream :: [TVar]
+variableStream = map toString [1..]
+
+sem :: AST -> Either [SemError] AST
+//sem a = pure a
+sem (AST fd) = case foldM (const $ hasNoDups fd) () fd
+ >>| foldM (const isNiceMain) () fd
+ >>| hasMain fd
+ >>| evalStateT (type fd) (zero, variableStream) of
+ Left e = Left [e]
+ Right fds = Right (AST fds)
+ //_ = case execRWST (constraints fd) zero variableStream of
+ // Left e = Left [e]
+ // Right (a, b) = Right b
+where
+ constraints :: [FunDecl] -> Typing ()
+ constraints _ = pure ()
+ //TODO: fix
+ //constraints fds = mapM_ funconstraint fds >>| pure ()
+
+ funconstraint :: FunDecl -> Typing ()
+ funconstraint fd=:(FunDecl _ ident args mt vardecls stmts) = case mt of
+ Nothing = abort "Cannot infer functions yet"
+ _ = pure ()
+ //Just t = inEnv (ident, (Forall [] t)) (
+ // mapM_ vardeclconstraint vardecls >>| pure ())
+
+ vardeclconstraint :: VarDecl -> Typing ()
+ vardeclconstraint _ = pure ()
+ //TODO: fix!
+ //vardeclconstraint (VarDecl p mt ident expr) = infer expr
+ //>>= \it->inEnv (ident, (Forall [] it)) (pure ())
+
+ hasNoDups :: [FunDecl] FunDecl -> Either SemError ()
+ hasNoDups fds (FunDecl p n _ _ _ _)
+ # mbs = map (\(FunDecl p` n` _ _ _ _)->if (n == n`) (Just p`) Nothing) fds
+ = case catMaybes mbs of
+ [] = Left $ SanityError p "HUH THIS SHOULDN'T HAPPEN"
+ [x] = pure ()
+ [_:x] = Left $ SanityError p (concat
+ [n, " multiply defined at ", toString p])
+
+ hasMain :: [FunDecl] -> Either SemError ()
+ hasMain [(FunDecl _ "main" _ _ _ _):fd] = pure ()
+ hasMain [_:fd] = hasMain fd
+ hasMain [] = Left $ SanityError zero "no main function defined"
+
+ isNiceMain :: FunDecl -> Either SemError ()
+ isNiceMain (FunDecl p "main" as mt _ _) = case (as, mt) of
+ ([_:_], _) = Left $ SanityError p "main must have arity 0"
+ ([], t) = (case t of
+ Nothing = pure ()
+ Just VoidType = pure ()
+ _ = Left $ SanityError p "main has to return Void")
+ isNiceMain _ = pure ()
+
+class Typeable a where
+ ftv :: a -> [TVar]
+ subst :: Substitution a -> a
+
+instance Typeable Scheme where
+ ftv (Forall bound t) = difference (ftv t) bound
+ subst s (Forall bound t) = Forall bound $ subst s_ t
+ where s_ = 'Map'.filterWithKey (\k _ -> not (elem k bound)) s
+
+instance Typeable [a] | Typeable a where
+ ftv types = foldr (\t ts-> ftv t ++ ts) [] types
+ subst s ts = map (\t->subst s t) ts
+
+instance Typeable Type where
+ ftv (TupleType (t1, t2)) = ftv t1 ++ ftv t2
+ ftv (ListType t) = ftv t
+ ftv (IdType tvar) = [tvar]
+ ftv (t1 ->> t2) = ftv t1 ++ ftv t2
+ ftv _ = []
+ subst s (TupleType (t1, t2))= TupleType (subst s t1, subst s t2)
+ subst s (ListType t1) = ListType (subst s t1)
+ subst s (t1 ->> t2) = (subst s t1) ->> (subst s t2)
+ subst s t1=:(IdType tvar) = 'Map'.findWithDefault t1 tvar s
+ subst s t = t
+
+instance Typeable Gamma where
+ ftv gamma = concatMap id $ map ftv ('Map'.elems gamma)
+ subst s gamma = Mapmap (subst s) gamma
+
+extend :: String Scheme Gamma -> Gamma
+extend k t g = 'Map'.put k t g
+
+//// ------------------------
+//// algorithm U, Unification
+//// ------------------------
+instance zero Substitution where zero = 'Map'.newMap
+
+compose :: Substitution Substitution -> Substitution
+compose s1 s2 = 'Map'.union (Mapmap (subst s1) s2) s1
+//Note: just like function compositon compose does snd first
+
+occurs :: TVar a -> Bool | Typeable a
+occurs tvar a = elem tvar (ftv a)
+
+unify :: Type Type -> Either SemError Substitution
+unify t1 t2=:(IdType tv) | t1 == (IdType tv) = Right zero
+ | occurs tv t1 = Left $ InfiniteTypeError zero t1
+ | otherwise = Right $ 'Map'.singleton tv t1
+unify t1=:(IdType tv) t2 = unify t2 t1
+unify (ta1->>ta2) (tb1->>tb2) = unify ta1 tb1 >>= \s1->
+ unify ta2 tb2 >>= \s2->
+ Right $ compose s1 s2
+unify (TupleType (ta1,ta2)) (TupleType (tb1,tb2)) = unify ta1 tb1 >>= \s1->
+ unify ta2 tb2 >>= \s2->
+ Right $ compose s1 s2
+unify (ListType t1) (ListType t2) = unify t1 t2
+unify t1 t2 | t1 == t2 = Right zero
+ | otherwise = Left $ UnifyError zero t1 t2
+
+//// ------------------------
+//// Algorithm M, Inference and Solving
+//// ------------------------
+gamma :: Typing Gamma
+gamma = gets fst
+putGamma :: Gamma -> Typing ()
+putGamma g = modify (appFst $ const g) >>| pure ()
+changeGamma :: (Gamma -> Gamma) -> Typing Gamma
+changeGamma f = modify (appFst f) >>| gamma
+withGamma :: (Gamma -> a) -> Typing a
+withGamma f = f <$> gamma
+fresh :: Typing Type
+fresh = gets snd >>= \vars->
+ modify (appSnd $ const $ tail vars) >>|
+ pure (IdType (head vars))
+
+lift :: (Either SemError a) -> Typing a
+lift (Left e) = liftT $ Left e
+lift (Right v) = pure v
+
+//instantiate maps a schemes type variables to variables with fresh names
+//and drops the quantification: i.e. forall a,b.a->[b] becomes c->[d]
+instantiate :: Scheme -> Typing Type
+instantiate (Forall bound t) =
+ mapM (const fresh) bound >>= \newVars->
+ let s = 'Map'.fromList (zip (bound,newVars)) in
+ pure (subst s t)
+
+//generalize quentifies all free type variables in a type which are not
+//in the gamma
+generalize :: Type -> Typing Scheme
+generalize t = gamma >>= \g-> pure $ Forall (difference (ftv t) (ftv g)) t
+
+lookup :: String -> Typing Type
+lookup k = gamma >>= \g-> case 'Map'.member k g of
+ False = liftT (Left $ UndeclaredVariableError zero k)
+ True = instantiate $ 'Map'.find k g