Safe Haskell	Safe-Inferred
Language	Haskell2010

Language.Drasil.WellTyped

Synopsis

type TypeError = String
type TypingContext t = Map UID t
inferFromContext :: TypingContext t -> UID -> Either t TypeError
class (Eq t, Show t) => Typed e t where
- infer :: TypingContext t -> e -> Either t TypeError
- check :: TypingContext t -> e -> t -> Either t TypeError
class Typed e t => RequiresChecking c e t where
- requiredChecks :: c -> [(e, t)]
typeCheckByInfer :: Typed e t => TypingContext t -> e -> t -> Either t TypeError
allOfType :: Typed e t => TypingContext t -> [e] -> t -> t -> TypeError -> Either t TypeError
temporaryIndent :: String -> String -> String

Documentation

type TypeError = String Source #

type TypingContext t = Map UID t Source #

We can only type check UIDs within a type context relating UIDs to types since they don't carry any type information.

inferFromContext :: TypingContext t -> UID -> Either t TypeError Source #

Look for a known type of a specific UID.

class (Eq t, Show t) => Typed e t where Source #

Build a bidirectional type checker for your expression language, e, with respect to a specific type universe, t.

Methods

infer :: TypingContext t -> e -> Either t TypeError Source #

Given a typing context and an expression, infer a unique type or explain what went awry.

check :: TypingContext t -> e -> t -> Either t TypeError Source #

Given a typing context, an expression, and an expected type, check if the expression can satisfy the expectation.

Instances

Instances details

Typed Expr Space Source #
Instance details Defined in Language.Drasil.Expr.Lang Methods infer :: TypingContext Space -> Expr -> Either Space TypeError Source # check :: TypingContext Space -> Expr -> Space -> Either Space TypeError Source #
Typed Literal Space Source #
Instance details Defined in Language.Drasil.Literal.Lang Methods infer :: TypingContext Space -> Literal -> Either Space TypeError Source # check :: TypingContext Space -> Literal -> Space -> Either Space TypeError Source #

class Typed e t => RequiresChecking c e t where Source #

For all containers, c, which contain typed expressions, e, against a specific type universe, t, expose all expressions and relations that need to be type-checked.

Methods

requiredChecks :: c -> [(e, t)] Source #

All things that need type checking.

Instances

Instances details

RequiresChecking DifferentialModel Expr Space Source #
Instance details Defined in Language.Drasil.Chunk.DifferentialModel Methods requiredChecks :: DifferentialModel -> [(Expr, Space)] Source #
RequiresChecking (QDefinition Expr) Expr Space Source #
Instance details Defined in Language.Drasil.Chunk.Eq Methods requiredChecks :: QDefinition Expr -> [(Expr, Space)] Source #

typeCheckByInfer :: Typed e t => TypingContext t -> e -> t -> Either t TypeError Source #

`Check' an expressions type based by an inference.

allOfType :: Typed e t => TypingContext t -> [e] -> t -> t -> TypeError -> Either t TypeError Source #

temporaryIndent :: String -> String -> String Source #

A temporary, hacky, indentation function. It should be removed when we switch to using something else for error messages, which can be later formatted nicely.