Disco.Typecheck

Typecheck the Disco surface language and transform it into a type-annotated AST.

Documentation

containerTy :: Container -> Type -> Type

containerToCon :: Container -> Con

inferTelescope :: (Alpha b, Alpha tyb, Member (Reader TyCtx) r) => (b -> Sem r (tyb, TyCtx)) -> Telescope b -> Sem r (Telescope tyb, TyCtx)

Infer the type of a telescope, given a way to infer the type of each item along with a context of variables it binds; each such context is then added to the overall context when inferring subsequent items in the telescope.

checkModule :: Members '[Output Message, Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh] r => ModuleName -> Map ModuleName ModuleInfo -> Module -> Sem r ModuleInfo

Check all the types and extract all relevant info (docs, properties, types) from a module, returning a ModuleInfo record on success. This function does not handle imports at all; any imports should already be checked and passed in as the second argument.

makeTyDefnCtx :: Members '[Reader TyDefCtx, Error TCError] r => [TypeDefn] -> Sem r TyDefCtx

Turn a list of type definitions into a TyDefCtx, checking for duplicate names among the definitions and also any type definitions already in the context.

checkTyDefn :: Members '[Reader TyDefCtx, Error LocTCError] r => ModuleName -> TypeDefn -> Sem r ()

Check the validity of a type definition.

checkCyclicTy :: Members '[Reader TyDefCtx, Error TCError] r => Type -> Set String -> Sem r (Set String)

Check if a given type is cyclic. A type ty is cyclic if:

1. ty is the name of a user-defined type.
2. Repeated expansions of the type yield nothing but other user-defined types.
3. An expansion of one of those types yields another type that has been previously encountered.

In other words, repeatedly expanding the definition can get us back to exactly where we started.

The function returns the set of TyDefs encountered during expansion if the TyDef is not cyclic.

checkUnboundVars :: Members '[Reader TyDefCtx, Error TCError] r => TypeDefn -> Sem r ()

Ensure that a type definition does not use any unbound type variables or undefined types.

checkPolyRec :: Member (Error TCError) r => TypeDefn -> Sem r ()

Check for polymorphic recursion: starting from a user-defined type, keep expanding its definition recursively, ensuring that any recursive references to the defined type have only type variables as arguments.

filterDups :: Ord a => [a] -> [a]

Keep only the duplicate elements from a list.

>>> filterDups [1,3,2,1,1,4,2]
[1,2]

makeTyCtx :: Members '[Reader TyDefCtx, Error TCError] r => ModuleName -> [TypeDecl] -> Sem r TyCtx

Given a list of type declarations from a module, first check that there are no duplicate type declarations, and that the types are well-formed; then create a type context containing the given declarations.

checkCtx :: Members '[Reader TyDefCtx, Error TCError] r => TyCtx -> Sem r ()

Check that all the types in a context are valid.

checkDefn :: Members '[Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh, Output Message] r => ModuleName -> TermDefn -> Sem r Defn

Type check a top-level definition in the given module.

checkProperties :: Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output Message] r => Ctx Term Docs -> Sem r (Ctx ATerm [AProperty])

Given a context mapping names to documentation, extract the properties attached to each name and typecheck them.

checkProperty :: Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output Message] r => Property -> Sem r AProperty

Check the types of the terms embedded in a property.

checkPolyTyValid :: Members '[Reader TyDefCtx, Error TCError] r => PolyType -> Sem r ()

Check that a sigma type is a valid type. See checkTypeValid.

checkTypeValid :: Members '[Reader TyDefCtx, Error TCError] r => Type -> Sem r ()

Disco doesn't need kinds per se, since all types must be fully applied. But we do need to check that every type is applied to the correct number of arguments.

conArity :: Members '[Reader TyDefCtx, Error TCError] r => Con -> Sem r Int

data Mode

Typechecking can be in one of two modes: inference mode means we are trying to synthesize a valid type for a term; checking mode means we are trying to show that a term has a given type.

Constructors

Infer

Check Type

Instances

Show Mode

Defined in Disco.Typecheck

Methods

showsPrec :: Int -> Mode -> ShowS

show :: Mode -> String

showList :: [Mode] -> ShowS

