Language.Hakaru.Syntax.TypeCheck

Bidirectional type checking for our AST.

The type checking monad

type TypeCheckError = Text

data TypeCheckMonad a

Instances

Monad TypeCheckMonad

Methods

(>>=) :: TypeCheckMonad a -> (a -> TypeCheckMonad b) -> TypeCheckMonad b

(>>) :: TypeCheckMonad a -> TypeCheckMonad b -> TypeCheckMonad b

return :: a -> TypeCheckMonad a

fail :: String -> TypeCheckMonad a

Functor TypeCheckMonad

Methods

fmap :: (a -> b) -> TypeCheckMonad a -> TypeCheckMonad b

(<$) :: a -> TypeCheckMonad b -> TypeCheckMonad a

Applicative TypeCheckMonad

Methods

pure :: a -> TypeCheckMonad a

(<*>) :: TypeCheckMonad (a -> b) -> TypeCheckMonad a -> TypeCheckMonad b

liftA2 :: (a -> b -> c) -> TypeCheckMonad a -> TypeCheckMonad b -> TypeCheckMonad c

(*>) :: TypeCheckMonad a -> TypeCheckMonad b -> TypeCheckMonad b

(<*) :: TypeCheckMonad a -> TypeCheckMonad b -> TypeCheckMonad a

runTCM :: TypeCheckMonad a -> Input -> TypeCheckMode -> Either TypeCheckError a

unTCM :: TypeCheckMonad a -> Ctx -> Input -> TypeCheckMode -> Either TypeCheckError a

data TypeCheckMode

Constructors

StrictMode

LaxMode

UnsafeMode

Instances

Read TypeCheckMode

Methods

readsPrec :: Int -> ReadS TypeCheckMode

readList :: ReadS [TypeCheckMode]

readPrec :: ReadPrec TypeCheckMode

readListPrec :: ReadPrec [TypeCheckMode]

Show TypeCheckMode

Methods

showsPrec :: Int -> TypeCheckMode -> ShowS

show :: TypeCheckMode -> String

showList :: [TypeCheckMode] -> ShowS

Type checking itself

inferable :: AST -> Bool

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

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 :: [Hakaru] -> Hakaru -> *)

• Terms whose type is existentially quantified packed with a singleton for the type.

The e' ∈ τ portion of the inference judgement.

Constructors

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

Instances

Show2 abt => Show (TypedAST abt)

Methods

showsPrec :: Int -> TypedAST abt -> ShowS

show :: TypedAST abt -> String

showList :: [TypedAST abt] -> ShowS

onTypedAST :: (forall b. abt '[] b -> abt '[] b) -> TypedAST abt -> TypedAST abt

onTypedASTM :: Functor m => (forall b. abt '[] b -> m (abt '[] b)) -> TypedAST abt -> m (TypedAST abt)

elimTypedAST :: (forall b. Sing b -> abt '[] b -> x) -> TypedAST abt -> x

inferType :: forall abt. ABT Term abt => AST -> TypeCheckMonad (TypedAST abt)

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)

Given a typing environment, a type, and a term, verify that the term satisfies the type (and produce an elaborated term):

Γ ⊢ τ ∋ e ⇒ e'