假設您有一個簡單的向量型別，例如
data Vector a
= V2 a a
| V3 a a a
我感興趣的是你如何——以及你應該如何——實作特定于型別建構式的特定邏輯。我的意思可以用一個例子來說明。
假設我想實作：
instance Num a => Num (Vector a) where
( ) =
(*) = _
abs = _
signum = _
fromInteger = _
negate = _
由于模式匹配，我可以很容易地V2匹配V2. 但是，如果我希望它對特定組合無效，例如 between V2andV3怎么辦？
在這種情況下，是否需要為V2和制作單獨的型別V3？但是，我不會失去它們目前擁有的多型屬性，是相同的型別嗎？例如，如果我開始使用 my 構建操作Vector，我目前只需要一個函式。但是，如果我分成兩種型別，我需要兩個不同的功能。
如何通過思考型別來解決這個問題？
uj5u.com熱心網友回復：
因此，您希望您的 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引數，但您仍然可以撰寫vectorFst適用于任何len.
下一級 - 不要創建特殊用途Len2和Len3型別，使用 GHC 支持的數字型別級文字：
data Vector len a where
V2 :: a -> a -> Vector 2 a
V3 :: a -> a -> a -> Vector 3 a
uj5u.com熱心網友回復：
（因為您可能不想制作Vectora Num，所以我將指代 monad 操作。）
Haskell 的[]monad 通過簡單地遍歷所有可能的元素組合來解決這個問題。例如，[( 1),(*2)] <*> [3,6,5]= [4,7,6, 6,12,10]。但是，對于Vector僅支持兩個或三個元素的實作，這是行不通的。V2 ( 1) (*2) <*> V3 3 6 5會有兩個或三個元素嗎？出于這個原因，您可能希望擴展您的型別以支持所有長度的串列，這只會讓您回到[].
但是，如果您想保持這種“壓縮”操作……事情會變得更加復雜。可能，但很復雜。基本思想是將向量的長度嵌入到型別中，同時仍然保持多型性。我們基本上可以用型別級自然數來做到這一點......
data N = Z | S N
（Z代表“零”和S“繼任者”，例如S (S (S (S Z)))= 4）
...我們可以將其與資料型別和GADT 一起使用：
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是所有非空向量的型別（長度至少為一個）。不幸的是，（GHC 的）型別推斷在存在 GADT 的情況下會失效，因此您可能需要作用域型別變數（以及許多顯式型別簽名）來做任何有用的事情。
所有實際的資料定義都在說Nil長度為零，并且添加到向量 ( ) 的元素的x :^ xs長度比給定的向量大一。
例如，這里有一個Functor實體，定義fmap類似于[]'s 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有助于作用域a，b因此它們可以在 for 型別中使用go。如果它不存在，那么aand binfmap和 the aand bingo將是完全獨立的型別變數，只是名稱相似。
為了定義更有趣的函式，GHC 需要知道我們想要與串列的長度進行互動，所以我們定義了一個“細化”長度的單例型別......
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類似地定義[]'s 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
從這里，您可以定義一個vzip :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c類似于[]'s 的zip。
（另請參閱這個問題，它以稍微不同的方式擴展了這些想法。）
uj5u.com熱心網友回復：
在這種情況下，是否需要為
V2和制作單獨的型別V3？但是，我不會失去它們目前擁有的多型屬性，是相同的型別嗎？例如，如果我開始使用我的 Vector 構建操作，我目前只需要一個函式。但是，如果我分成兩種型別，我需要兩個不同的功能。
您需要兩個不同的函式——但它們不必有兩個不同的名稱！為對任一型別的向量有意義的所有基本操作創建一個類；然后，如果您愿意，您可以根據它們構建更高級別的函式。例如：
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 Applicative v => Vector v where ...和定義lerp = liftA2 . scalarLerp. 這里的開發只是為了說明目的。）
轉載請註明出處，本文鏈接：https://www.uj5u.com/shujuku/477440.html
下一篇：創建一個生成逆矩陣的函式