6

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?

Improve this question
1
  • 2
    Smart constructors, mostly. Forbid using T and S directly, and create newT and newS functions that verify the numbers passed. Commented Oct 20, 2014 at 13:51

3 Answers 3

Reset to default
10

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.

Improve this answer
Sign up to request clarification or add additional context in comments.

4 Comments

Nice. Do you happen to know where could I find more examples of this kind of trick?
And you can remove the handwave with Integer.
@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
The link above is 404 now; the new correct one is agda.github.io/agda-stdlib/Agda.Builtin.Int.html#178
9

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.

Improve this answer

Comments

6

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.

Improve this answer

3 Comments

This seems sort of dual to the request. Interesting, though.
I also appreciate the Monty Python reference.
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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.