-//:: Typing a :== StateT (Gamma, [TVar]) Either a
-
-//map a schemes type variables to variables with fresh names
-//i.e. a->[b] becomes c->[d]
+//The typing monad
+:: Typing a :== StateT (Gamma, [TVar]) (Either SemError) a
+gamma :: Typing Gamma
+gamma = gets fst
+putGamma :: Gamma -> Typing ()
+putGamma g = modify (appFst $ const g) >>| pure ()
+withGamma :: (Gamma -> Gamma) -> Typing ()
+withGamma f = modify (appFst f) >>| pure ()
+fresh :: Typing Type
+fresh = gets snd >>= \vars->
+ modify (appSnd $ const $ tail vars) >>|
+ pure (IdType (head vars))
+
+//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