Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How do I define a data type that only accepts numbers?

I am attempting to create a data type, Point, that takes three numbers for its constructor. Initially, I had written

data Point = Point Double Double Double

but I ran into some issues when certain pieces of code expected Ints.

So I changed it to

data Point a = Point a a a

but now I would like to enforce that a is an instance (?) of Num - I only want to accept numbers in the constructor.

Is this possible? If not, what is the accepted practice? How many times did I use the wrong word to describe something?

like image 563
sdasdadas Avatar asked Oct 29 '13 04:10

sdasdadas


2 Answers

Yes! At least if you allow yourself some language extensions GHC provide. You basically have four options where one is bad, one is better, one is not as obvious as the other two and one is the Right Way™.

1. The Bad

You can write

{-# LANGUAGE DatatypeContexts #-}
data Num a => Point a = Point a a a

This will make it so that the constructor Point can only be called with Num a values. However, it does not limit the contents of a Point value to Num a values. This means that if you further down the road want to add two points, you would still have to do

addPoints :: Num a => Point a -> Point a -> Point a
addPoints (Point x1 y1 z1) {- ... -}

Do you see the extra Num a declaration? That shouldn't be necessary since we know a Point can only contain Num a anyway, but that's the way DatatypeContexts work! You have to put constraints on every function needing it anyway.

This is why, if you enable DatatypeContexts, GHC will scream at you a little for using a "misfeature."

2. The Better

The solution involves turning on GADTs. Generalised algebraic datatypes allow you to do what you want. Your declaration would then look like

{-# LANGUAGE GADTs #-}
data Point a where
  Point :: Num a => a -> a -> a -> Point a

When using GADTs, you declare constructors by stating their type signature instead, almost like when creating typeclasses.

Constraints on GADT constructors have the benefit that they carry over to the value that is created – in this case that means both you and the compiler knows that the only existing Point as have members who are Num as. You can therefore write your addPoint function as just

addPoints :: Point a -> Point a -> Point a
addPoints (Point x1 y1 z1) {- ... -}

without the irritating extra constraint.

Side note: Deriving Classes for GADTs

Deriving classes with GADTs (or any non-Haskell-98 type) requires an extra language extension and it is not as smooth sailing as with normal ADTs. The principle is

{-# LANGUAGE StandaloneDeriving #-}
deriving instance Show (Point a)

This will just blindly generate code for the Show class, and it is up to you to make sure that code typechecks.

3. The Obscure

As shachaf points out in the comments to this post, you can get the relevant parts of GADT behaviour while retaining traditional data syntax by enabling ExistentialQuantification in GHC. This makes the data declaration as simple as

{-# LANGUAGE ExistentialQuantification #-}
data Point a = Num a => Point a a a

4. The Correct

However, none of the solutions above is what the consensus in the community is. If you ask knowledgeable people (thanks to edwardk and startling in the #haskell channel for sharing their knowledge), they will tell you not to constrain your types at all. They will tell you that you should define your type as

data Point a = Point a a a

and then constrain any functions operating on Points, like for example the one to add two points together:

addPoints :: Num a => Point a -> Point a -> Point a
addPoints (Point x1 y1 z1) {- ... -}

The reason to not constrain your types is that when doing so, you seriously limit your options for using the types later, in ways you probably don't expect. For example, creating a Functor instance for your point might be useful, like so:

instance Functor Point where
  fmap f (Point x y z) = Point (f x) (f y) (f z)

and then you can do something like approximating a Point Double with a Point Int by simply evaluating

round <$> Point 3.5 9.7 1.3

which will produce

Point 4 10 1

This would not be possible if you constrained your Point a to Num as only, because you can't define a Functor instance for such a constrained type. You woud have to create your own pointFmap function, which would go against all reusability and modularity that Haskell stands for.

Perhaps even more convincing, if you ask the user for coordinates but the user only enters two of them, you can model that as a

Point (Just 4) (Just 7) Nothing

and easily convert it to a point on the XY plane in 3D space by mapping

fromMaybe 0 <$> Point (Just 4) (Just 7) Nothing

which will return

Point 4 7 0

Note here that this latter example wouldn't work for two reasons if you had a Num a constraint on your point:

  1. You would not be able to define a Functor instance for your Point, and
  2. You would not at all be able to store Maybe a coordinates in your point.

And this is just one useful example of the many you would forego if you applied the Num a constraint on the point.

On the flip side of this, what do you gain by constraining your types? I can think of three reasons:

  1. "I don't want to accidentally create a Point String and try to manipulate it as a number." You won't be able to. The type system will stop you anyway.

  2. "But it's for documentation purposes! I want to show that a Point is a collection of numeric values." ...except when it is not, such as Point [-3, 3] [5] [2, 6] which expresses alternative coordinates on the axes, which may or may not all be valid.

  3. "I don't want to keep adding Num constraints to all my functions!" Fair enough. You can copy and paste them from ghci in this case. A little keyboard work is worth all the benefits, in my opinion.

like image 172
kqr Avatar answered Oct 05 '22 06:10

kqr


You can use GADT to specify the constraint:

{-# Language GADTs #-}

data Point a where
  Point :: (Num a) => a -> a ->  a -> Point a 
like image 41
Ankur Avatar answered Oct 05 '22 07:10

Ankur