Oters - Type System

Oters implements and extends the type system described by Patrick Bahr in his Modal FRP for all paper. The type system is therefore a modal type system and most likely different to any other you have previously come across. But before getting into the modal type constructs, I introduce the other, more traditional, types that Oters implements.

Primitive Types

• unit: a unit type written ().
• int: a 64-bit signed integer.
• float: a 64-bit floating point.
• string: a string type. Specifically implemented using Rust’s String type.
• bool: a boolean type.

Compound Types

• tuple: a tuple type composed of potentially different types. For example the expression ("Hello", 21, true) would be of type (string, int, bool).
• list: a linked list type similar to OCaml’s basic lists. A list [0, 1, 2, 3] would have type [int].
• function: a function type comprised of the argument’s type and a return type. The function fn x -> x + 1 would have type int -> int
• struct: compound data types akin to Rust’s structs. They are declared by the user and referred to by their name.
• enum: also user defined and similar to Rust’s enums. Like structs they are referred to by their name.

Generic Types

Oters supports user defined generic types. For example the Option<T> type is a generic enum. Similarly the Stream<A> which is at the core of Oters is also generic. They are defined and composed using angle brackets like in Rust. A good example of this is the Event type which is defined as follows:

type Event<A> = Stream<Option<A>>

Modal Types

A mentioned in the previous section, Functional Reactive Programming works on temporal data, specifically through the stream data type. The modal time system aims to capture this distinction we wish to make of values across time. Earlier we described streams as being composed of a head containing a value at the current time step and a tail that contains a reference to the future values of a stream. Here, we are making a distinction between a value available now and the rest of the stream available later. This gives the following modal type definition for streams:

Where the \(\bigcirc\) represents a value available later, specifically in the next time step. The reason we want to make this temporal distinction so explicit is to preserve causality. In other words, we do not want to be able to access values that aren’t yet available in the current time step. Since computing in advance all the future (often infinite) values of a stream is unfeasible, we evaluate the tail one time step at a time. Therefore, by using the \(\bigcirc\) modality, the type system can enforce that values available later can only be accessed later.

Aside from the \(\bigcirc\) modality, Oters includes the stable modality marked with the symbol \(\square\).Primitive types are inherently stable since they cannot change over time, as well as as compound types such as tuples, lists and structs whose underlying types are all also stable.

This leaves function types and \(\bigcirc\) types as being temporally variant or unstable. Function types in particular are unstable because they can capture unstable types in their closure. \(\bigcirc\) types are naturally unstable since they reference the next time step.

However, we can prefix an unstable type with a \(\square\) to turn it into a time-invariant type. This allows us to transport temporal types into any time step by suspending their computation until they are unwrapped. Right now this will seem quite abstract, but it is explained in more detail in following sections.

Lastly, we mark these modalities in Oters using the @ symbol for \(\bigcirc\) and the # symbol for \(\square\):

type Stream<A> = (A, @Stream<A>)
type Map<A,B> = #(A -> B) -> Stream<A> -> Stream<B>

Guarded Recursion

The last concept that Oters borrows from Bahr’s type system is that of guarded recursive types. When working with streams we want to ensure productivity. What this means is that we want a guarantee that any computations that are due at the next time step (i.e. those behind a \(\bigcirc\)) will become available on time. This is implemented through guarded recursion, which ensures that all recursive calls to time variant types is done behind a \(\bigcirc\). Streams are an example of a guarded recursive type. This means that the definition above is equivalent to the following with an explicit guarded fixed point and its corresponding unfolding:

However, this concept of guarded recursion is made transparent to the user, and Oters automatically transforms recursive types and variables into their corresponding fixed point. This section on guarded recursion is included here for completeness’ sake, but you need not worry as a programmer.

Finally, I would like to point you to Patrick Bahr’s paper once again. Oters type system is just an extension of his Rattus and you can find much more detailed explanations of these concepts in his paper.