The following defines various Futhark-specific terms used in the documentation and in compiler output.
- Abstract type¶
A type whose definition has been hidden through a module ascription.
The aliases of a variable is a set of those other variables with which it might be aliased.
Whether two values might potentially share the same memory at run-time. Clearly, after
let y = x,
yare aliased. Also, the slice
x[i:j]is also aliased with
x. Aliasing is used to type-check In-place Updates.
- Anonymous size¶
Auxiliary information attached to an expression or declaration, which the compiler or other tool might use for various purposes. See Attributes.
Shorthand for a Size coercion.
- Compiler backend¶
A Futhark compiler backend is technically only responsible for the final compilation result, but from the user’s perspective is also coupled with a compiler pipeline. The backend corresponds to compiler subcommand, such as
futhark multicore, etc.
- Compiler frontend¶
The part of the compiler responsible for reading code from files, parsing it, and type checking it.
- Compiler pipeline¶
The series of compiler passes that lie between the compiler frontend and the compiler backend. Responsible for the majority of program optimisations. In principle the pipeline could be configurable, but in practice each backend is coupled with a specific pipeline.
- Constructive use¶
nis used constructively in a type if it is used as the size of an array at least once outside of any function arrows. For example, the following types use
([n]bool, bool -> [n]bool)
The following do not:
bool -> [n]bool
[n]bool -> bool
If a value is passed for a consuming function parameter, that value may no longer be used. We say that a an expression is with consumption if any values are consumed in the expression. This is banned in some cases where that expression might otherwise be evaluated multiple times. See In-place Updates.
- Data parallelism¶
A program transformation always performed by the Futhark compiler, that replaces function values with non-function values. The goal is to avoid having indirect calls through function pointers at run-time. To permit zero-overhead defunctionalisation, the Futhark type rules impose restrictions on lifted types.
A program transformation always performed by the Futhark compiler, that compiles away modules using an approach similar to defunctionalisation. This makes using e.g. a parametric module completely free at run-time.
The process conducted out by the type checker, where it infers and inserts information not explicitly provided in the program. The most important part of this is type inference, but also includes various other things.
- Existential size¶
An existential size is a size that is bound by the existential quantifier
?in the same type. For example, in a type
[n]bool -> ?[m].[m]bool, the size
mis existential. When such a function is applied, each existential size is instantiated as an unknown size.
The Standard ML term for what Futhark calls a parametric module.
- GPU backend¶
A compiler backend that ultimately produces GPU code. The backends
gpuare GPU backends. These have more restrictions than some other backends, particularly with respect to irregular nested data parallelism.
- Higher-ranked type¶
- In-place updates¶
A somewhat misleading term for the syntactic forms
x with [i] = vand
let x[i] = v. These are not semantic in-place updates, but can be operationally understood as thus. See In-place Updates.
- Irrefutable pattern¶
- Irregular array¶
An array where the elements do not have the same size. For example,
[, [2,3]is irregular. These are not supported in Futhark.
- Irregular memory allocation¶
A situation that occurs when the generated code has to allocate memory inside of an instance of nested data parallelism, where the amount to allocate is variant to the outer parallel levels. As a contrived example (that the actual compiler would just optimise away), consider:
map (\n -> let A = iota n in A) ns
To construct the array
Ain memory, we require
nis not known until we start executing the body of the
map. While such simple cases are handled, more complicated ones that involve nested sequential loops are not supported by the GPU backends.
- Irregular nested data parallelism¶
An instance of nested data parallelism, where the parallel width of inner parallelism is variant to the outer parallelism. For example, the following expression exhibits irregular nested data parallelism:
map (\n -> reduce (+) 0 (iota n)) ns
Because the width of the inner
n, and every iteration of the outer
maphas a (potentially) different
n. The Futhark GPU backends currently do not support irregular nested data parallelism well, and will usually sequentialise the irregular loops. In cases that require an irregular memory allocation, the compiler may entirely fail to generate code.
- Lifted type¶
A mapping from names to definitions of types, values, or nested modules. See Modules.
- Module ascription¶
- Module expression¶
- Module type¶
- Module type expression¶
An expression that is evaluated during type-checking to a module type.
A program transformation that instantiates a copy of each polymorphic functions for each type it is used with. Performed by the Futhark compiler.
A lexical token consisting of alphanumeric characters and underscores, for example
do_it. Most variables are names. See also symbol.
- Nested data parallelism¶
Nested data parallelism occurs when a parallel construct is used inside of another parallel construct. For example, a
reducemight be used inside a function passed to
- Parallel width¶
A somewhat informal term used to describe the size of an array on which we apply a SOAC. For example, if
map f xhas a parallel width of 1000. Intuitively, the “amount of processors” that would be needed to fully exploit the parallelism of the program, although nested data parallelism muddles the picture.
- Parametric module¶
A function from modules to modules. The most powerful form of abstraction provided by Futhark.
A syntactical construct for decomposing a value into its consituent parts. Patterns are used in function parameters,
match. See Patterns.
- Polymorphic function¶
The concept of being polymorphic.
A function that calls itself. Currently not supported in Futhark.
- Refutable pattern¶
A pattern that does does not match all possible values. For example, the pattern
(1,x)matches only tuples where the first element is
1. These may not be used in
letexpressions or in function parameters. See also irrefutable pattern.
- Regular nested data parallelism¶
The symbolic size of an array dimension or abstract type.
- Size argument¶
- Size expression¶
An expression that occurs as the size of an array or size argument. For example, in the type
x+2is a size expression. Size expressions can occur syntactically in source code, or due to parameter substitution when applying a size-dependent function.
- Size parameter¶
A parameter of a polymorphic function or type constructor that ranges over sizes. These are written as [n] for some n, after which n is in scope as a term of type
i64within the rest of the definition. Do not confuse them with type parameters.
- Size types¶
- Size-dependent types¶
An umbrella term for the part of Futhark’s type system that tracks array sizes. See Size Types.
- Size-dependent function¶
A function where the size of the result depends on the values of the parameters. The function
iotais perhaps the simplest example.
- Size-lifted type¶
- Second Order Array Combinator¶
A term covering the main parallel building blocks provided by Futhark: functions such as
scan, and so on. They are second order because they accept a functional argument, and so permit nested data parallelism.
A lexical token that consts of symbolic (non-alphabetic characters), and can be bound to a value. Infix operators such as
/are symbols. See also name.
A classification of values.
i32are examples of types.
- Type abbreviation¶
A shorthand for a longer type, e.g.
type t = i32. Can accept type parameters and size parameters. The definition is visible to users, unless hidden with a module ascription. See Type Abbreviations.
- Type argument¶
- Type constructor¶
A type abbreviation or abstract type that has at least one type parameter or size parameter. Futhark does not support higher-ranked types, so when referencing a type constructor in a type expression, you must provide corresponding type arguments and size arguments in an appopriate order.
- Type expression¶
- Type parameter¶
A parameter of a polymorphic function or type constructor that ranges over types. These are written as ‘t for some t, after which t is in scope as a type within the rest of the definition. Do not confuse them with size parameters.
- Uniqueness types¶
A somewhat misleading term that describes Futhark’s system of allowing consumption of values, in the interest of allowing in-place updates. The only place where uniqueness truly occurs is in return types, where e.g. the return type of
copyis unique to indicate that the result does not alias the argument.
- Unknown size¶
A size produced by invoking a function whose result type contains an existentially quantified size, such as
filter, or because the original size expression involves variables that have gone out of scope.
An object such as the integer
123or the array
[1,2,3]. Expressions variables are bound to values and all valid expressions have a type describing the form of values they can return.
When some value
vcomputed inside a loop takes a different value for each iteration inside the loop, we say that
vis variant to the loop (and otherwise invariant). Often used to talk about irregularity. When something is nested inside multiple loops, it may be variant to just one of them.