hakaru-0.3.0: A probabilistic programming language

CopyrightCopyright (c) 2016 the Hakaru team
Safe HaskellNone




Bidirectional type checking for our AST.


The type checking monad

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.

data TypedAST abt Source #

The e' ∈ τ portion of the inference judgement.


TypedAST !(Sing b) !(abt '[] b) 


Show2 Hakaru [Hakaru] abt => Show (TypedAST abt) Source # 


showsPrec :: Int -> TypedAST abt -> ShowS #

show :: TypedAST abt -> String #

showList :: [TypedAST abt] -> ShowS #

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'

Orphan instances

ABT Hakaru Term abt => Coerce (Branch a abt) Source # 


coerceTo :: Coercion a b -> Branch a abt a -> Branch a abt b Source #

coerceFrom :: Coercion a b -> Branch a abt b -> Branch a abt a Source #