Constraining Data Types

Question

Suppose you have a nice inductive definition and you want to define it as a data type in Haskell. However, your inductive definition is (as many inductive definitions are) of such a form that the generating rules require their 'premisses' to have a certain structure. For instance, suppose we have the following definition:

• if x is an even integer, then T x is a weapon,
• if x is an odd integer, then S x is a weapon.

If I want to define this (as a single) data type in Haskell, I would write something like

data Weapon =  T Int | S Int

Obviously, this will not work as you now can generate T 5 and S 4, for instance. Is there a natural way to pass on restrictions on the constructor arguments, so that I could write something similar to the above code which would give the correct definition?

Answer 1

This is a bit un-Haskelly, but is more idiomatic in e.g. Agda: change the interpretation of your representation so that it is forced to be correct by construction.

In this case, notice that if n :: Int, then even (2 * n) and odd (2 * n + 1). If we handwave away the case of too large Ints, we can say there's a bijection between the even Ints and the Ints; and another one between the odd Ints and the Ints.

So using this, you can choose this representation:

data Weapon = T Int | S Int

and change its interpretation such that the value T n actually represents T (2 * n) and the value S n represents S (2 * n + 1). So no matter what n :: Int you choose, T n will be valid since you will regard it as the "T-of-2*n" value.