Haskell type synonym declaration with constraint possible?

Question

Let's say I wanna make a type synonym for all lists with Int's.

I could do:

type NumberList = [Int]

But what if I want to call all lists that contains numbers NumberList? How would I put a constraint and say that all [a] as long as "Num a" should be called the same?

Edit:: After seeing the answers I rethought. It seemed like I was going against one of the basic ideas behind Haskell and the reward was relatively small (just a formal matter). I decided on this: If a type has the need for two instances identical to each other that only differ in Int or Float, then the difference between them is too small to warrant the workaround needed to accomplish the use of both Int and Float but calling them the same thing, which is why I must restrict the use to one of them. IF however there is an important reason to why I should have both, then I can probably reflect this important reason in the name of the instance and thereby avoid the problem by doing:

data Thing = Thing_A(String, String Float) | Thing_B(String,String,Int)

---and thereby stick to Haskell's typing system and still accept both of them as data type Thing. What I wanted to do at first was

data Thing = Thing(String, String, Float) | Thing(String, String, Int)

Answer 1

This corresponds to existential quantification. In pseudo-Haskell,

type NumberList = exists a . Num a => [a]

I say «pseudo» because GHC doesn't allow introducing existential quantifiers on the fly — you need to create a separate datatype for that.

Now, most of the type you'd use NumberList to the left of the arrow, where «exists» effectively changes its meaning to «forall».

That is, instead of writing

isIncreasing :: NumberList -> Bool

which is the same as

isIncreasing :: (exists a . Num a => [a]) -> Bool

you can write

isIncreasing :: forall a . Num a => [a] -> Bool

or simply

isIncreasing :: Num a => [a] -> Bool

Of course, having a type synonym seems like less code, but it has disadvantages as well. These disadvantages, by the way, are typical for object-oriented programming, which is based on the existential approach.

For example, you want to concatenate two lists. Ordinarily you would write

(++) :: forall a . [a] -> [a] -> [a]

(where again forall is unnecessary and added for clarity). Since a is the same across the entire signature, that ensures that you are concatenating lists of the same type.

How do we concatenate two numeric lists? A signature

(++) :: NumberList -> NumberList -> NumberList

wouldn't work, since one list may contain Ints and the other may contain Doubles. And the resulting NumberList has to contain values of a single type.

Or, say, you want to find the sum of the list elements.

Usually you write

sum :: Num a => [a] -> a

Notice that the result type is the same as the type of list elements. Alas, we cannot do the same for NumberList!

sum :: NumberList -> ???

What is the result type? We could apply existential quantification there as well.

sum :: NumberList -> (exists a . Num a => a)

But now the connection between the original list type and the sum type is lost — at least for Haskell's type system. If you then decide to write a function like

multiplySum :: Integer -> [Integer] -> Integer
multiplySum x ys = x * sum ys

then you'll get a type error, because sum ys may be of any type, not necessarily of type Integer.

It would work if you pushed everything to extreme and made every type existentially-quantified — but then you'd end up essentially with another object-oriented-like language with all their problems.

(That said, there are some good use cases for existential quantification, of course.)

Answer 2

Use data and parameters, not existentials to get contexts

I think if you wanted

data Thing = Good [(Char,Int)] | Bad String | Indifferent Leg

but also sometimes

data Thing = Good [(Char,Float)] | Bad String | Indifferent Arm

You could define

data Thing num bodypart = Good [(Char,num)] | Bad String | Indifferent bodypart

or if you want to make sure num is always numeric, you could do

data Num num => Thing num bodypart = Good [(Char,num)] | Bad String | Indifferent bodypart

and finally, you could restrict the types allowed in bodypart by defining your own class:

class Body a where
   -- some useful function(s) here

instance Body Leg where
   -- define useful function(s) on Legs
instance Body Arm
   -- define useful function(s) on Arms

data (Num num,Body bodypart) => Thing num bodypart = 
                                                             Good [(Char,num)] | Bad String | Indifferent bodypart

I'd like to discourage you from using existential types via the forall constructor or via GADTs because adding the num parameter to your data type is considerably more useful in practice, even though it takes more typing.

Constraints on type synonyms?

Note that when you use a constraint like

data (Num num) => Thing num = T [(Char,num)]

really only changes the type of the constructor T to

T :: (Num num) => [(Char,num)] -> Thing num

instead of T :: [(Char,num)] -> Thing num. This means every time you use T, there needs to be a context (Num num), but that's really what you wanted - to stop people putting data in your data type that isn't numeric.

A consequence of this fact is that you can't write

type Num num => [(Char,num)]

because there's no data constructor function T for the context (Num num) to be required on; if I have a [('4',False)], it automatically matches the type [(Char,num)] because it's a synonym. The compiler can't be going running around your code looking for instances before it decides what type something is. In the data case, it's got a constructor T that tells it the type, and it can guarantee there's a Num num instance because it checked your use of the function T. No T, no context.

Answer 3

GHC allows this using RankNTypes.

So you can do this:

type NumList = forall a . (Num a ,Fractional a) => [a]

And then if we have:

numList:: NumList
numList = [1,2,3]

fracList:: NumList
fracList = [1.3,1.7]

doing a concatenation yields :

fracList ++ numList :: Fractional a => [a]

which NumList is a synonym of. All in all i really don't see the point in this case.