Algebraic Typing in Lime

Before I started working on Lime, and was only familiar with statically typed languages in the context of Java and C, I thought type systems were really limiting. However, the incredible capability of type systems of languages like Haskell and Rust (Rust's is even turing complete!) have proven this very wrong.

A lot of these innovations come from a field of mathematics called category theory. The fundamental object of category theory is a directed graph called a category:

A drawing showing the objects X, Y, and Z connected by f, g, and f of g. X is mapped to Y by f, Y is mapped to Z by g, and Z is connected to X by g of f.

The nodes of these graphs are called objects, and the edges are called morphisms (hence the term polymorphism).

One of the most important parts of modern type systems is something called algebraic typing. Algebraic typing allows for functions that can take multiple forms, based on an algebraic expression. For example, the car command which returns the first element of a list must have a form for int$, str$, int$$, and so on, cannot be defined through polymorphism: there would be infinitely many forms. Instead, it can be defined algebraically:

car (list:A$) -> A

where A is a placeholder, which may be substituted for any type. Therefore, car will be defined for lists of all types.

More complicated expressions can be done with container types like dictionaries:

dget (dict:[A->B] key:A) -> B

In this example, the theoretical dget command (to get a value from a key in a dictionary) accepts dictionaries mapping any type to any other type, accepts a key of the key type of the dictionary, and returns a value with the type of the value type of the dictionary.

Additionally, since Lime is a first-order language, all functions have explicit types signatures, declaring their input and output types and arity. Functions that operate on other functions can have super explicit type signatures. For example, the map command's signature is:

map (lambda[A->B] A$) -> B$

which will ensure that the list being mapped is of the input type of the function, and will make the output type of map a list of the output type of the function.

The new type system will be merged in 1.2.0.