# Functional Model: IR & Typing

###### tags: `study`

## PART 1: (Internal) Representation of Functional Languages

### De Brujin Indices vs. Symbols

De Brujin indices enable symbol-free representation of lambda calculus. The identity function $λx.x$ for example just becomes $λ 0$ using (zero-based) De Brujin indices. The zero index always represents the parameter of the innermost function. Larger indices represent parameters of respective outer functions. So for example $λx.λy.x$ will become $λ λ 1$, and $λx.λy.λz.y z (y z)$ will become $λ λ λ 2 0 (1 0)$.

Advantages of De Brujin indices in intermediate representations:

* Identical expressions always have the same representation (in contrast to symbol-based representations where e.g. $λx.x$ means the same as $λy.y$). This simplifies things like common subexpression elimination.
* No symbol scope management, symbol clashes etc.
* Efficient (short) visual representation.

Disadvantages:

* Probably less intuitive for most people. Transformations require different thinking (rather “how do I have to change the variable numbers” instead of “where could symbol clashes happen and how can we resolve them”). Also, it might be non-intuitive that variables with the same index may refer to different things, e.g. $λ 0 (λ 0)$ is equivalent to $λx.x (λy.y)$. That is, the index $0$ once refers to $x$ and once to $y$.

### Curried Function Representation

Typically, in modern functional languages (Haskell, OCaml, …) all functions take a single argument and return a single value. That is, all functions are represented in a _curried_ form by default. So even trivial functions like addition have a type of the form $a → a → a$ (where $a$ is a type variable), that is, a function taking an argument of type $a$ and returning a function of type $a → a$. This has several benefits:

* Functions can easily be partially applied.
* This matches lambda calculus!
* Thus: many papers and books available on type checking etc. from dozens of years of research.

From a code generation perspective, the curried representation might look like a disadvantage, as we might do not want to generate high-order functions when they are not necessary. Or we might even face environments where they are not supported (FPGAs, in-memory compute units?). However, in most common cases it should be fairly trivial to uncurry functions before code generation.

## PART 2: Typing Issues With Current Builtins

Several of our builtin functions have some minor or major issues when we look at them from a functional perspective. These are just notes on some findings that might or might not be relevant for topics like type reconstruction/checking and code generation in the future.

### Variadic `make_tuple`

`make_tuple` is the only builtin that requires variadic arguments. It has a rather strange signature $a_1 → a_2 → … → a_n → (a_1, a_2, …, a_n)$. Obviously, this signature does not make any sense in lambda calculus (e.g. if you call $\mathrm{make\_tuple} 0 1$, there is no way for $\mathrm{make\_tuple}$ to know if it should return a 2-tuple or rather a function that takes another argument and returns a 3-tuple or …). Maybe there should be support for tuples in the grammar for the language? This would also allow tuple literals. Alternatively, specific versions for different number of arguments would work, e.g. $\mathrm{make\_tuple2}::a_1 → a_2 → (a_1, a_2)$.

### The `tuple_get` Overloads

The index argument of `tuple_get` has to be a compile-time literal integer (otherwise we can not derive a unique return type). So the correct solution in a functional world is to have a different functions for different indices (like e.g. Haskell’s `fst` and `snd`). So the definitions would look like
$$
\begin{align}
\mathrm{tuple\_get0}&:: (a_1, a_2, …, a_n) → a_1 \\
\mathrm{tuple\_get1}&:: (a_1, a_2, …, a_n) → a_2 \\
\vdots
\end{align}
$$
As this still requires overloads that complicate the life of the type checker, a simpler approach would be to have functions also specific to the tuple size (also like in Haskell):
$$
\begin{align}
\mathrm{tuple2\_get0}&:: (a_1, a_2) → a_1 \\
\mathrm{tuple2\_get1}&:: (a_1, a_2) → a_2 \\
\mathrm{tuple3\_get0}&:: (a_1, a_2, a_3) → a_1 \\
\mathrm{tuple3\_get1}&:: (a_1, a_2, a_3) → a_2 \\
\mathrm{tuple3\_get2}&:: (a_1, a_2, a_3) → a_3 \\
\vdots
\end{align}
$$

### The `shift`

