Simply-typed Curry-style (nominal) lambda-calculus with integers and zero-comparison Type inference
- data Typ
- type TVarName = Int
- data Term
- type VarName = String
- type TEnv = [(VarName, Typ)]
- env0 :: TEnv
- lkup :: TEnv -> VarName -> Typ
- ext :: TEnv -> (VarName, Typ) -> TEnv
- data TVE = TVE Int (IntMap Typ)
- newtv :: TVE -> (Typ, TVE)
- 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
- teval' :: TEnv -> Term -> TVE -> (Typ, TVE)
- teval :: TEnv -> Term -> Typ
Documentation
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