Typedefs

Introduction

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.

Type system

The core theory defines the following rules Typedefs.idrs/TDef:

  • 0 the empty type;
  • 1 the 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;
  • a b application.

With this you define algebraic data types (ADTs) such as:

  • Types with a fixed finite number of terms, such as bits (2): Bool
  • 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 units

The theory has two ground terms, from which all concrete types are assembled:

  • 0 the empty type;
  • 1 the 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 + and ×, 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 + b is a type;
  • The product (or tuple) formation rule: for all types a & b, a × b is 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.

Some examples:

  • We write 1 + 1 to describe the finite type 2 that has two terms, the left and the right unit terms of 1;
  • The type 2 * 2 is the product of two 1 + 1 terms, so a pair of booleans if you wish.

Type variables

Type variables can be used to describe parametric type, such as the optional type.

Given a type x, 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.

Recursive 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.

Input Language

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 Maybe α.

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.

TODO

That’s it for now, more to be written.

If you want to learn more, you can browse the source code or Try Typedefs!.