The computation of appending lists at the type and value level

Recently, I spent some time experimenting with Haskell’s type families – a concept that allows one to perform computation at the type level in Haskell.

In one example, I wrote an append implementation at the value and the type level, and also other stuff such as Merge Sort implementation at the type level.

In this post, I will show different implementations of appending two lists together, written both in Haskell and in Idris, as well as some observations around the differences.

Haskell, value level

The implementation for this is straightforward. We need to build a recursive function that accepts two lists, such that:

When one of the list is empty, return the other
Chop the left list, appending values one by one recursively with the other list

append []     ys = ys
append (x:xs) ys = x : append xs ys

Example evaluation:

> append [1] [2]
[1,2]

Written as a mathematical recursive function:

$append(xs, ys) = \left\{ \begin{array}{ll} ys & \mbox{if } xs = [] \\ cons(head(xs), append(tail(xs), ys)) & \mbox otherwise \end{array} \right.$

With the corresponding compact definition in Haskell:

append xs ys = if xs == [] then ys
               else (:) (head xs) (append (tail xs) ys)

Haskell, type family level

Per the official docs:

Type families are useful for generic programming, for creating highly parameterised library interfaces, and for creating interfaces with enhanced static information, much like dependent types.

The implementation for this almost maps 1:1 with the previous one (append).

type family Append xs ys where
  Append '[]    ys = ys
  Append (x:xs) ys = x : Append xs ys

Example evaluation:

> :set -XDataKinds
> :kind! Append '[1] '[2]
Append '[1] '[2] :: [GHC.Types.Nat]
= '[1, 2]

Idris, value level

The implementation at the value level would look pretty similar to Haskell’s, so we skip it.

Idris, type level

Here is one way to implement it:

data Append : List a -> List a -> List a -> Type where
  AppendNil : Append [] ys ys
  AppendRec : Append xs ys zs -> Append (x :: xs) ys (x :: zs)

To show [1] ++ [2] is [1, 2], we use the following proof:

appendEg1 : Append [1] [2] [1, 2]
appendEg1 = AppendRec AppendNil

We can also prove that Append produces the same result as append

total proof_1 : Append xs ys zs -> zs = append xs ys
proof_1 AppendNil = Refl
proof_1 (AppendRec prf) = let IH = proof_1 prf in rewrite IH in Refl

We can represent the same rules in natural deduction style:

$\cfrac{}{[] \mathbin{{+}\mspace{-8mu}{+}} ys = ys} (\texttt{AppendNil}) \quad \cfrac{xs \mathbin{{+}\mspace{-8mu}{+}} ys = zs}{(x::xs) \mathbin{{+}\mspace{-8mu}{+}} ys = (x :: zs)} (\texttt{AppendRec})$

Discussion

The implementation of Append in Idris requires some discussion, as it might not be immediately obvious how it directly maps to the previous implementations of append.

In fact, it’s easy to see how this corresponds to Haskell’s type family instance. Compare:

-- Idris type level
AppendNil : Append [] ys ys
AppendRec : Append xs ys zs -> Append (x :: xs) ys (x :: zs)

-- Haskell type family
Append '[]    ys = ys
Append (x:xs) ys = x : Append xs ys

While working with Haskell’s type families at the type level we were able to use lists as the return value, in Idris we are only able to return Type as return value, so we need to introduce another parameter zs that will represent the returning list.

Starting with this reasoning:

For the base case, Append '[] ys = ys becomes Append '[] ys ys, since the value for Append '[] ys is ys.
For the recursive step, note that Append (x:xs) ys appends x to some list Append xs ys. Let’s call this list zs = Append xs ys. Now we have Append (x:xs) ys = x : zs. But hey, that’s actually Append (x :: xs) ys (x :: zs) (which is AppendRec from before). In addition, since we used zs, we also need to add it to the hypothesis – note that zs = Append xs ys really means Append xs ys zs. Thus it becomes Append xs ys zs -> Append (x :: xs) ys (x :: zs).

The formulas in natural deduction:

$\cfrac{}{\texttt{Append} \ [] \ ys \ ys} (\texttt{AppendNil}) \quad \cfrac{\texttt{Append} \ xs \ ys \ zs}{\texttt{Append} \ (x :: xs) \ ys \ (x :: zs)} (\texttt{AppendRec})$

Bonus: This formula can be directly applied to the Prolog programming language, where unification lies at the heart of computation:

append([ ], Ys, Ys).
append([X|Xs], Ys, [X|Zs]) :- append(Xs, Ys, Zs).

Closing thoughts

There is a chapter in Logical Foundations that does something similar – calculating the same things at the value level and at the type level. (I highly recommend Logical Foundations.)

In addition, you can compare Hoare implementation in Coq (type level), vs my Hoare implementation in Haskell (value level).

Haskell’s type system is Turing complete, and thus unsound as a proof system (since some “proofs” may not terminate). Idris, on the other hand, allows functions to be defined as total and therefore must terminate.

One compact way to define computation is in the form of a computable function: A function $f : \mathbb{N}^{k} \to \mathbb{N}$ is said to be computable if there’s a procedure such that for any $k$ -tuple of natural numbers, it produces $f(x)$ , e.g. $(1, 2, 3) \to 1$ . The computability thesis states that all computation can be captured by computable functions.

In any case, whether at the value level, as a mathematical recursive function, at the type-level, or in the natural deduction style, computation comes from many forms (different notations), whereas the actual process as to what is to be computed is the same.