Support arbitrary size expressions

Futhark is basically dependently typed now.  Some work remains to be done, but this is surprisingly useful already.

Closes #1659.

docs/error-index.rst

@@ -267,6 +267,44 @@ not any free variables.  Use ``copy`` to fix this:
 
   def f () = copy x
 
+.. _size-expression-bind:
+
+"Size expression with binding is replaced by unknown size."
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+To illustrate this error, consider the following program
+
+.. code-block:: futhark
+
+   def main (xs: *[]i64) =
+     let a = iota (let n = 10 in n+n)
+     in ...
+
+Intuitively, the type of ``a`` should be ``[let n = 10 in n+n]i32``,
+but this puts a binding into a size expression, which is invalid.
+Therefore, the type checker invents an :term:`unknown size`
+variable, say ``l``, and assigns ``a`` the type ``[l]i32``.
+
+.. _size-expression-consume:
+
+"Size expression with consumption is replaced by unknown size."
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+To illustrate this error, consider the following program
+
+.. code-block:: futhark
+
+   def consume (xs: *[]i64): i64 = xs[0]
+
+   def main (xs: *[]i64) =
+     let a = iota (consume xs)
+     in ...
+
+Intuitively, the type of ``a`` should be ``[consume ys]i32``, but this
+puts a consumption of the array ``ys`` into a size expression, which
+is invalid.  Therefore, the type checker invents an :term:`unknown
+size` variable, say ``l``, and assigns ``a`` the type ``[l]i32``.
+
 .. _inaccessible-size:
 
 "Parameter *x* refers to size *y* which will not be accessible to the caller
@@ -385,7 +423,7 @@ into a separate ``let``-binding preceding the problematic expressions.
 
 This error occurs when you define a function that can never be
 applied, as it requires an input of a specific size, and that size is
-not known.  Somewhat contrived example:
+an :term:`unknown size`.  Somewhat contrived example:
 
 .. code-block:: futhark
 
@@ -471,8 +509,9 @@ use of either pipelining or composition.
 "Existential size *n* not used as array size"
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-This error occurs for type expressions that use explicit existential
-quantification in an incorrect way, such as the following examples:
+This error occurs for type expressions that bind an existential size
+for which there is no :term:`constructive use`, such as in the
+following examples:
 
 .. code-block:: futhark
 
@@ -481,12 +520,12 @@ quantification in an incorrect way, such as the following examples:
   ?[n].bool -> [n]bool
 
 When we use existential quantification, we are required to use the
-size within its scope, *and* it must not exclusively be used to the
-right of function arrow.
+size constructively within its scope, *in particular* it must not be
+exclusively as the parameter or return type of a function.
 
 To understand the motivation behind this rule, consider that when we
-use an existential quantifier we are saying that there is *some size*,
-it just cannot be known statically, but must be read from some value
+use an existential quantifier we are saying that there is *some size*.
+The size is not known statically, but must be read from some value
 (i.e. array) at runtime.  In the first example above, the existential
 size ``n`` is not used at all, so the actual value cannot be
 determined at runtime.  In the second example, while an array
@@ -943,3 +982,41 @@ ordinary parameter:
 .. code-block:: futhark
 
    entry f (n: i64) : [0][n]i32 = []
+
+.. _nonconstructive-entry:
+
+"Entry point size parameter [n] only used non-constructively."
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+This error occurs for programs such as the following::
+
+.. code-block:: futhark
+
+   entry main [x] (A: [x+1]i32) = ...
+
+The size parameter ``[x]`` is only used in an size expression ``x+1``,
+rather than directly as an array size.  This is allowed for ordinary
+functions, but not for entry points.  The reason is that entry points
+are not subject to ordinary type inference, as they are called from
+the external world, meaning that the value of the size parameter
+``[x]`` will have to be determined from the size of the array ``A``.
+This is in principle not a problem for simple sizes like ``x+1``, as
+it is obvious that ``x == length A - 1``, but in the general case it
+would require computing function inverses that might not exist.  For
+this reason, entry points require that all size parameters are used
+:term:`constructively<constructive use>`.
+
+As a workaround, you can rewrite the entry point as follows:
+
+.. code-block:: futhark
+
+   entry main [n] (A: [n]i32) =
+     let x = n-1
+     let A = A :> [x+1]i32
+     ...
+
+Or by passing the ``x`` explicitly:
+
+.. code-block:: futhark
+
+   entry main (x: i64) (A: [x+1]i32) = ...

