module Language.HM.Theta where
import Data.Fix
import qualified Data.Map as M
import Language.HM.Type
import Language.HM.Term
type Theta = M.Map String Tau
class CanApply a where
apply :: Theta -> a -> a
instance CanApply Tau where
apply s = cata g
where
g :: TauF Tau -> Tau
g (VarT x) = case M.lookup x s of
Nothing -> varT x
Just t -> apply s t
g (ArrowT t0 t1) = arrowT t0 t1
instance CanApply Sigma where
apply s = cata g
where
g :: SigmaF Sigma -> Sigma
g (MonoT t) = monoT (apply s t)
g (ForAllT x t) = forAllT x (apply (M.delete x s) t)
instance CanApply t => CanApply (Typed t a) where
apply s (Typed x t) = Typed x (apply s t)
instance CanApply TyTerm where
apply s = cata g
where
g (TypedF t) = Fix $ TypedF (apply s t)
(<@>) :: Theta -> Theta -> Theta
s1 <@> s2 = M.map (apply s1) s2 `M.union` s1