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?

Ogden

Smart constructors, mostly. Forbid using T and S directly, and create newT and newS functions that verify the numbers passed. – Tala

Answer 1

Your best shot is not to export T and S explicitly, but allow a custom 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 won't be able to create T and S explicitly, but only with your smartConstruct function.

Tesch

Answer 2

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.

Crystallize

Nice. Do you happen to know where could I find more examples of this kind of trick? – Fini

And you can remove the handwave with Integer. – Hattie

@danidiaz: there are several instances of this pattern in the Agda standard library, e.g. check out agda.github.io/agda-stdlib/html/Data.Integer.html#915 – Crystallize

The link above is 404 now; the new correct one is agda.github.io/agda-stdlib/Agda.Builtin.Int.html#178 – Crystallize

Answer 3

If you are willing to restrict yourself to using Nats, and are ok with 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 for yourself, that it won't compile with wrong (odd/even) numbers.

Edit: More practical is probably cactus' approach though.

Etherege

This seems sort of dual to the request. Interesting, though. – Hattie

I also appreciate the Monty Python reference. – Hattie

why do you think it is dual? you need to go to some lengths to construct these natty weapons on runtime, but it's not hard (and a different kind of question). it does guarantee that only even bananas and odd pointy sticks gets constructed though. – Etherege