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)

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.