| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
L3.Core.Infer
Description
Type checking and type inference
Synopsis
- weakInferType :: (Eq a, Enum a, Show a) => Context a -> Expr a -> Result (Expr a)
- inferType :: (Eq a, Enum a, Show a) => Context a -> Expr a -> Result (Expr a)
- inferType0 :: (Eq a, Enum a, Show a) => Expr a -> Result (Expr a)
- inferType1 :: (Eq a, Enum a, Show a) => Context a -> Expr a -> Result (Expr a)
- wellTyped :: (Eq a, Enum a, Show a) => Context a -> Expr a -> Bool
- wellTyped0 :: (Eq a, Enum a, Show a) => Expr a -> Bool
Documentation
weakInferType :: (Eq a, Enum a, Show a) => Context a -> Expr a -> Result (Expr a) Source #
Type-check an expression and return the expression's type if type-checking
| succeeds or an error message if type-checking fails
| inferType` does not necessarily normalize the type since full normalization
| is not necessary for just type-checking. If you actually care about the
| returned type then you may want to normalize it afterwards.
| Type inference is within a type context (list of global names and their types)
|
| Weak type infernce here refers to the lack of partial evaluation for contextual
| beta-equivalence. For some X, a by-value and by-reference of X should be legal:
| (λ (T : *) . λ (f : π (X : *) . X) . λ (x : T) . f x) X
| In fact, resolving T := X as beta-equivalent to X will fail for weakInferType.
inferType :: (Eq a, Enum a, Show a) => Context a -> Expr a -> Result (Expr a) Source #
Type-check an expression and return the expression's normalized type if | type-checking succeeds or an error message if type-checking fails
inferType0 :: (Eq a, Enum a, Show a) => Expr a -> Result (Expr a) Source #
inferType0 is the same as inferType with an empty context, meaning that
| the expression must be closed (i.e. no free variables), otherwise type-checking
| will fail.
inferType1 :: (Eq a, Enum a, Show a) => Context a -> Expr a -> Result (Expr a) Source #
Type-check an expression and return the expression's normalized type if
| type-checking succeeds or an error message if type-checking fails
| Perform partial evaluation by substitution of lambda-applications to types
| to ensure the problem-case for weakInferType does not fail here.