Pattern match on functions on the type level is possible, but not on the value level, why is this difference?

Question

In this paper by SPJ, on page 3 and 4, it is written:

class Mutation m where
  type Ref m :: * -> *
  newRef :: a -> m (Ref m a)
  readRef :: Ref m a -> m a
  writeRef :: Ref m a -> a -> m ()

instance Mutation IO where
  type Ref IO = IORef
  newRef = newIORef
  readRef = readIORef
  writeRef = writeIORef

instance Mutation (ST s) where
  type Ref (ST s) = STRef s
  newRef = newSTRef
  readRef = readSTRef
  writeRef = writeSTRef

and:

The class declaration now introduces a type function Ref (with a specified kind) alongside the usual value functions such as newRef (each with a specified type). Similarly, each instance declaration contributes a clause defining the type function at the instance type alongside a witness for each value function.

We say that Ref is a type family, or an associated type of the class Mutation. It behaves like a function at the type level, so we also call Ref a type function. Applying a type function uses the same syntax as applying a type constructor: Ref m a above means to apply the type function Ref to m, then apply the resulting type constructor to a.

So, in other words,

Ref :: (*->*)->*->*

that is, Ref takes a type level function as argument, like Maybe or IO or [] and produces another type level function, such as IORef using a pattern match,i.e. Ref is defined by a pattern match.

So, how is it possible that it is possible to pattern match on functions at the type level but not on the value level ?

For example,

fun2int:: (Int->Int)->Int
fun2int (+)=2
fun2int (*)=3

is not possible to write because equality on functions is undecidable.

1) So how is it possible that on the type level this causes no problem ?

2) Is it because the functions on the type level are of very restricted sort ? So not any kind of function on the type level can be an argument to Ref, only a selected few, namely the ones declared by the programmer and not functions like (+), which are more general than the ones declared by the programmer ? Is this the reason why on the type level function pattern match causes no problem ?

3) Is the answer to this question related to this part of the GHC spec?

Answer 1

Briefly put, there is no pattern matching on type-level function values, but only on their name.

In Haskell, as in many other languages, types are kept apart by their name, even if their representation is identical.

data A x = A Int x
data B x = B Int x

Above, A and B are two different type constructors, even if they describe the same type-level function: in pseudo-code \x -> (Int, x), roughly. In a sense, these two identical type-level functions have a different name/identity.

This is different from

type C x = (Int, x)
type D x = (Int, x)

which both describe the same type-level function as above, but do not introduce two new type names. The above are just synonyms: they denote a function, but do not have their own distinct identity.

This is why one can add a class instance for A x or B x, but not for C x or D x: attempting to do the latter would add an instance to the type (Int, x) instead, relating the instance to the type names (,), Int instead.

At the value level, the situation is not so much different. Indeed, there we have value constructors, which are special functions with a name/identity, and regular functions without an actual identity. We can pattern match against a pattern, built from constructors, but not against anything else

case expOfTypeA   of A n t -> ... -- ok
case someFunction of succ -> ...  -- no

Note that at the type level we can't do pattern matching that easily. Haskell allows to do that exploiting type classes, only. This is done to preserve some theoretical properties (parametricity), and to allow an efficient implementation as well (allowing type erasure -- we do not have to tag every value with its type at runtime). These features come at the price of restricting type-level pattern matching to type classes -- this does put some burden on the programmer, but the benefits outweigh the drawbacks.