Type System

Type System

Created: | Thursday, May 5, 2022 |
---|---|

Author: | David Delassus |

Category: | Language Design |

Status: | FINAL |

This LEP specifies the Letlang Type System, its features, its syntax and its implementation.

In almost all programming languages, an object is associated to a single type:

`42`

is an integer`"hello world"`

is a string`2.3`

is a float

Some programming languages implement polymorphism with inheritence, giving the developer the ability to create new types from the builtin types of said language. A function expecting a specific type as parameter will accept any derived type, but nothing else.

Other programming languages implement polymorphism with interfaces, giving the developer the ability to indicate what operations must be supported by the supplied argument.

This creates a strong coupling between the structure of data and the implementation of the operations manipulating such data.

However, in mathematics, objects have no type. Instead, the mathematician will define a collection with rules indicating which objects are part of said collection.

Therefore, `42`

is an integer, a real, a complex, a rank-1 tensor, etc…

Then, the mathematician will define the operations available for every object of such collections.

In most programming languages, you will find a keyword, or function named
`typeof`

, allowing the developer to ask for the type of an object. In
mathematics, we ask wether an object is part of a collection or not, since
objects do not have an inherent “type”.

The field of fundamental mathematics aims to create a framework, at the root of mathematics, from which we can build the rest of all mathematics.

The ZFC Set Theory^{[1]} is one of such frameworks. In this
theory, all objects could be described as **sets**. And only the *belongs to*
relationship can exists between two objects of this theory.

From this, we can define a few axioms to build equality, numbers, etc…

This theory is an improvment over naive set theory^{[2]} which
leads to the Russel’s Paradox^{[3]}:

Does the set of all set that do not contain itself, contains itself?

If such set `S`

does not contain itself, by definition, it should. But if it
does contain itself, by definition, it shouldn’t.

The ZFC Set Theory uses a restricted comprehension axiom preventing the mathematician to build such sets.

However, there are other workarounds to this paradox:

- classes
- type hierarchy

A class is a collection of objects, but it is not an objet, therefore no set or class can contain a class.

The collection of all set that do not contain itself is a class.

Type hierarchy introduces the following rule:

- objects of Type 1 can only contain objects of Type 0
- objects of Type 2 can only contain objects of Type 1
- …
- objects of Type N can only contain objects of Type N-1

If a set is an object of Type 0, then a set of sets is an object of Type 1.

The set of all sets that do not contain itself is higher in the type hierarchy, and therefore, cannot contain itself.

The Letlang type system is inspired by those concepts and differes from other programming languages:

- a Letlang object (or value) does not have a type
- the developer can define collections of objects (or values) and the rules to indicate wether or not they are part of the collection
- Letlang have 2 kinds of collections: sets and classes
- Letlang’s sets are hierarchical (they cannot contains themselves)

Letlang provides some literal values that are part of at least one builtin class:

- booleans
`true`

and`false`

are part of the class`bool`

- numbers are part of the class
`number`

and`int`

if their fractional part is 0 - UTF-8 strings are part of the class
`string`

- atoms (just like Elixir
^{[4]}) are part of the class`atom`

NB:An atom is a developer-defined symbol (starting with`@`

), once compiled, it is translated to a unique identifier.

From those literal values, Letlang allows you to build:

Container | Example of value | Class |
---|---|---|

tuples | `(@ok, 42)` | `tuple<atom, number>` |

structures | `{x: 0, y: 0}` | `{x: number, y: number}` |

lists | `[1, 2, 3]` | `list<number>` |

finite sets | `{1, 2, 3}` | `set<number>` |

infinite sets | `{x: number | x < 0}` | `set<number>` |

NB:The classes`tuple`

,`struct`

,`list`

, and`set`

do not exist. They are generic types and require type parameters.

Therefore, type hierarchy is implemented thanks to generics. This implies that the following would raise a typing error:

```
Sa := { s: set | s not in s }; # TypeError: class set does not exist
Sb := { s: set<number> | s not in s }; # TypeError: set<number> can only contain numbers
```

The developer is able to define its own collections of objects (classes):

```
class point(p: {x: number, y: number});
```

According to the above definition, any structure with at list `x`

and `y`

as
numbers are part of the `point`

class:

```
{x: 0, y: 0} is point = true;
{x: 0} is point = false;
{x: 0, y: 0, z: 0} is point = true;
```

Additionally, a class can define an expression that must returns `true`

for
every object it contains:

```
class even(n: int) {
n % 2 = 0;
}
```

According to the above definition:

```
42 is even = true;
43 is even = false;
```

To reduce code duplication, a class can require type parameters:

```
class vector<T>(v: {x: T, y: T});
```

According to the above definition:

```
{x: 0, y: 0} is vector<int> = true;
{x: 0, y: 0} is vector<string> = false;
```

The `letlang_runtime`

Rust crate provides a structure `Value`

used to encapsulate
Letlang objects:

```
use letlang_runtime::*;
let i = Value::Primitive(PrimitiveValue::Number(42));
```

NB:Implementation details may vary.

The `letlang_runtime`

Rust crate provides a trait `Type`

used to represent a
Letlang class.

A Letlang class is effectively a function which takes a `Value`

as parameter and
returns a `bool`

, indicating wether or not the class contains the supplied value.

**Example:**

```
use letlang_runtime::*;
struct BooleanType;
impl Type for BooleanType {
fn has(&self, llval: &Value) -> bool {
match llval {
Value::Primitive(PrimitiveValue::Boolean(_)) => true,
_ => false,
}
}
}
```

A Letlang value can be used as a type:

```
class highlander(v: "connor macleod");
```

According to the above definition:

```
"connor macleod" is highlander = true;
"anyone else" is highlander = false;
# there can be only one
```

Letlang provides 3 operators to combine types together:

Operator | Description | Example | Example of values |
---|---|---|---|

`|` | One Of | `int | string` | `42` , `"hello world"` |

`&` | All Of | `int & even` | `42` |

`!` | Not | `!even` | `43` , `"hello world"` |

A class is not an object. If it were, it is unclear how we would avoid the
Russel’s Paradox^{[3]}.

For some time, a class `object`

which would contain every Letlang object was
considered. But it was a way to work around the type hierarchy of sets.
Therefore, it was abandonned.

Since a class is not an object, such expression cannot return any value. It was decided to make it a statement at the toplevel of a module.

Reference | Title | Link |
---|---|---|

1 | The ZFC Set Theory | https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory |

2 | Naive Set Theory | https://en.wikipedia.org/wiki/Naive_set_theory |

3 | Russel’s Paradox | https://en.wikipedia.org/wiki/Russell%27s_paradox |

4 | Elixir atoms | https://hexdocs.pm/elixir/1.13/Atom.html |