hakaru-0.3.0: A probabilistic programming language

CopyrightCopyright (c) 2016 the Hakaru team
LicenseBSD3
Maintainerwren@community.haskell.org
Stabilityexperimental
PortabilityGHC-only
Safe HaskellNone
LanguageHaskell2010

Language.Hakaru.Syntax.TypeCheck

Contents

Description

Bidirectional type checking for our AST.

Synopsis

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.

Constructors

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

Instances

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

Methods

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 # 

Methods

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 #