Haskell using typeclasses inside type signatures

Question

Assuming a simple typeclass constrained signature:

f :: (Eq a, Num b) => a -> b
f str = 4

I was wondering why these didn't work

f :: (Eq a) -> (Num b)
f str = 4

f :: Eq -> Num
f str = 4

I know that type classes have the kind * -> Constraint, whereas the type signatures only accept kinds of *.

But my question is why is there this restriction? Why can't typeclasses be used like types? What would be the advantages and disadvantages of allowing the ability to use typeclasses like types?

Answer 1

There is (if we neglect unboxed types) only one kind whose types actually have any values: *. All other kinds don't contain types as such, but just "type-level entities". The compiler can use those to determine what to do with the actual types and their values around, but it's never possible to have at runtime a value of a "type" with some kind like * -> Constraint.

That * is the kind for value-types is just a rule of the game. It's a good thing to have, for much the same reason it's a good idea to have a strong static type system which prevents nonsensical conversions at runtime. ^Wat?? Or, let's take it literally, for the same reason you can't just hop your king over your pawns, no matter how appealing that feature might look in a particular situation you've run into.

If some extension did allow making values from non-*-kinded types, in particular * -> Constraint, we'd need a whole bunch of non-obvious definitions to make it clear how these "class-values" are actually supposed to be used. Likely, it would amount to a record type containing the class' methods as a dictionary. But, how exactly... the specification would be pretty much of a nightmare. And complicating the language itself this way is in no way worth the expenditure, since 1. the standard way of using type classes is just fine for at least 95% of all applications, and 2. when you do need reified type classes, you can quite easily do so with GADTs, ConstraintKinds, or even plain old manually-defined dictionary records. None of that requires distorting the fundamental ideas of how the language treats values, as non-*-types would.

---

Anyway... let's explore for a moment how this might work. One thing is for sure: it would not allow you to write stuff anything as simple as f str = 4!

Consider

f1 :: forall a, b . Eq a -> Num b

Both Eq a, Num b :: Constraint, so we'd have values of type of kind Constraint. That would basically be a particular dictionary of methods for a given instance. So the implementation of f1 would have to look something like

f1 (EqDict (d_eq :: a -> a -> Bool))
       = NumDict { dict_fromInteger = ??? :: Integer -> b
                 , dict_plus        = ??? :: b -> b -> b
                 , ...
                 , dict_signum      = ??? :: b -> b
                 }

Evidently there is no meaningful way to define all those methods in the result. All you could do with such a "class-function" is to "project" from a stronger class to a weaker one. E.g. you could define

monadApp :: forall m . Monad m -> Applicative m
monadApp (MonadDict {dict_return = d_ret, dict_bind = d_bd})
        = ApplicativeDict { dict_pure = d_ret
                          , dict_app = \fs vs -> d_bd fs (\f -> d_bd vs $ d_ret . f) }

That specific one would be, in fact, somewhat useful, but only because Monad (still, but not for long!) lacks Applicative as a superclass which it should simply have. Normally, there shouldn't be much reason having to explicitly "downgrade" any classes, because superclass-relations (or tuple-ConstraintKinds) do just that automatically.

Answer 2

Type variables may appear more than once in a type signature:

f :: Eq a => a -> a -> a -> Bool

Writing the above as

f :: Eq a -> Eq a -> Eq a -> Bool

looks inconvenient. Worse, we might have more than one constraint on a:

g :: (Show a, Eq a) => a -> Bool

How would we write this in the alternative notation?

g :: (Show & Eq) a -> Bool    -- ??

Forgetting the a completely as you suggest in the last example makes signatures ambiguous: consider

h1 :: (Eq a)       => a -> a -> a -> a -> Bool
h2 :: (Eq a, Eq b) => a -> a -> b -> b -> Bool

These are quite different signatures: you can call h2 1 2 [1] [2] but not h1 1 2 [1] [2] since the latter requires the four arguments to be of the same type. After the proposed convention is used, they are reduced to the same signature:

h12 :: Eq -> Eq -> Eq -> Eq -> Bool

Is the call h12 1 2 [1] [2] valid? The above signature is too ambiguous to tell.