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 :: UncheckedExp -> 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.

checkFunDef :: (Name, Maybe UncheckedTypeExp, [UncheckedTypeParam], [UncheckedPattern], UncheckedExp, SrcLoc) -> TypeM (VName, [TypeParam], [Pattern], Maybe (TypeExp VName), StructType, [VName], 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.