您如何设计类似类型来执行特定规则？

Question

假设您有一种幼稚的向量类型，例如

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

我对如何以及如何应该 - 实现特定于该类型的构造函数的特定逻辑。我的意思是可以用一个例子来澄清。

假设我要实现：

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

由于模式匹配，我可以很容易地将v2与v2匹配。但是，如果我希望特定组合（例如v2和v3之间）该怎么办？

在这种情况下，是否需要为v2和v3制作单个类型？但是，我不会失去他们目前拥有的多态性特性，是相同类型的？例如，如果我开始构建消耗vector的操作，我目前只需要一个功能。但是，如果我分为两种类型，则需要两个不同的功能。

如何通过类型的思考来解决这个问题？

Answer 1

因此，您希望有时您的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编译器识别v2和v3永远无法匹配因为它们总是具有不同的len参数，但您仍然可以编写适用于任何len的vectorfst。

下一级别 - 不要创建特殊用途len2和len3类型，请使用GHC支持的数字类型级文字：

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

Answer 2

在这种情况下，是否需要为v2和v3制作单个类型？但是，我不会失去他们目前拥有的多态性特性，是相同类型的？例如，如果我开始构建消耗矢量的操作，目前我只需要一个功能。但是，如果我分为两种类型，我需要两个不同的功能。

您需要两个不同的功能 - 但是它们不必有两个不同的名称！为所有类型的向量有意义的所有基本操作上课；然后，如果愿意，您可以根据它们构建高级功能。例如：

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)

计算两个向量的平均长度，它将享受在v2 s或v3 S，即使它仅定义一次。

（实际上，我永远不会将lerp放在vector class;而是我写类应用v =＆gt; vector v其中...代码>定义lifta2。

Answer 3

（因为您可能不想制作vector a num，我将转到Monad操作。）

Haskell的[]单一简单地浏览元素的所有可能组合来解决此问题。例如，[（+1），（*2）]＆lt;*＆gt; [3,6,5] = [4,7,6，6,12,10]。对于您的vector实现仅支持两个或三个元素，这将行不通。将V2（+1）（*2）＆lt;*＆gt; v3 3 6 5有两个或三个元素？因此，您可能想扩展您的类型以支持所有列表，这只会使您直接回到[]。

如果您想维护此“拉链”操作，但是……事情变得更加复杂。可能，但很复杂。基本思想是将向量的长度嵌入到该类型中，同时仍保持多态性。我们从本质上可以使用类型级的自然数量来做到这一点...

data N = Z | S N

（z代表“ Zero”和s“继任者”，例如s（s（s） s（sz）））） = 4）

...我们可以使用数据类型和 gadts ：

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

这里，n是向量的长度。例如，v2将由vector（s（sz））a和v3 by vector> vector（s（s（sz）） ）））。不过，值得注意的是，您可以制作长度多态性，例如vector（s n）a是所有非空置矢量的类型（长度至少为一个）。不幸的是，（GHC的）类型推理在GADT的存在下分解，因此您可能需要范围的类型变量（以及许多显式类型的签名）来执行任何有用的事情。

所有实际的数据定义都在说nil的长度为零，并且在向量（x：^ xs）的元素中，长度比给出的向量多。

例如，这是一个functor实例，定义fmap类似于[

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此处有助于范围a和b，以便可以在go go的类型中使用它们。如果不在 in go将是完全独立的类型变量，只有类似名称。

为了定义更有趣的功能，GHC需要知道我们要与列表的长度进行交互，因此我们定义了一种“完善”长度的Singleton类型...

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

（读取p n为“” n的自然值的证明）

...以及可以访问该类型的类：

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

从这里，我们可以将replicatev类似地定义为[] [] <代码>复制：

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

从这里定义vzip ::（a - ＆gt; b - ＆gt; c） - ＆gt; zip

＆gt; vector n c 类似于 如何制作长度 - 长度 - 媒介物实施的“>”这个问题，以稍微不同的方式扩展了这些想法。）