你如何设计相似的类型来执行特定的规则?

How do you design similar types to enforce particular rules?

假设您有一个朴素的向量类型,例如

data Vector a
  = V2 a a
  | V3 a a a

我感兴趣的是您可以如何——以及您应该如何——实现特定于类型构造函数的特定逻辑。我的意思可以用一个例子来说明。

假设我要实现:

instance Num a => Num (Vector a) where
  (+) = 
  (*) = _
  abs = _
  signum = _
  fromInteger = _
  negate = _

由于模式匹配,我可以很容易地将 V2V2 匹配。但是,如果我希望它对特定组合无效怎么办,例如在 V2V3 之间?

这样的话,是否需要为V2V3做单独的类型?但是,那么,我是否不会失去它们当前拥有的多态属性,因为它们是同一类型?例如,如果我开始构建使用我的 Vector 的操作,我目前只需要一个函数。但是,如果我分成两种类型,我需要两个不同的功能。

如何通过类型思考解决这个问题?

所以您希望您的 ADT 案例有时看起来像不同的类型,这样它们就不会意外混合,但有时您又希望能够对它们进行同类处理?这就是 GADT 的用途(除其他外)。

给你的类型一个幻像类型参数,并强制它对于不同的构造函数是不同的。如果您不在乎,您可以将该类型参数设为通用:

data Len2
data Len3

data Vector len a where
  V2 :: a -> a -> Vector Len2 a
  V3 :: a -> a -> a -> Vector Len3 a

vectorAdd :: Num a => Vector len a -> Vector len a -> Vector len a
vectorAdd (V2 x1 y1) (V2 x2 y2) = V2 (x1+x2) (y1+y2)
vectorAdd (V3 x1 y1 z1) (V3 x2 y2 z2) = V3 (x1+x2) (y1+y2) (z1+z2)

vectorFst :: Vector len a -> a
vectorFst (V2 x _) = x
vectorFst (V3 x _ _) = x

vectorAdd 中,编译器认为 V2V3 永远无法匹配,因为它们总是具有不同的 len 参数,但您仍然可以编写 vectorFst 适用于任何 len.

下一级 - 不要创建 special-purpose Len2Len3 类型,使用 GHC 支持的数字 type-level 文字:

data Vector len a where
  V2 :: a -> a -> Vector 2 a
  V3 :: a -> a -> a -> Vector 3 a

(因为您可能不想让 Vector 成为 Num,我将改为指 monad 操作。)

Haskell 的 [] monad 通过简单地遍历所有可能的元素组合来解决这个问题。例如,[(+1),(*2)] <*> [3,6,5] = [4,7,6, 6,12,10]。但是,对于仅支持两个或三个元素的 Vector 实现,这是行不通的。 V2 (+1) (*2) <*> V3 3 6 5 会有两个或三个元素吗?出于这个原因,您可能希望扩展您的类型以支持所有长度的列表,这只会让您回到 [].

如果您想保持这种“压缩”操作,但是……事情会变得更加复杂。可能,但复杂。基本思想是将向量的长度嵌入到类型中,同时仍然保持多态性。我们基本上可以用 type-level 自然数来做到这一点...

data N = Z | S N

(Z 代表“零”,S 代表“后继”,例如 S (S (S (S Z))) = 4)

...我们可以利用它 data kinds and GADTs:

data Vector n a where
    Nil :: Vector 'Z a
    (:^) :: a -> Vector n a -> Vector ('S n) a

这里,n是向量的长度。例如,V2 将由 Vector (S (S Z)) a 表示,而 V3 将由 Vector (S (S (S Z))) a 表示。但是,值得注意的是,您可以使长度多态,例如Vector (S n) a 是所有 non-empty 向量的类型(长度至少为一个)。不幸的是,(GHC 的)类型推断在 GADT 存在的情况下会崩溃,因此您可能需要 scoped type variables(以及大量显式类型签名)来做任何有用的事情。

所有实际的数据定义都在说 Nil 的长度为零,并且向量前面的元素 (x :^ xs) 的长度比给定的向量多 1。

例如,这里有一个 Functor 实例,定义 fmap 类似于 []map:

instance Functor (Vector n) where
    fmap :: forall a b. (a -> b) -> Vector n a -> Vector n b
    fmap f = go where
        go :: Vector k a -> Vector k b
        go Nil = Nil
        go (x:^xs) = f x :^ go xs

注意散落在各​​处的所有类型签名。不幸的是,这几乎总是必要的,因为 GHC 不太热衷于在 GADT 存在的情况下假设多态性。这里的 forall 帮助范围 ab 以便它们可以在 go 的类型中使用。如果它不存在,那么 fmap 中的 ab 以及 go 中的 ab 将是完全独立的类型变量,只是名称相似。

为了定义更多有趣的函数,GHC 需要知道我们想要与列表的长度进行交互,所以我们定义了一个“细化”长度的单例类型...

data P n where
    PZ :: P 'Z
    PS :: P n -> P ('S n)

(阅读 P n 作为“n 自然价值的证明)

...和一个 class 可以访问该类型:

class Nat n where
    nat :: P n
instance Nat 'Z where
    nat = PZ
instance Nat n => Nat (S n) where
    nat = PS nat

从这里,我们可以定义 replicateV 类似于 []replicate:

replicateV :: forall n a. Nat n => a -> Vector n a
replicateV x = go nat where
    -- read as "go takes a proof of k's value and returns a vector of length k"
    go :: P k -> Vector k a
    go PZ = Nil
    go (PS p) = x :^ go p

从这里,您可以定义类似于 []zipvzip :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c

(另请参阅 ,它以稍微不同的方式扩展了这些想法。)

In this case, is it required to make individual types for V2 and V3? Then, however, do I not lose the polymorphic properties they currently have, being the same type? For example, if I begin building operations consuming my Vector, I currently need only one function. However, if I split into two types, I need two distinct functions.

您需要两个不同的函数 -- 但它们不必有两个不同的名称!为对任何一种类型的向量有意义的所有基本操作做一个 class;然后你可以根据需要构建 higher-level 函数。例如:

data V2 a = V2 a a
data V3 a = V3 a a a

class Vector v where
    magnitude :: Floating a => v a -> a
    lerp :: Floating a => a -> v a -> v a -> v a

scalarLerp :: Floating a => a -> a -> a -> a
scalarLerp alpha a b = alpha*a + (1-alpha)*b

instance Vector V2 where
    magnitude (V2 x y) = sqrt (x^2 + y^2)
    lerp alpha (V2 x y) (V2 x' y') = V2
        (scalarLerp alpha x x')
        (scalarLerp alpha y y')

instance Vector V3 where
    magnitude (V3 x y z) = sqrt (x^2 + y^2 + z^2)
    lerp alpha (V3 x y z) (V3 x' y' z') = V3
        (scalarLerp alpha x x')
        (scalarLerp alpha y y')
        (scalarLerp alpha z z')

然后你可以定义,比如说,

midMagnitude :: (Vector v, Floating a) => v a -> v a -> a
midMagnitude v1 v2 = magnitude (lerp 0.5 v1 v2)

来计算两个向量的平均值的长度,并且它将享受在 V2s 或 V3s 上工作的良好多态性 属性,即使它只是定义一次。

(实际上,我永远不会把 lerp 放在 Vector class 中;相反,我会写 class Applicative v => Vector v where ... 并定义 lerp = liftA2 . scalarLerp。这里的发展只是为了说明目的。)