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

Question

在 SPJ 的 this 论文中，第 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 :: (*->*)->*->*

即，Ref 将类型级函数作为参数，如 Maybe 或 IO 或 [] 并生成另一个类型级函数，如 IORef 使用 模式匹配 ，即Ref 由 模式匹配定义 。

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

例如，

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

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

1) 那么这怎么可能在类型级别上没有问题呢？

2) 是不是因为类型级别的函数种类非常有限？因此，在类型级别上，不是任何类型的函数都可以作为 Ref 的参数，只有少数几个，即程序员声明的函数，而不是像 (+) 这样的函数，它们比由声明的函数更通用程序员？这就是为什么在类型级别上函数模式匹配没有问题的原因吗？

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

Answer 1

简而言之，type-level 函数 values 没有模式匹配，只有它们的 name.

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

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

上面，A和B是两个不同的类型构造函数，即使它们描述了相同的type-level函数：在pseudo-code\x -> (Int, x)中，大致. 从某种意义上说，这两个相同的 type-level 函数具有不同的 name/identity.

这不同于

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

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

这就是为什么可以为 A x 或 B x 添加 class 实例，但不能为 C x 或 D x 添加实例的原因：试图做后者会向类型 (Int, x) 添加一个实例，而是将实例与类型名称 (,)、Int 相关联。

在价值层面，情况并没有太大的不同。事实上，我们有值构造函数，它们是带有 name/identity 的特殊函数，以及没有实际身份的常规函数。我们可以针对模式进行模式匹配，该模式由构造函数构建，但不能针对其他任何东西

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

请注意，在类型级别，我们无法轻松进行模式匹配。 Haskell 仅允许利用类型 classes 进行此操作。这样做是为了保留一些理论属性（参数性），并允许高效的实现（允许类型擦除——我们不必在运行时用它的类型标记每个值）。这些特性的代价是将 type-level 模式匹配限制为 classes 类型——这确实给程序员带来了一些负担，但利大于弊。

Answer 2

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

让我们在 Haskell.

中的类型和价值级别之间画一些相似之处

首先，我们在类型和值级别上都有不受限制的功能。在类型级别，您几乎可以使用类型族来表达任何东西。您不能在类型或值级别的任意函数上进行模式匹配。例如。你不能说

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’

其次，我们充分应用了数据和类型构造函数，例如值级别的Just 5 :: Maybe Integer或类型级别的Just 5 :: Maybe Nat。

可以对这些进行模式匹配：

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

注意任意函数和 type/data 构造函数 之间的区别。构造函数的属性有时被称为 生成性 。对于两个不同的函数 f 和 g，很可能 f x = g x 对于某些 x。另一方面，对于构造函数，f x = g x 意味着 f = g。这种差异使得第一种情况（pattern-matching 在任意函数上）不可判定，而第二种情况（pattern-matching 在完全应用的构造函数上）可判定且易于处理。

到目前为止，我们已经看到了类型和值级别的一致性。

最后，我们已经部分应用了（包括un-applied）构造函数。在类型级别上，这些包括 Maybe、IO 和 []（未应用），以及 Either String 和 (,) Int（部分应用）。在价值层面，我们没有应用Just和Left，部分应用了(,) 5和(:) True。

生成条件不关心应用程序是否已满；所以没有什么可以排除部分应用的构造函数的模式匹配。这就是您在类型级别上看到的；而且我们也可以在价值层面拥有它。

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

不支持的原因是效率。类型级别的计算在编译期间以解释模式执行；所以我们负担得起携带大量关于类型和类型函数的元数据以进行模式匹配他们。

值级别的计算已编译，需要尽可能快可能的。保留足够的元数据以支持部分模式匹配应用的构造函数会使编译器复杂化并减慢程序速度运行;为这样一个奇特的功能付出太多了。

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

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

haskell

type-families

higher-order-types