As offsets can be arbitrary in our model, the type checker can not check their type, right? The signature of `shift` will probably just be $a → \mathrm{Iterator} b → \mathrm{Iterator} b$. This should not be a big issue though, as errors will easily be catched at a later stage in the compilation process.

### The `lift` Overloads

`lift` has some fancy overloads. Specially, it has to dispatch on the return type of the given function. The “standard” signature already looks like $(\mathrm{Iterator} a_1 → … → \mathrm{Iterator} a_n → b) → (\mathrm{Iterator} a_1 → … → \mathrm{Iterator} a_n → \mathrm{Iterator} b)$. But we also plan to have an overload for stencils returning tuples:
$(\mathrm{Iterator} a_1 → … → \mathrm{Iterator} a_n → (b_1, …, b_n)) → (\mathrm{Iterator} a_1 → … → \mathrm{Iterator} a_n → (\mathrm{Iterator} b_1, …, \mathrm{Iterator} b_n))$
Or do we rather introduce an additional builtin that enables the conversion from $\mathrm{Iterator} (a_1, …, a_b)$ to $(\mathrm{Iterator} a_1, …, \mathrm{Iterator} a_n)$?
In any case, `lift` might be a challenge for an as-simple-as-possible type checker.

Relatively simple expressions can not be type-checked anymore using this fancy lift, e.g. $λ f.λ x. \mathrm{lift} f x$ as there is an infinite number of matching types. Note that this is probably not something a user would write, but still a valid expression in our language.

Possible workaround for the first issue: use different lift functions instead of overloads. The specific function to use could either be inferred by the front end or before type checking. So we would have the following definitions:

$$
\begin{align}
\mathrm{lift1}&:: (\mathrm{Iterator} a_1 → b) → (\mathrm{Iterator} a_1 → \mathrm{Iterator} b) \\
\mathrm{lift2}&:: (\mathrm{Iterator} a_1 → \mathrm{Iterator} a_2 → b) → (\mathrm{Iterator} a_1 → \mathrm{Iterator} a_2 → \mathrm{Iterator} b) \\
\vdots
\end{align}
$$

Now, the type checker could easily derive the correct type of e.g. $λ f.λ x. \mathrm{lift1} f x$ as $(\mathrm{Iterator} a_1 → b) → \mathrm{Iterator} a_1 → \mathrm{Iterator} b$.

With this strategy, the additionally required conversions from iterators of tuples to tuples of iterators requires the additional functions

$$
\begin{align}
\mathrm{ittup\_to\_tupit2}&::\mathrm{Iterator} (a_1, a_2) → (\mathrm{Iterator} a_1, \mathrm{Iterator} a_2) \\
\mathrm{tupit\_to\_ittup2}&::(\mathrm{Iterator} a_1, \mathrm{Iterator} a_2) → \mathrm{Iterator} (a_1, a_2) \\
\vdots
\end{align}
$$

Note that these functions can be implemented using already available builtins as follows:

$$
\begin{align}
\mathrm{ittup\_to\_tupit2} &= λx.(\mathrm{lift1} (λy.\mathrm{tuple2\_get0} (\mathrm{deref} y)) x, \mathrm{lift1} (λy.\mathrm{tuple2\_get1} (\mathrm{deref} y)) x) \\
\mathrm{tupit\_to\_ittup2} &= λx.\mathrm{lift2} (λy.λz.(\mathrm{deref} y, \mathrm{deref} z)) (\mathrm{tuple2\_get0} x) (\mathrm{tuple2\_get1} x) \\
\vdots
\end{align}
$$

(where $(*, *)$ is used instead of $\mathrm{make\_tuple}$).

### The `scan` Overloads

Exactly same problem as `lift`. Can also be worked around by using `scan1`, `scan2`, etc. instead of overloads. E.g.:
$$
\begin{align}
\mathrm{scan1}&:: (s → \mathrm{Iterator} a_1 → b) → bool → s → (\mathrm{Iterator} (\mathrm{Column} a_1) → \mathrm{Column} b)\\
\vdots
\end{align}
$$

### Getting a Value From an Optional

Not really a problem with our model, but an uncertainty: the current Python iterator implementation does not seem to properly handle optional types. There does not seem to be a difference between optionals and non-optionals?