A section on the module system.

Author: athas

futhark.tex

@@ -21,6 +21,7 @@
     val,
     while,
     with,
+    module,
   },
   sensitive=true, % keywords are not case-sensitive
   morecomment=[l]{--}, % l is for line comment

main.tex

@@ -1139,7 +1139,251 @@ \subsection{When To Use In-Place Updates}
 \section{Modules}
 \label{sec:modules}
 
-Yet to be written...
+When most programmers think of module systems, they think of rather
+utilitarian systems for namespace control and splitting programs
+across multiple files.  And in most languages, the module system is
+indeed little more than this.  But in Futhark, we have adopted an
+ML-style higher-order module system that permits \textit{abstraction}
+over modules.  The module system is not just a method for organising
+Futhark programs, but also the sole facility for writing generic code.
+
+\subsection{Simple Modules}
+
+At the most basic level, a \textit{module} (called a \textit{struct}
+in Standard ML) is merely a collection of declarations
+
+\begin{lstlisting}
+module AddI32 = {
+  type t = i32
+  fun add (x: t) (y: t): t = x + y
+  val zero: t = 0
+}
+\end{lstlisting}
+
+Now, \texttt{AddI32.t} is an alias for the type \texttt{i32}, and
+\texttt{Addi32.add} is a function that adds two values of type
+\texttt{i32}.  The only peculiar thing about this notation is the
+equal sign before the opening brace.  The declaration above is
+actually a combination of a *module binding*
+
+\begin{lstlisting}
+module ADDI32 = ...
+\end{lstlisting}
+
+And a \textit{module expression}
+
+\begin{lstlisting}
+{
+  type t = i32
+  fun add (x: t) (y: t): t = x + y
+  val zero: t = 0
+}
+\end{lstlisting}
+
+In this case, the module expression is just some declarations enclosed
+in curly braces.  But, as the name suggests, a module expression is
+just some expression that returns a module.  A module expression is
+syntactically and conceptually distinct from a regular value
+expression, but serves much the same purpose.  The module language is
+designed such that evaluation a module expression can always be done
+at compile time.
+
+Apart from a sequence of declarations, a module expression can also be
+merely the name of another module
+
+\begin{lstlisting}
+module Foo = AddInt32
+\end{lstlisting}
+
+Now every name defined in \texttt{AddInt32} is also available in
+\texttt{Foo}.  At compile-time, only a single version of the
+\texttt{add} function is defined.
+
+\subsection{Module Types}
+
+What we have seen so far is nothing more than a simple namespacing
+mechanism.  The ML module system only becomes truly powerful once we
+introduce module types and parametric modules (in Standard ML, these
+are called \textit{signatures} and \textit{functors}).
+
+A module type is the counterpart to a value type.  It describes which
+names are defined, and as what.  We can define a module type that
+describes \texttt{AddInt32}
+
+\begin{lstlisting}
+module type Int32Adder = {
+  type t = i32
+  val add: t -> t -> t
+  val zero: t
+}
+\end{lstlisting}
+
+As with modules, we have the notion of a \textit{module type expression}.  In
+this case, the module type expression is a sequence of \textit{specs}
+enclosed in curly braces.  A spec is a requirement of how some name
+must be defined: as a value (including functions) of some type, as a
+type abbreviation, or as an abstract type (which we will return to
+later).
+
+We can assert that some module implements a specific module type via
+module type ascription
+
+\begin{lstlisting}
+module Foo = AddInt32 : Int32Adder
+\end{lstlisting}
+
+Syntactical sugar that allows us to move the module type to the left
+of the equal sign makes a common case look smoother
+
+\begin{lstlisting}
+module AddInt32: Int32Adder = {
+  ...
+}
+\end{lstlisting}
+
+When we are ascribing a module with a module type, the module type
+functions as a filter, removing anything not explicitly mentioned in
+the module type
+
+\begin{lstlisting}
+module Bar = AddInt32 : { type t = int
+                          val zero: t }
+\end{lstlisting}
+
+An attempt to access \texttt{Bar.add} will result in a compilation
+error, as the ascription has hidden it.  This is known as an
+\textit{opaque} ascription, because it obscures anything not
+explicitly mentioned in the module type.  The module systems in
+Standard ML and OCaml support both opaque and \textit{transparent}
+ascription, but in Futhark we support only the former.  This example
+also demonstrates the use of an anonymous module type.  Module types
+work much like structural types known from e.g. Go ("compile-time duck
+typing"), and are named only for convenience.
+
+We can use type ascription with abstract types to hide the definition
+of a type from the users of a module
+
+\begin{lstlisting}
+module Speeds: { type thing
+                 val car: thing
+                 val plane: thing
+                 val futhark: thing
+                 val speed: thing -> int } = {
+  type thing = int
+
+  val car: thing = 0
+  val plane: thing = 1
+  val futhark: thing = 2
+
+  fun speed (x: thing): int =
+    if      x == car     then 120
+    else if x == plane   then 800
+    else if x == futhark then 10000
+    else                      0 -- will never happen
+}
+\end{lstlisting}
+
+The (anonymous) module type asserts that a distinct type \texttt{thing}
+must exist, but does not mention its definition.  There is no way for
+a user of the \texttt{Speeds} module to do anything with a value of type
+\texttt{Speeds.thing} apart from passing it to \texttt{Speeds.speed} (except
+putting it in an array or tuple, or returning it from a function).
+Its definition is entirely abstract.  Furthermore, no values of type
+\texttt{Speeds.thing} exist except those that are created by the \texttt{Speeds}
+module.
+
+\subsection{Parametric Modules}
+
+While module types serve some purpose for namespace control and
+abstraction, their most interesting use is in the definition of
+parametric modules.  A parametric module is conceptually
+equivalent to a function.  Where a function takes a value as input and
+produces a value, a parametric module takes a module and produces a
+module.  For example, given a module type
+
+\begin{lstlisting}
+module type Monoid = {
+  type t
+  val add: t -> t -> t
+  val zero: t
+}
+\end{lstlisting}
+
+We can define a parametric module that accepts a module satisfying
+the \texttt{Monoid} module type, and produces a module containing a
+function for collapsing an array
+
+\begin{lstlisting}
+module Sum(M: Monoid) = {
+  fun sum (a: []M.t): M.t =
+    reduce M.add M.zero a
+}
+\end{lstlisting}
+
+There is an implied assumption here, which is not captured by the type
+system: the function \texttt{add} must be associative and have
+\texttt{zero} as its neutral element.  These constraints are from the
+parallel semantics of \texttt{reduce}, and the algebraic concept of a
+\textit{monoid}.  Note that in \texttt{Monoid}, no definition is given
+of the type \texttt{t} - we only assert that there must be some type
+\texttt{t}, and that certain operations are defined for it.
+
+We can use the parametric module \texttt{Sum} thus
+
+\begin{lstlisting}
+  module SumI32s = Sum(AddInt32)
+\end{lstlisting}
+
+We can now refer to the function \texttt{SumI32s.sum}, which has type
+\texttt{[]i32 -> i32}.  The type is only abstract inside the definition of
+the parametric module.  We can instantiate \texttt{Sum} again with
+another module; this one anonymous
+
+\begin{lstlisting}
+module Prod64s = Sum({
+  type t = 64
+  fun (x: f64) (y: f64): f64 = x * y
+  fun zero: f64 = 1.0
+})
+\end{lstlisting}
+
+The function \texttt{Prodf64s.sum} has type \texttt{[]f64 -> f64}, and computes
+the product of an array of numbers (we should probably have picked a
+more generic name than \texttt{sum} for this function).
+
+Operationally, each application of a parametric module results in
+its definition being duplicated and references to the module parameter
+replace by references to the concrete module argument.  This is quite
+similar to how C++ templates are implemented.  Indeed, parametric
+modules can be seen as a simplified variant with no specialisation,
+and with module types to ensure rigid type checking.  In C++, a
+template is type-checked when it is instantiated, whereas a
+parametric module is type-checked when it is defined.
+
+Parametric modules, like other modules, can contain more than one
+declaration.  This is useful for giving related functionality a common
+abstraction, for example to implement linear algebra operations that
+are polymorphic over the type of scalars.  This example uses an
+anonymous module type for the module parameter, and the \texttt{open}
+declaration, which brings the names from a module into the current
+scope
+
+\begin{lstlisting}
+  module Linalg(M: {
+    type scalar
+    val zero: scalar
+    val add: scalar -> scalar -> scalar
+    val mul: scalar -> scalar -> scalar
+  }) = {
+    open M
+
+    fun dotprod (xs: [n]scalar) (ys: [n]scalar): scalar =
+      reduce add zero (zipWith mul xs ys)
+
+    fun matmul (xss: [n][p]scalar) (yss: [p][m]scalar): [n][m]scalar =
+      map (\xs -> map (dotprod xs) (transpose yss)) xss
+  }
+\end{lstlisting}
 
 \section{Benchmarking}
 \label{sec:benchmarking}
@@ -2413,4 +2657,5 @@ \chapter{Tool References}
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
+%%% TeX-engine: luatex
 %%% End: