Simply-typed Curry-style (nominal) lambda-calculus with integers and zero-comparison Let-polymorphism via inlining Type inference
- data Typ
- type TVarName = Int
- data Term
- type VarName = String
- type TEnv = [(VarName, TVEM Typ)]
- env0 :: TEnv
- lkup :: TEnv -> VarName -> TVEM Typ
- ext :: TEnv -> (VarName, TVEM Typ) -> TEnv
- data TVE = TVE Int (IntMap Typ)
- type TVEM = State TVE
- newtv :: TVEM Typ
- tve0 :: TVE
- tvlkup :: TVE -> TVarName -> Maybe Typ
- tvext :: TVE -> (TVarName, Typ) -> TVE
- tvsub :: TVE -> Typ -> Typ
- tvchase :: TVE -> Typ -> Typ
- unify :: Typ -> Typ -> TVE -> Either String TVE
- unify' :: Typ -> Typ -> TVE -> Either String TVE
- unifyv :: TVarName -> Typ -> TVE -> Either String TVE
- occurs :: TVarName -> Typ -> TVE -> Bool
- unifyM :: Typ -> Typ -> (String -> String) -> TVEM ()
- teval' :: TEnv -> Term -> TVEM Typ
- teval :: TEnv -> Term -> Typ
Documentation
type TEnv = [(VarName, TVEM Typ)]Source
Type Environment: associating *would-be* types with free
term variables
Type Variable Environment: associating types with free
type variables
tvchase :: TVE -> Typ -> TypSource
shallow
substitution; check if tv is bound to anything substantial
unify :: Typ -> Typ -> TVE -> Either String TVESource
The unification. If unification failed, return the reason
unify' :: Typ -> Typ -> TVE -> Either String TVESource
If either t1 or t2 are type variables, they are definitely unbound