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.

Answer 2

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
import GHC.TypeLits

Let's draw some parallels between the type and value level in Haskell.

First, we have unrestricted functions on both type and value level. On the type level, you can express almost anything using type families. You cannot pattern match on arbitrary functions on either type or value level. E.g. you can't say

type family F (a :: *) :: *
type family IsF  (f :: * -> *) :: Bool where
  IsF F = True
  IsF notF = False

-- Illegal type synonym family application in instance: F
-- In the equations for closed type family ‘IsF’
-- In the type family declaration for ‘IsF’

Second, we have fully applied data and type constructors, such as Just 5 :: Maybe Integer on the value level or Just 5 :: Maybe Nat on the type level.

It is possible to pattern match on these:

isJust5 :: Maybe Integer -> Bool
isJust5 (Just 5) = True
isJust5 _ = False

type family IsJust5 (x :: Maybe Nat) :: Bool where
  IsJust5 (Just 5) = True
  IsJust5 x = False

Note the difference between arbitrary functions and type/data constructors. The property of constructors is sometimes called generativity. For two different functions f and g, it very well may be possible that f x = g x for some x. On the other hand, for constructors, f x = g x implies f = g. This difference makes the first case (pattern-matching on arbitrary functions) undecidable, and the second case (pattern-matching on fully applied constructors) decidable and tractable.

So far we have seen consistency across the type and value level.

Finally, we have partially applied (including un-applied) constructors. On the type level, these include Maybe, IO, and [] (unapplied), as well as Either String and (,) Int (partially applied). On the value level, we have unapplied Just and Left, and partially applied (,) 5 and (:) True.

The generativity condition doesn't care whether the application is full or not; so there's nothing precluding pattern matching for partially applied constructors. That's what you see on the type level; and we could have it on the value level, too.

type family IsLeft (x :: k -> k1) :: Bool where
  IsLeft Left = True
  IsLeft x = False

isLeft :: (a -> Either a b) -> Bool
isLeft Left = True
isLeft _ = False
-- Constructor ‘Left’ should have 1 argument, but has been given none
-- In the pattern: Left
-- In an equation for ‘isLeft’: isLeft Left = True

The reason this is not supported is efficiency. Computations on the type level are carried out during compile time in interpreted mode; so we can afford to carry around lots of metadata about types and type functions to pattern match on them.

Computations on the value level are compiled, and need to be as fast as possible. Keeping enough metadata to support pattern matching on partially applied constructors would complicate the compiler and slow down the program at runtime; it's just too much to pay for such an exotic feature.