docs/glossary.rst

@@ -73,11 +73,13 @@ documentation and in compiler output.
 
        * ``[n]bool``
        * ``([n]bool, bool -> [n]bool)``
+       * ``([n]bool, [n+1]bool)``
 
      The following do not:
 
        * ``[n+1]bool``
        * ``bool -> [n]bool``
+       * ``[n]bool -> bool``
 
    Consumption
 
@@ -296,6 +298,20 @@ documentation and in compiler output.
 
      The symbolic size of an array dimension or :term:`abstract type`.
 
+   Size expression
+
+     An expression that occurs as the size of an array or size
+     argument.  For example, in the type ``[x+2]i32``, ``x+2`` is a
+     size expression.  Size expressions can occur syntactically in
+     source code, or due to parameter substitution when applying a
+     :term:`size-dependent function`.
+
+   Size-dependent function
+
+     A function where the size of the result depends on the values of
+     the parameters.  The function ``iota`` is perhaps the simplest
+     example.
+
    Size types
    Size-dependent types
 
@@ -385,7 +401,9 @@ documentation and in compiler output.
    Unknown size
 
      A size produced by invoking a function whose result type contains
-     an existentially quantified size, such as ``filter``.
+     an existentially quantified size, such as ``filter``, or because
+     the original :term:`size expression` involves variables that have
+     gone out of scope.
 
    Value
 

prelude/array.fut

@@ -28,12 +28,12 @@ def last [n] 't (x: [n]t) = x[n-1]
 -- | Everything but the first element of the array.
 --
 -- **Complexity:** O(1).
-def tail [n] 't (x: [n]t) = x[1:]
+def tail [n] 't (x: [n]t): [n-1]t = x[1:]
 
 -- | Everything but the last element of the array.
 --
 -- **Complexity:** O(1).
-def init [n] 't (x: [n]t) = x[0:n-1]
+def init [n] 't (x: [n]t): [n-1]t = x[0:n-1]
 
 -- | Take some number of elements from the head of the array.
 --
@@ -43,12 +43,12 @@ def take [n] 't (i: i64) (x: [n]t): [i]t = x[0:i]
 -- | Remove some number of elements from the head of the array.
 --
 -- **Complexity:** O(1).
-def drop [n] 't (i: i64) (x: [n]t) = x[i:]
+def drop [n] 't (i: i64) (x: [n]t): [n-i]t = x[i:]
 
 -- | Split an array at a given position.
 --
 -- **Complexity:** O(1).
-def split [n] 't (i: i64) (xs: [n]t): ([i]t, []t) =
+def split [n] 't (i: i64) (xs: [n]t): ([i]t, [n-i]t) =
   (xs[0:i], xs[i:])
 
 -- | Return the elements of the array in reverse order.
@@ -62,10 +62,10 @@ def reverse [n] 't (x: [n]t): [n]t = x[::-1]
 -- **Work:** O(n).
 --
 -- **Span:** O(1).
-def (++) [n] [m] 't (xs: [n]t) (ys: [m]t): *[]t = intrinsics.concat xs ys
+def (++) [n] [m] 't (xs: [n]t) (ys: [m]t): *[n+m]t = intrinsics.concat xs ys
 
 -- | An old-fashioned way of saying `++`.
-def concat [n] [m] 't (xs: [n]t) (ys: [m]t): *[]t = xs ++ ys
+def concat [n] [m] 't (xs: [n]t) (ys: [m]t): *[n+m]t = xs ++ ys
 
 -- | Concatenation where the result has a predetermined size.  If the
 -- provided size is wrong, the function will fail with a run-time
@@ -123,7 +123,7 @@ def copy 't (a: t): *t =
 -- | Combines the outer two dimensions of an array.
 --
 -- **Complexity:** O(1).
-def flatten [n][m] 't (xs: [n][m]t): []t =
+def flatten [n][m] 't (xs: [n][m]t): [n*m]t =
   intrinsics.flatten xs
 
 -- | Like `flatten`@term, but where the final size is known.  Fails at
@@ -132,25 +132,25 @@ def flatten_to [n][m] 't (l: i64) (xs: [n][m]t): [l]t =
   flatten xs :> [l]t
 
 -- | Like `flatten`, but on the outer three dimensions of an array.
-def flatten_3d [n][m][l] 't (xs: [n][m][l]t): []t =
+def flatten_3d [n][m][l] 't (xs: [n][m][l]t): [n*m*l]t =
   flatten (flatten xs)
 
 -- | Like `flatten`, but on the outer four dimensions of an array.
