.. _glossary: Glossary ======== The following defines various Futhark-specific terms used in the documentation and in compiler output. .. glossary:: :sorted: Abstract type A type whose definition has been hidden through a :term:`module ascription`. Aliases The *aliases* of a variable is a set of those other variables with which it might be :term:`aliased`. Aliasing Whether two values might potentially share the same memory at run-time. Clearly, after ``let y = x``, ``x`` and ``y`` are aliased. Also, the slice ``x[i:j]`` is also aliased with ``x``. Aliasing is used to type-check :ref:`in-place-updates`. Anonymous size In a type expression, a size of the form `[]`. Will be :term:`elaborated` to some name (possibly :term:`existentially bound`) by the type checker. Attribute Auxiliary information attached to an expression or declaration, which the compiler or other tool might use for various purposes. See :ref:`attributes`. Coercion Shorthand for a :ref:`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 :term:`compiler pipeline`. The backend corresponds to compiler subcommand, such as ``futhark c``, ``futhark cuda``, ``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 :term:`compiler frontend` and the :term:`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 A variable ``n`` is 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`` constructively: * ``[n]bool`` * ``([n]bool, bool -> [n]bool)`` The following do not: * ``[n+1]bool`` * ``bool -> [n]bool`` Consumption 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 :ref:`in-place-updates`. Data parallelism Performing the same operation on multiple elements of a collection, such as an array. The ``map`` :term:`SOAC` is the simplest example. This is the form of parallelism supported by Futhark. `See also Wikipedia `_. Defunctionalisation 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 :term:`lifted types `. Defunctorisation A program transformation always performed by the Futhark compiler, that compiles away modules using an approach similar to :term:`defunctionalisation`. This makes using e.g. a :term:`parametric module` completely free at run-time. Elaboration 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 ``m`` is existential. When such a function is applied, each existential size is instantiated as an :term:`unknown size`. Functor The Standard ML term for what Futhark calls a :term:`parametric module`. GPU backend A :term:`compiler backend` that ultimately produces GPU code. The backends ``opencl`` and ``gpu`` are GPU backends. These have more restrictions than some other backends, particularly with respect to :term:`irregular nested data parallelism`. Higher-ranked type A type that does not describe :term:`values `. Can be seen as a partially applied :term:`type constructor`. Not directly supported by Futhark, but a similar effect can be achieved through the :ref:`module-system`. In-place updates A somewhat misleading term for the syntactic forms ``x with [i] = v`` and ``let x[i] = v``. These are not semantic in-place updates, but can be operationally understood as thus. See :ref:`in-place-updates`. Invariant Not :term:`variant`. Irregular Something that is not regular. Usually used as shorthand for :term:`irregular nested data parallelism` or :term:`irregular array`. Irregular array An array where the elements do not have the same size. For example, ``[[1], [2,3]`` is irregular. These are not supported in Futhark. Irregular nested data parallelism An instance of :term:`nested data parallelism`, where the :term:`parallel width` of inner parallelism is :term:`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 ``reduce`` is ``n``, and every iteration of the outer ``map`` has a (potentially) different ``n``. The Futhark :term:`GPU backends` *currently* do not support irregular nested data parallelism well, and will usually sequentialise the irregular loops. In cases that require an :term:`irregular memory allocation`, the compiler may entirely fail to generate code. Irregular memory allocation A situation that occurs when the generated code has to allocate memory inside of an instance of :term:`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[10]) ns To construct the array ``A`` in memory, we require ``8n`` bytes, but ``n`` is 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 :term:`GPU backends`. Parametric module A function from :term:`modules` to modules. The most powerful form of abstraction provided by Futhark. Polymorphic Usually means a :term:`polymorphic function`, but sometimes a :term:`parametric modules `. Should not be used to describe a :term:`type constructor `. Polymorphism The concept of being :term:`polymorphic`. Polymorphic function A function with :term:`type parameters `, such that the function can be applied to arguments of various types. Compiled using :term:`monomorphisation`. Lifted type A type that may contain functions, including function types themselves. These have various restrictions on their use in order to support :term:`defunctionalisation`. See :ref:`hofs`. Module A mapping from names to definitions of types, values, or nested modules. See :ref:`module-system`. Module ascription A feature of the module system through which the contents of a module can be hidden. Written as ``m : mt`` where ``m`` is a :term:`module expression` and ``mt`` is a :term:`module type expression`. See :ref:`module-system`. Module expression An expression that is evaluated at compile time, through :term:`defunctorisation` to a :term:`module`. Most commonly just the name of a module. Module type A description of the interface of a :term:`module`. Most commonly used to hide contents in a :term:`module ascription` or to require implementation of an interface in a :term:`parametric module`. Module type expression An expression that is evaluated during type-checking to a :term:`module type`. Monomorphisation A program transformation that instantiates a copy of each :term:`polymorphic` functions for each type it is used with. Performed by the Futhark compiler. Nested data parallelism Nested :term:`data parallelism` occurs when a parallel construct is used inside of another parallel construct. For example, a ``reduce`` might be used inside a function passed to ``map``. Parallel width A somewhat informal term used to describe the size of an array on which we apply a :term:`SOAC`. For example, if ``x`` has type ``[1000]i32``, then ``map f x`` has a parallel width of 1000. Intuitively, the "amount of processors" that would be needed to fully exploit the parallelism of the program, although :term:`nested data parallelism` muddles the picture. Recursion A function that calls itself. Currently not supported in Futhark. Regular nested data parallelism An instance of :term:`nested data parallelism` that is not :term:`irregular`. Fully supports by any :term:`GPU backend`. Size The symbolic size of an array dimension or :term:`abstract type`. Size types Size-dependent types An umbrella term for the part of Futhark's type system that tracks array sizes. See :ref:`size-types`. Size-lifted type A type that may contain internal hidden sizes. These cannot be array elements, as that might potentially result in an :term:`irregular array`. See :ref:`typeabbrevs`. Size argument An argument to a :term:`type constructor` in a :term:`type expression` of the form ``[n]`` or ``[]``. The latter is called an :term:`anonymous size`. Must match a corresponding :term:`size parameter`. Size parameter A parameter of a :term:`polymorphic function` or :term:`type constructor` that ranges over :term:`sizes `. These are written as `[n]` for some `n`, after which `n` is in scope as a term of type ``i64`` within the rest of the definition. Do not confuse them with :term:`type parameters `. SOAC Second Order Array Combinator A term covering the main parallel building blocks provided by Futhark: functions such as ``map``, ``reduce``, ``scan``, and so on. They are *second order* because they accept a functional argument, and so permit :term:`nested data parallelism`. Type A classification of values. ``i32`` and ``[10]i32`` are examples of types. Type abbreviation A shorthand for a longer type, e.g. ``type t = [100]i32``. Can accept :term:`type parameters ` and :term:`size parameters `. The definition is visible to users, unless hidden with a :term:`module ascription`. See :ref:`typeabbrevs`. Type argument An argument to a :term:`type constructor` that is itself a :term:`type`. Must match a corresponding :term:`type parameter`. Type constructor A :term:`type abbreviation` or :term:`abstract type` that has at least one :term:`type parameter` or :term:`size parameter`. Futhark does not support :term:`higher-ranked types `, so when referencing a type constructor in a :term:`type expression`, you must provide corresponding :term:`type arguments ` and :term:`size arguments ` in an appopriate order. Type expression A syntactic construct that is evaluated to a :term:`type` in the type checker, but may contain uses of :term:`type abbreviations ` and :term:`anonymous sizes `. Type parameter A parameter of a :term:`polymorphic function` or :term:`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 :term:`size parameters `. Uniqueness types A somewhat misleading term that describes Futhark's system of allowing :term:`consumption` of values, in the interest of allowing :term:`in-place updates`. The only place where *uniqueness* truly occurs is in return types, where e.g. the return type of ``copy`` is *unique* to indicate that the result does not :term:`alias` the argument. Unknown size A size produced by invoking a function whose result type contains an existentially quantified size, such as ``filter``. Value An object such as the integer ``123`` or the array ``[1,2,3]``. Expressions variables are bound to values and all valid expressions have a :term:`type` describing the form of values they can return. Variant When some value ``v`` computed inside a loop takes a different value for each iteration inside the loop, we say that ``v`` is *variant* to the loop (and otherwise :term:`invariant`). Often used to talk about :term:`irregularity `. When something is nested inside multiple loops, it may be variant to just one of them.