Dex is a functional, statically typed language for array processing.
Here we introduce the language in a tutorial format. We assume
reading familiarity with functional programming in the Haskell/ML style
and numerical programming in the NumPy/MATLAB style.
This is a literate program with outputs generated mechanically.
You can follow along in the REPL, `dex repl`

,
or, on Linux, in the live notebook: `dex web examples/tutorial.dx`

.
See the README for installation instructions.

## Expression syntax

We can evaluate and print expressions with `:p`

We can write let bindings as `x = <expr>; <expr>`

. Bindings can be separated
with a line break or a semicolon.

We also have lambda, tuple construction and (tuple) pattern-matching (destructuring):

We use white space for function application (we write `f x y`

instead of `f(x, y)`

).
To see how subexpressions are grouped, it can be helpful to pretty-print the
internal AST using `:parse`

. For example, we see that function application
associates to the left and binds more tightly than infix operators.

To reduce parentheses, we sometimes use `$`

for function application. `$`

binds
very loosely:

We can combine a let binding with a lambda expression, writing `f = lam x. <expr>`

as `f x = <expr>`

. This is just syntactic sugar. These three expression all parse
to exactly the same thing:

## Types

Why did we write `1. + 2.`

instead of just `1 + 2`

? Let's try that:

The problem is that `1`

is an integer whereas `+`

operates on reals. (Note that
Haskell overloads `+`

and literals using typeclasses. We could do the same,
but we're keeping it simple for now.) We can query the *type* of an
expression with `:t`

.

The type system is completely static. As a consequence, type errors appear at a function's call site rather than in its implementation.

The expressions we've seen so far have been *implicitly* typed. There have
been no type annotations at all. The Dex compiler fills in the types using
very standard Hindley-Milner-style type inference. The result of this process,
is an *explicitly* typed IR, similar to System F, in which all binders are
annotated. We can look at the explicitly typed IR with `:typed`

:

We can also add some explicit annotations if we like. Type inference then becomes type checking.

## Polymorphism and let generalization

Unusually for Hindley-Milner-style languages, user-supplied type annotation are
mandatory for let-bound *polymorphic* expressions. That is, we don't do let
generalization. For example, although we can write this:

It's an error to write this:

Instead, we have to give the type explicitly:

The motivation for this choice is a bit subtle. It's related to the reasons for Haskell's ("dreaded") monomorphism restriction: automatic let generalization can lead to surprising runtime work duplication in the presence of polymorphism that's not purely parametric. We'll say more about it later, when we discuss index sets as types.

In the explicitly typed IR, polymorphism is represented by functions which
take types as arguments. Explicit types are supplied at call sites, as in
`myid @Int 1`

above. This type application is available (but optional) in the
source language too.

Generally, a design goal has been to make sure that all well-typed terms in the explicitly typed IR can be written in the source langauge too.

## Tables (arrays)

The central data structure in Dex is the "table". We could also call it an "vector" or "array" and we'll use these terms interchangeably. A table is a mapping from indices to elements. We can build one like this:

Notice its type, `(3=>Int)`

. Here `3`

is a *type* representing the index set
`{0, 1, 2}`

. The `=>`

arrow is the type constructor for table types. A table
`a=>b`

is a mapping from the index set `a`

to the element type `b`

. Our
particular table, `[10,20,30]`

, maps `0`

to `10`

, `1`

to `20`

and `2`

to `30`

.

Index set types are quite constrainted, as we'll see later, but elements can be any type, including tables. We can construct a two-dimensional table as a table of tables:

Notice rectangularity is enforced by the type system. The elements of the
outer table all have the same type `3=>Int`

and therefore the same size. We'll
get a type error if we try to construct a non-rectangular two-dimensional table:

This has an important consequence for the implementation: the elements of a table all have the same size, and we can use an efficient unboxed runtime representation (i.e. flat buffers and strided indices). Later, we'll see how to represent ragged tables, with irregularly sized elements using existential types, with corresponding run-time cost.

What can we do with a table? Surely we can index into it. In Dex, we use `.`

for indexing, so we might try to index in to a table like this:

Unfortunately, it's a type error. `i`

is an integer, but we need an index of
type `3`

(the index set `{0,1,2}`

). The error might be surprising because we
know `i=0`

in this case, but that's only true *dynamically* and the static type
system doesn't know about that. If we're willing to put up with runtime errors
we can cast the integer to the required index set.

But we're better off using indices of the right type to begin with. Where
would such an index come from? The main means of introducing an index is using
Dex's `for`

construct:

`for`

is to tables as `lam`

is to functions. It builds a new table whose
elements are the result of evaluating its body at each index `i`

in the given
index set. Like `lam`

, the type annotation (`::3`

) is optional and can be
inferred. Also like `lam`

, we can combine the let binding with the `for`

expression
in a way that looks like mathematical index notation. Type inference gives us
the same thing as if we'd annotated the binders manually.

Index set types interact nicely with polymorphism. The language of types, with type variables, is a very natural way to express shape constraints. For example, adding two vectors of the same size:

Transposing an array

Extracting the diagonal of a square array

## TODO:

- table/function contrast (cheap to create, expensive to apply and vice versa)
- structured index sets like pairs
- visible type application
- existentials, packing/unpacking
- input and output
- compiler internals -- normalized IR, imperative IR, LLVM
- currying tables
- mention prelude
- splittable PRNG
- automatic differentiation
- more syntax
- scan, fold