8

在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 ma 表示将类型函数 Ref 应用于 m，然后将生成的类型构造函数应用于 a。

所以，换句话说，

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

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

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

例如，

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

不可能写，因为函数的相等性是不可判定的。

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

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

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

4

2 回答 2

7

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

在 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这就是为什么可以为or添加一个类实例B x，但不能为C xor添加一个类实例的原因D x：尝试执行后者会将一个实例添加到类型中，(Int, x)而是将实例与类型名称相关联。(,)Int

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

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

请注意，在类型级别，我们不能那么容易地进行模式匹配。Haskell 只允许利用类型类来做到这一点。这样做是为了保留一些理论属性（参数性），并允许有效的实现（允许类型擦除——我们不必在运行时用其类型标记每个值）。这些特性的代价是将类型级别的模式匹配限制在类型类中——这确实给程序员带来了一些负担，但好处大于坏处。

于 2015-12-31T09:55:55.230 回答
7 
{-# 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

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

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

于 2015-12-31T10:15:45.710 回答