类型级别上的函数的模式匹配是可能的,但不是在值级别上,为什么这有区别？

在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

和:

类声明现在引入了一个类型函数Ref(具有指定的类型)以及常用的值函数,例如newRef(每个都具有指定的类型).类似地,每个实例声明都提供了一个子句,它定义了实例类型的类型函数以及每个值函数的见证.

我们说Ref是一个类型族,或Mutation类的相关类型.它的行为类似于类型级别的 函数,因此我们也将Ref称为类型函数.应用类型函数使用与应用类型构造函数相同的语法:上面的参考意味着将类型函数Ref应用于m,然后将结果类型构造函数应用于a.

所以,换句话说,

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

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

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

例如,

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

是不可能写的,因为函数上的相等是不可判定的.

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

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

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

简而言之,类型级函数值上没有模式匹配,只有它们的名称.

在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而不是.

在价值层面,情况并没有太大的不同.实际上,我们有值构造函数,它们是具有名称/标识的特殊函数,以及没有实际标识的常规函数​​.我们可以模式匹配模式,从构造函数构建,但不能与其他任何东西相对

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

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

{-# 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

注意任意函数和类型/数据构造函数之间的区别.构造函数的属性有时被称为生成性.对于两种不同的功能f和g,它很可能也是有可能的是f x = g x对于一些x.另一方面,对于构造函数,f x = g x暗示f = g.这种差异使得第一种情况(任意函数上的模式匹配)不可判定,第二种情况(完全应用的构造函数上的模式匹配)可判定且易于处理.

到目前为止,我们已经看到了类型和价值水平的一致性.

最后,我们已部分应用(包括未应用)构造函数.在类型级别,这些包括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

不支持这一点的原因是效率.类型级别的计算在编译期间以解释模式执行; 因此我们可以承担大量关于类型和类型函数的元数据,以便对它们进行模式匹配.

编译值级别的计算,并且需要尽可能快.保留足够的元数据以支持部分应用的构造函数上的模式匹配会使编译器复杂化并在运行时减慢程序的速度; 为这样一个异国情调的功能支付太多了.