# 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!.