check :: Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Term -> Type -> Sem r ATerm

Check that a term has the given type. Either throws an error, or returns the term annotated with types for all subterms.

This function is provided for convenience; it simply calls typecheck with an appropriate Mode.

checkPolyTy :: Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Term -> PolyType -> Sem r ATerm

Check that a term has the given polymorphic type.

infer :: Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Term -> Sem r ATerm

Infer the type of a term. If it succeeds, it returns the term with all subterms annotated.

This function is provided for convenience; it simply calls typecheck with an appropriate Mode.

inferTop :: Members '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r => Term -> Sem r (ATerm, PolyType)

Top-level type inference algorithm: infer a (polymorphic) type for a term by running type inference, solving the resulting constraints, and quantifying over any remaining type variables.

checkTop :: Members '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r => Term -> PolyType -> Sem r ATerm

Top-level type checking algorithm: check that a term has a given polymorphic type by running type checking and solving the resulting constraints.

typecheck :: Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Mode -> Term -> Sem r ATerm

The main workhorse of the typechecker. Instead of having two functions, one for inference and one for checking, typecheck takes a Mode. This cuts down on code duplication in many cases, and allows all the checking and inference code related to a given AST node to be placed together.

checkPattern :: Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Pattern -> Type -> Sem r (TyCtx, APattern)

Check that a pattern has the given type, and return a context of pattern variables bound in the pattern along with their types.

cAbs :: Members '[Writer Constraint, Fresh] r => Type -> Type -> Sem r ()

Constraints needed on a function type for it to be the type of the absolute value function.

cSize :: Members '[Writer Constraint, Fresh] r => Type -> Type -> Sem r ()

Constraints needed on a function type for it to be the type of the container size operation.

cPos :: Members '[Writer Constraint, Fresh] r => Type -> Sem r Type

Given an input type ty, return a type which represents the output type of the absolute value function, and generate appropriate constraints.

cInt :: Members '[Writer Constraint, Fresh] r => Type -> Sem r Type

Given an input type ty, return a type which represents the output type of the floor or ceiling functions, and generate appropriate constraints.

cExp :: Members '[Writer Constraint, Fresh] r => Type -> Type -> Sem r Type

Given input types to the exponentiation operator, return a type which represents the output type, and generate appropriate constraints.

getEltTy :: Members '[Writer Constraint, Fresh] r => Container -> Type -> Sem r Type

Get the argument (element) type of a (known) container type. Returns a fresh variable with a suitable constraint if the given type is not literally a container type.

ensureConstr :: forall r. Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Con -> Type -> Either Term Pattern -> Sem r [Type]

Ensure that a type's outermost constructor matches the provided constructor, returning the types within the matched constructor or throwing a type error. If the type provided is a type variable, appropriate constraints are generated to guarantee the type variable's outermost constructor matches the provided constructor, and a list of fresh type variables is returned whose count matches the arity of the provided constructor.

ensureConstr1 :: Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Con -> Type -> Either Term Pattern -> Sem r Type

A variant of ensureConstr that expects to get exactly one argument type out, and throws an error if we get any other number.

ensureConstr2 :: Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Con -> Type -> Either Term Pattern -> Sem r (Type, Type)

A variant of ensureConstr that expects to get exactly two argument types out, and throws an error if we get any other number.

ensureConstrMode :: Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Con -> Mode -> Either Term Pattern -> Sem r [Mode]

A variant of ensureConstr that works on Modes instead of Types. Behaves similarly to ensureConstr if the Mode is Check; otherwise it generates an appropriate number of copies of Infer.

ensureConstrMode1 :: Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Con -> Mode -> Either Term Pattern -> Sem r Mode

A variant of ensureConstrMode that expects to get a single Mode and throws an error if it encounters any other number.

ensureConstrMode2 :: Members '[Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r => Con -> Mode -> Either Term Pattern -> Sem r (Mode, Mode)

A variant of ensureConstrMode that expects to get two Modes and throws an error if it encounters any other number.

ensureEq :: Member (Writer Constraint) r => Type -> Type -> Sem r ()

Ensure that two types are equal: 1. Do nothing if they are literally equal 2. Generate an equality constraint otherwise