-def flatten_4d [n][m][l][k] 't (xs: [n][m][l][k]t): []t =
+def flatten_4d [n][m][l][k] 't (xs: [n][m][l][k]t): [n*m*l*k]t =
   flatten (flatten_3d xs)
 
 -- | Splits the outer dimension of an array in two.
 --
 -- **Complexity:** O(1).
-def unflatten [p] 't (n: i64) (m: i64) (xs: [p]t): [n][m]t =
+def unflatten 't (n: i64) (m: i64) (xs: [n*m]t): [n][m]t =
   intrinsics.unflatten n m xs :> [n][m]t
 
 -- | Like `unflatten`, but produces three dimensions.
-def unflatten_3d [p] 't (n: i64) (m: i64) (l: i64) (xs: [p]t): [n][m][l]t =
+def unflatten_3d 't (n: i64) (m: i64) (l: i64) (xs: [n*m*l]t): [n][m][l]t =
   unflatten n m (unflatten (n*m) l xs)
 
 -- | Like `unflatten`, but produces four dimensions.
-def unflatten_4d [p] 't (n: i64) (m: i64) (l: i64) (k: i64) (xs: [p]t): [n][m][l][k]t =
+def unflatten_4d 't (n: i64) (m: i64) (l: i64) (k: i64) (xs: [n*m*l*k]t): [n][m][l][k]t =
   unflatten n m (unflatten_3d (n*m) l k xs)
 
 -- | Transpose an array.

src/Futhark/CLI/Dev.hs

@@ -76,7 +76,7 @@ data FutharkPipeline
     Defunctorise
   | -- | Defunctorise and monomorphise.
     Monomorphise
-  | -- | Defunctorise, monomorphise, and lambda-lift.
+  | -- | Defunctorise, monomorphise and lambda-lift.
     LiftLambdas
   | -- | Defunctorise, monomorphise, lambda-lift, and defunctionalise.
     Defunctionalise

src/Futhark/Doc/Generator.hs

@@ -541,8 +541,8 @@ prettyShape (Shape ds) =
   mconcat <$> mapM dimDeclHtml ds
 
 typeArgHtml :: TypeArg Size -> DocM Html
-typeArgHtml (TypeArgDim d _) = dimDeclHtml d
-typeArgHtml (TypeArgType t _) = typeHtml t
+typeArgHtml (TypeArgDim d) = dimDeclHtml d
+typeArgHtml (TypeArgType t) = typeHtml t
 
 modParamHtml :: [ModParamBase Info VName] -> DocM Html
 modParamHtml [] = pure mempty
@@ -706,8 +706,7 @@ relativise dest src =
   concat (replicate (length (splitPath src) - 1) "../") ++ dest
 
 dimDeclHtml :: Size -> DocM Html
-dimDeclHtml (NamedSize v) = brackets <$> qualNameHtml v
-dimDeclHtml (ConstSize n) = pure $ brackets $ toHtml (show n)
+dimDeclHtml (SizeExpr e) = pure $ brackets $ toHtml $ prettyString e
 dimDeclHtml AnySize {} = pure $ brackets mempty
 
 dimExpHtml :: SizeExp Info VName -> DocM Html

src/Futhark/IR/Parse.hs

@@ -12,7 +12,7 @@ where
 
 import Data.Char (isAlpha)
 import Data.Functor
-import Data.List (zipWith4)
+import Data.List (singleton, zipWith4)
 import Data.List.NonEmpty (NonEmpty (..))
 import Data.List.NonEmpty qualified as NE
 import Data.Set qualified as S
@@ -54,13 +54,13 @@ pName =
 pVName :: Parser VName
 pVName = lexeme $ do
   (s, tag) <-
-    satisfy constituent
+    choice [exprBox, singleton <$> satisfy constituent]
       `manyTill_` try pTag
       <?> "variable name"
-  pure $ VName (nameFromString s) tag
+  pure $ VName (nameFromString $ concat s) tag
   where
-    pTag =
-      "_" *> L.decimal <* notFollowedBy (satisfy constituent)
+    pTag = "_" *> L.decimal <* notFollowedBy (satisfy constituent)
+    exprBox = ("<{" <>) . (<> "}>") <$> (chunk "<{" *> manyTill anySingle (chunk "}>"))
 
 pBool :: Parser Bool
 pBool = choice [keyword "true" $> True, keyword "false" $> False]