How do you define in particular a linked list in abstract type theory? Or would you even do that?

Question

I understand somewhat how abstract List is defined. But still not 100%. Type theory literature is not that great yet.

I want to know how to build basic data types. That is the closest stepping stone for me to learning more type theory.

Does type theory go on to define different implementations of list such as a basic pointer-based linked list?

Answer 1

Let start from the basic: a list, of type $A$, is a data type $L(A)$ whose values can either be

• the empty list, let denote it by $( )$,

• a pair $(x,xs)$ where $x \colon A$ and $xs$ is a list of type $A$, that is $xs \colon L(A)$.

When implementing this data type in a computer one can think of $xs$ as above as a reference to another list (the tail of your list), so I guess this actually provides the type theoretic version of your pointer-based list.

From a type theoretic perspective the type list of $A$ can be represented as the least solution to the type equation

$$L=1+A\times L$$

i.e. as the least fixed point to the type operator $$X \mapsto 1+A\times X\ .$$

Usually all the classical recursive data types are implementented exactly in this way, i.e. as fixed point for some type-operators.

Other examples of recursive types defined in this way are

• natural numbers, which is the least fixed point for the operator $$X \mapsto 1+X$$
• binary trees with nodes of a given type $A$, i.e. fixed the point for the operator $$X \mapsto A+(A \times X \times X)$$
• arbitrary trees, that is the fixed point for $$X \mapsto (A \times L(X))$$ where $L(X)$ denotes the type of lists of elements of type $X$.

There is also a very simple rule to translate this kind of definitions in haskell code and vice versa but in order to show that a little knowledge of haskell's syntax would be required.

I hope this helps.