Are type synonyms with typeclass constraints possible?

Question

Feel free to change the title, I'm just not experienced enough to know what's really going on.

So, I was writing a program loosely based on this, and wrote this (as it is in the original)

type Row a    = [a]
type Matrix a = [Row a]

Nothing special there. However, I found myself writing a couple of functions with a type like this:

Eq a => Row a -> ...

So I thought that perhaps I could write this constraint into the type synonym definition, because to my mind it shouldn't be that much more complicated, right? If the compiler can work with this in functions, it should work as a type synonym. There are no partial applications here or anything or some kind of trickery (to my eyes).

So I tried this:

type Row a = Eq a => [a]

This doesn't work, and the compiler suggested switching on RankNTypes. The option made it compile, but the functions still required that I leave the Eq a => in their type declarations. As an aside, if I tried also having a type synonym like type Matrix a = [Row a] like before, it results in an error.

So my question(s) are thus:

• Is it possible to have a type synonym with a typeclass constraint in its definition?

  • If not, why?

• Is the goal behind this question achievable in some other way?

Answer 1

Constraints on a type variable can not be part of any Haskell type signature.

This may seem a bit of a ridiculous statement: "what's (==) :: Eq a => a -> a -> a then?"

The answer is that a doesn't really exist, in much the same way there is not really an x in the definition f x = x * log x. You've sure enough used the x symbol in defining that function, but really it was just a local tool used in the lambda-abstraction. There is absolutely no way to access this symbol from the outside, indeed it's not required that the compiler even generates anything corresponding to x in the machine code – it might just get optimised away.

Indeed, any polymorphic signature can basically be read as a lambda expression accepting a type variable; various writing styles:

(==) :: forall a . Eq a => a -> a -> a
(==) :: ∀ a . Eq a => a -> a -> a
(==) :: Λa. {Eq a} -> a -> a -> a

This is called System F.

Note that there is not really a "constraint" in this signature, but an extra argument: the Eq-class dictionary.