haskell - 函数在类型级别上的模式匹配是可能的，但在值级别上则不行，为什么会出现这种差异？

Question

在 this SPJ 的论文，第 3 页和第 4 页写道:

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

和:

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.

所以，换句话说，

引用::(*->*)->*->*

也就是说，Ref 采用类型级别函数作为参数，例如 Maybe 或 IO 或 []并生成另一个类型级函数，例如使用模式匹配的IORef，即Ref 由模式匹配定义。

那么，怎么可能在类型级别上对函数进行模式匹配，而不是在值级别上进行模式匹配呢？

例如，

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

无法写入，因为函数的相等性是 undecidable 。

1)那么在类型级别上这怎么可能不会导致问题呢？

2) 是不是因为类型级别上的函数的排序非常有限？因此，并不是类型级别上的任何类型的函数都可以作为 Ref 的参数，只有选定的少数函数，即由程序员声明的函数，而不是像 (+) 这样的函数，它们比由程序员声明的？这就是类型级别函数模式匹配不会导致问题的原因吗？

3) 这个问题的答案与 this 相关吗？ GHC 规范的一部分？

Answer 1

简单地说，类型级函数值上没有模式匹配，只有它们的名称。

在 Haskell 中，与许多其他语言一样，类型通过名称来区分，即使它们的表示形式相同。

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

上面，A 和 B 是两个不同的类型构造函数，即使它们描述相同的类型级函数:在伪代码中 \x -> (Int, x)，粗略地说。从某种意义上说，这两个相同的类型级函数具有不同的名称/标识。

这与

不同

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

它们都描述了与上面相同的类型级函数，但没有引入两个新的类型名称。以上只是同义词:它们表示一个函数，但没有自己独特的标识。

这就是为什么可以为 A x 或 B x 添加类实例，但不能为 C x 或 D 添加类实例x:尝试执行后者会向类型 (Int, x) 添加一个实例，并将该实例与类型名称 (,) 相关联，改为Int。

在值(value)层面，情况并没有太大不同。事实上，我们有值构造函数，它们是具有名称/标识的特殊函数，以及没有实际标识的常规函数​​。我们可以针对从构造函数构建的模式进行模式匹配，但不能针对其他任何内容进行模式匹配

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

请注意，在类型级别，我们无法轻松进行模式匹配。 Haskell 只允许利用类型类来做到这一点。这样做是为了保留一些理论属性(参数性)，并允许有效的实现(允许类型删除——我们不必在运行时用其类型标记每个值)。这些功能的代价是将类型级模式匹配限制为类型类——这确实给程序员带来了一些负担，但利大于弊。