| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Language.Futhark.TypeChecker.Terms
Description
Facilities for type-checking Futhark terms. Checking a term requires a little more context to track consumption and such.
Type inference is implemented through a variation of Hindley-Milner. The main complication is supporting the rich number of built-in language constructs, as well as consumption and freshness. This is mostly done in an ad hoc way, and many programs will require the programmer to fall back on type annotations.
The strategy is to split type checking into sveral (main) passes:
1) A size-agnostic pass implemented in Language.Futhark.TypeChecker.Terms.Unsized.
2) Pass (1) has given us a program where we know the types of everything, but the sizes of nothing. Pass (2) then does essentially size inference, with the benefit of already knowing the full unsized type of everything. This is done using a syntax-driven approach, similar to Algorithm W.
3) The program is then checked for violation of the consumption and freshness rules, which is implemented in Language.Futhark.TypeChecker.Consumption.
Synopsis
- checkOneExp :: ExpBase (NoInfo :: Type -> Type) VName -> TypeM ([TypeParam], Exp)
- checkSizeExp :: ExpBase (NoInfo :: Type -> Type) VName -> TypeM Exp
- checkFunDef :: (VName, Maybe (TypeExp (ExpBase (NoInfo :: Type -> Type) VName) VName), [TypeParam], [PatBase (NoInfo :: Type -> Type) VName ParamType], ExpBase (NoInfo :: Type -> Type) VName, SrcLoc) -> TypeM ([TypeParam], [Pat ParamType], Maybe (TypeExp Exp VName), ResRetType, Exp)
Documentation
checkOneExp :: ExpBase (NoInfo :: Type -> Type) VName -> TypeM ([TypeParam], Exp) Source #
Type-check a single expression in isolation. This expression may turn out to be polymorphic, in which case the list of type parameters will be non-empty.
checkSizeExp :: ExpBase (NoInfo :: Type -> Type) VName -> TypeM Exp Source #
Type-check a single size expression in isolation. This expression may turn out to be polymorphic, in which case it is unified with i64.
checkFunDef :: (VName, Maybe (TypeExp (ExpBase (NoInfo :: Type -> Type) VName) VName), [TypeParam], [PatBase (NoInfo :: Type -> Type) VName ParamType], ExpBase (NoInfo :: Type -> Type) VName, SrcLoc) -> TypeM ([TypeParam], [Pat ParamType], Maybe (TypeExp Exp VName), ResRetType, Exp) Source #
Type-check a top-level (or module-level) function definition. Despite the name, this is also used for checking constant definitions, by treating them as 0-ary functions.