CODEWITHSUNDEEP
haskelltypesrepresentation
Holdwin
Holdwin

Reputation: 75

Constraining Data Types

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 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?

Upvotes: 6

Views: 172

Answers (3)

ibotty
ibotty

Reputation: 729

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.

Upvotes: 5

Cactus
Cactus

Reputation: 27626

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.

Upvotes: 10

Shoe
Shoe

Reputation: 76240

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.

Upvotes: 9

Related Questions