Data type restriction

Question

Suppose you have a good inductive definition and you want to define it as a data type in Haskell. However, your inductive definition (like many inductive definitions) is such that the generation rules require that their “premises” have a certain structure. For example, 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 one) data type in Haskell, I would write something like

 data Weapon = T Int | S Int 

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

Answer 1

It’s best not to export T and S explicitly, but to allow your own constructor:

 module YourModule (Weapon, smartConstruct) where data Weapon = T Int | S Int smartConstruct :: Int -> Weapon smartConstruct x | even x = T x | otherwise = S x 

Now, when importing YourModule users will not be able to explicitly create T and S , but only with your smartConstruct function.

Answer 2

It's a little non-Haskelli, but more idiomatic, for example. Agda: Change the interpretation of your view so that it is correctly constructed.

In this case, note that if n :: Int , then even (2 * n) and odd (2 * n + 1) . If we discard the case of too large Int s, we can say that there is a bijection between the even Int and Int s; and the other between the odd Int and Int s.

Thus, using this, you can select this view:

 data Weapon = T Int | S Int 

and change its interpretation so that the value of T n actually represents T (2 * n) , and the value of S n represents S (2 * n + 1) . Therefore, no matter which n :: Int you choose, T n will be valid, since you will consider it the value " T -of-2 * n".

Answer 3

If you want to limit yourself to using Nats and agree to using reasonably advanced type magic, you can use GHC.TypeLits .

 {-# LANGUAGE DataKinds, GADTs, TypeOperators, KindSignatures #-} import GHC.TypeLits data Weapon (n :: Nat) where Banana :: n ~ (2 * m) => Weapon n PointyStick :: n ~ (2 * m + 1) => Weapon n banana :: Weapon 2 banana = Banana pointyStick :: Weapon 3 pointyStick = PointyStick 

try it yourself that it will not compile with the wrong (odd / even) numbers.

Edit: A more practical, probably cactus approach.