Language.Futhark.TypeChecker.Terms

Facilities for type-checking Futhark terms. Checking a term requires a little more context to track uniqueness 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 uniqueness types. This is mostly done in an ad hoc way, and many programs will require the programmer to fall back on type annotations.

Documentation

checkOneExp :: ExpBase NoInfo VName -> TypeM ([TypeParam], Exp)

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 VName -> TypeM Exp

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 VName) VName), [TypeParam], [PatBase NoInfo VName ParamType], ExpBase NoInfo VName, SrcLoc) -> TypeM ([TypeParam], [Pat ParamType], Maybe (TypeExp Exp VName), ResRetType, Exp)

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.