| Copyright | Copyright (c) 2016 the Hakaru team |
|---|---|
| License | BSD3 |
| Maintainer | wren@community.haskell.org |
| Stability | experimental |
| Portability | GHC-only |
| Safe Haskell | None |
| Language | Haskell2010 |
Language.Hakaru.Syntax.TypeCheck
Description
Bidirectional type checking for our AST.
- type TypeCheckError = Text
- data TypeCheckMonad a
- runTCM :: TypeCheckMonad a -> Input -> TypeCheckMode -> Either TypeCheckError a
- unTCM :: TypeCheckMonad a -> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a
- data TypeCheckMode
- inferable :: AST -> Bool
- mustCheck :: AST -> Bool
- data TypedAST abt = TypedAST !(Sing b) !(abt '[] b)
- inferType :: forall abt. ABT Term abt => AST -> TypeCheckMonad (TypedAST abt)
- checkType :: forall abt a. ABT Term abt => Sing a -> AST -> TypeCheckMonad (abt '[] a)
The type checking monad
type TypeCheckError = Text Source #
data TypeCheckMonad a Source #
runTCM :: TypeCheckMonad a -> Input -> TypeCheckMode -> Either TypeCheckError a Source #
unTCM :: TypeCheckMonad a -> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a Source #
Type checking itself
inferable :: AST -> Bool Source #
Those terms from which we can synthesize a unique type. We are also allowed to check them, via the change-of-direction rule.
mustCheck :: AST -> Bool Source #
Those terms whose types must be checked analytically. We cannot synthesize (unambiguous) types for these terms.
N.B., this function assumes we're in StrictMode. If we're
actually in LaxMode then a handful of AST nodes behave
differently: in particular, NaryOp_, Superpose, and
Case_. In strict mode those cases can just infer one of their
arguments and then check the rest against the inferred type.
(For case-expressions, we must also check the scrutinee since
it's type cannot be unambiguously inferred from the patterns.)
Whereas in lax mode we must infer all arguments and then take
the lub of their types in order to know which coercions to
introduce.
The e' ∈ τ portion of the inference judgement.
inferType :: forall abt. ABT Term abt => AST -> TypeCheckMonad (TypedAST abt) Source #
Given a typing environment and a term, synthesize the term's type (and produce an elaborated term):
Γ ⊢ e ⇒ e' ∈ τ
checkType :: forall abt a. ABT Term abt => Sing a -> AST -> TypeCheckMonad (abt '[] a) Source #
Given a typing environment, a type, and a term, verify that the term satisfies the type (and produce an elaborated term):
Γ ⊢ τ ∋ e ⇒ e'