Safe Haskell	None
Language	Haskell2010

Control.Typecheckable

Contents

Typeclasses for Typechecking and Inference
Typing context and Type error structures
- General use
- ErrorContext

Description

Module containing typechecking functions and data structures.

Synopsis

Typeclasses for Typechecking and Inference

class Typecheckable term t where Source #

A typeclass for typechecking terms (term) with a typesystem (t).

Minimal complete definition

typecheck

Associated Types

type TypingContext term t :: * Source #

The typing context, in type theory this is usually shown as 𝚪.

For a basic typechecker of the simply-typed lambda calculus this might contain a mapping of variable and constant names to their types. This is left to be defined for the implementer though as other typesystems might need extra information in their contexts.

type TypeError term t :: * Source #

The type error representation.

Methods

typecheck :: TypingContext term t -> term t -> Either [TypeError term t] (TypingContext term t, t) Source #

Given a typing context, typecheck an expression and either return a typeerror or the type of the expression that was passed.

Instances

(Ord m, Ord c, Ord v) => Typecheckable (LambdaTerm c v) (SimplyTyped m) Source #
Associated Types type TypingContext (LambdaTerm c v :: * -> ) (SimplyTyped m) :: Source # type TypeError (LambdaTerm c v :: * -> ) (SimplyTyped m) :: Source # Methods typecheck :: TypingContext (LambdaTerm c v) (SimplyTyped m) -> LambdaTerm c v (SimplyTyped m) -> Either [TypeError (LambdaTerm c v) (SimplyTyped m)] (TypingContext (LambdaTerm c v) (SimplyTyped m), SimplyTyped m) Source #
(Ord c, Ord v, Ord m, Ord p) => Typecheckable (LambdaTerm c v) (SystemF m p) Source #
Associated Types type TypingContext (LambdaTerm c v :: * -> ) (SystemF m p) :: Source # type TypeError (LambdaTerm c v :: * -> ) (SystemF m p) :: Source # Methods typecheck :: TypingContext (LambdaTerm c v) (SystemF m p) -> LambdaTerm c v (SystemF m p) -> Either [TypeError (LambdaTerm c v) (SystemF m p)] (TypingContext (LambdaTerm c v) (SystemF m p), SystemF m p) Source #

class Typecheckable term t => Inferable term t where Source #

Minimal complete definition

infer, typingContext

Associated Types

type InferenceContext term t :: * Source #

The inference context, has a similar function to TypingContext

type InferError term t :: * Source #

The inference error representation.

Methods

infer :: InferenceContext term t -> term (Maybe t) -> Either [InferError term t] (InferenceContext term t, term t) Source #

typingContext :: InferenceContext term t -> TypingContext term t Source #

Get a typing context from an inference context.

Typing context and Type error structures

General use

type Typecheck term t = ExceptT [TypeError term t] (State (TypingContext term t)) Source #

Typechecking type, uses the TypingContext as state and TypeError as an exception type.

runTypecheck :: st -> ExceptT e (State st) t -> Either e (st, t) Source #

runs a Typecheck action

expression :: forall env expr err expr. Lens (ErrorContext env expr err) (ErrorContext env expr err) [expr] [expr] Source #

environment :: forall env expr err env. Lens (ErrorContext env expr err) (ErrorContext env expr err) env env Source #

(<><>) :: (Semigroup s1, Semigroup s2) => Either s1 s2 -> Either s1 s2 -> Either s1 s2 Source #

A validation semigroup on Eithers, combining Left values when two appear.

ErrorContext

data ErrorContext env expr err Source #

Data type for an error context, holding the expression where the error occurred, the environment when it did, and the error itself.

Constructors

ErrorContext
Fields _expression :: [expr] A stack of expressions leading the the expression that caused the error as the final element. _environment :: env The environment's state at the time of error. _errorOfContext :: err The error that occurred.

Instances

Functor (ErrorContext env expr) Source #
Methods fmap :: (a -> b) -> ErrorContext env expr a -> ErrorContext env expr b # (<$) :: a -> ErrorContext env expr b -> ErrorContext env expr a #
(Eq env, Eq expr, Eq err) => Eq (ErrorContext env expr err) Source #
Methods (==) :: ErrorContext env expr err -> ErrorContext env expr err -> Bool # (/=) :: ErrorContext env expr err -> ErrorContext env expr err -> Bool #
(Ord env, Ord expr, Ord err) => Ord (ErrorContext env expr err) Source #
Methods compare :: ErrorContext env expr err -> ErrorContext env expr err -> Ordering # (<) :: ErrorContext env expr err -> ErrorContext env expr err -> Bool # (<=) :: ErrorContext env expr err -> ErrorContext env expr err -> Bool # (>) :: ErrorContext env expr err -> ErrorContext env expr err -> Bool # (>=) :: ErrorContext env expr err -> ErrorContext env expr err -> Bool # max :: ErrorContext env expr err -> ErrorContext env expr err -> ErrorContext env expr err # min :: ErrorContext env expr err -> ErrorContext env expr err -> ErrorContext env expr err #
(Show env, Show expr, Show err) => Show (ErrorContext env expr err) Source #
Methods showsPrec :: Int -> ErrorContext env expr err -> ShowS # show :: ErrorContext env expr err -> String # showList :: [ErrorContext env expr err] -> ShowS #

type ErrorContext' term t err = ErrorContext (TypingContext term t) (term t) err Source #

ErrorContext but the environment is assumed to be the TypingContext of t.

throwErrorContext :: (MonadError [ErrorContext env expr err] m, MonadState env m) => [expr] -> err -> m b Source #

Throw an error in an ErrorContext.

throwErrorContexts :: (MonadError (f (ErrorContext env expr err)) m, MonadState env m, Functor f) => f ([expr], err) -> m b Source #

Throw a list of errors in ErrorContext's.

errorOfContext :: forall env expr err err. Lens (ErrorContext env expr err) (ErrorContext env expr err) err err Source #

appendExprToEContexts :: (MonadError (f (ErrorContext env expr err)) m, Functor f) => expr -> m a -> m a Source #

If there have been any errors, add the given expression to the head of all the error contexts' expression stacks.