See about for some background and motivation.
In this introduction we will start with a look at the type theory underlying Typedefs and in the next section we will show some examples in the S-expression syntax.
The core theory defines the following rules
0the empty type;
1the unit type;
+co-product of types (also known as sum-types);
×product of types (also known as tuples);
µfixpoint operator (also known as recursion);
- a, b variables;
With this you define algebraic data types (ADTs) such as:
- Types with a fixed finite number of terms, such as bits (2):
- Parametric types, such as the optional type:
α → Maybe α
- Recursive types, such as homogeneous lists:
α → List α
(Theoretically, these are least fixpoints of F-algebras. We recommend Bartosz Milewski’s blogpost on F-Algebras to learn about it.)
The theory has two ground terms, from which all concrete types are assembled:
0the empty type;
1the unit type.
The unit type 1 is the unique type that has only one term, usually denoted as •, a dot.
The zero type 0 is the unique type that has no terms (note: in practice you don’t really need the empty type, but there are theoretic reasons for including it).
Both these types are “units” with respect to the next two type formation rules
×, in the following sense:
0 + a = a + 0 = a
1 × a = a = a × 1
Note: at the moment, these equalities are not reduced away if you write them down.
OPEN: it is an partially open question still how to deal with normalization of types
Sum and product types
Using the familiar symbols
+ to express choice or co-product and
× for pairing we have the following two constructors:
- The coproduct (or sum) formation rule: for all types a and b,
a + bis a type;
- The product (or tuple) formation rule: for all types a & b,
a × bis a type.
The coproduct type expresses a choice between the terms of the two argument types.
The product type is the tuple or pair of the two argument types.
- We write
1 + 1to describe the finite type
2that has two terms, the left and the right unit terms of
- The type
2 * 2is the product of two
1 + 1terms, so a pair of booleans if you wish.
Type variables can be used to describe parametric type, such as the optional type.
Given a type
1 + x is the option or maybe type: its terms are the unit term or a term of type x.
Categorically, this defines the mapping 'x -> 1 + x`, which defines an endofunctor on the category of types.
There is also a 5th type formation rule, “mu”.
µfixpoint operator (also known as recursion)
When you apply µ to an algebraic functor, it expresses the fixpoint of that functor. Conceptually, “it closes the recursive type definition”.
For example, the list type,
l -> a -> (a * l a) + 1.
We currently use S-expressions as a convenient way to input type definitions.
You can use this from the browser at try.typedefs.com.
Alternatively, you can define types directly in Idris, see Examples.idr.
The Unit Type
In the S-expression language, it is predefined as the string
1 and you can assign a name to it as follows:
(name Unit 1)
Basic (closed) types
Let’s construct a very basic type, the booleans. In typedefs, we think of this as the co-product of two unit types, written as 1 + 1.
A co-product of types expresses a choice between terms of those types.
The equation 1 + 1 = 2 expresses nicely that the co-product of two unit types is isomorphic to a type called 2, that has two possible terms, namely the left or the right •.
Here is an example of such definition of the boolean type.
;; the Boolean type as the co-product of two unit-types (name Bool (+ 1 1))
This type is called closed because it does not have any free variables. (Note: as explained below, one way to think of these definitions is as endofunctors on typedefs. Closed typedefs are then functors from/to the unit type).
Type variables, basic parametric types
It is also possible to define “endofunctors on types”, such as the “optional” or “maybe” type.
Such a type is called parametric because it takes a typedef
α and constructs a new typedef
Hence, it is a 1-ary functor from typedefs to typedefs.
α → 1 + α
Here is the definiton:
;; the α → Maybe α type constructor (name Maybe (+ 1 (var 0)))
The number in
(var 0) is a De Bruijn index.
That’s it for now, more to be written.