LEP-004: Type System


Created:Thursday, May 5, 2022
Author:David Delassus
Category:Language Design
Status:FINAL

Abstract

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

Rationale

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)

Specification

Literal values

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.

Container values

From those literal values, Letlang allows you to build:

ContainerExample of valueClass
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

Type alias

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;

Type constraint

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;

Generic type

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;

Rust representation of values

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.

Rust representation of classes

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,
    }
  }
}

Literals as types

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

Combining types

Letlang provides 3 operators to combine types together:

OperatorDescriptionExampleExample of values
|One Ofint | string42, "hello world"
&All Ofint & even42
!Not!even43, "hello world"

Rejected Ideas

Classes as objects

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

Object class

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.

Class expressions

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.

References

ReferenceTitleLink
1The ZFC Set Theoryhttps://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory
2Naive Set Theoryhttps://en.wikipedia.org/wiki/Naive_set_theory
3Russel’s Paradoxhttps://en.wikipedia.org/wiki/Russell%27s_paradox
4Elixir atomshttps://hexdocs.pm/elixir/1.13/Atom.html