我正在嘗試撰寫一個take適用于長度索引向量的版本。這要求取自的數小于或等于向量的長度。
這是我的代碼的當前版本：
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
data SNat (n :: Nat) where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
data Vec (n :: Nat) (a :: Type) where
Nil :: Vec Zero a
Cons :: a -> Vec n a -> Vec (Succ n) a
class (m :: Nat) >= (n :: Nat)
instance m >= Zero
instance m >= n => (Succ m >= Succ n)
take :: (m >= n) => SNat n -> Vec m a -> Vec n a
take (SZero ) _ = Nil
take (SSucc n) (x `Cons` xs) = x `Cons` (take n xs)
但是，我收到了這個錯誤，我不確定如何解決：
* Could not deduce (n2 >= n1) arising from a use of `take'
from the context: m >= n
bound by the type signature for:
take :: forall (m :: Nat) (n :: Nat) a.
(m >= n) =>
SNat n -> Vec m a -> Vec n a
at src\AnotherOne.hs:39:1-48
or from: (n :: Nat) ~ ('Succ n1 :: Nat)
bound by a pattern with constructor:
SSucc :: forall (n :: Nat). SNat n -> SNat ('Succ n),
in an equation for `take'
at src\AnotherOne.hs:41:7-13
or from: (m :: Nat) ~ ('Succ n2 :: Nat)
bound by a pattern with constructor:
Cons :: forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a,
in an equation for `take'
at src\AnotherOne.hs:41:17-27
Possible fix:
add (n2 >= n1) to the context of the data constructor `Cons'
* In the second argument of `Cons', namely `(take n xs)'
In the expression: x `Cons` (take n xs)
In an equation for `take':
take (SSucc n) (x `Cons` xs) = x `Cons` (take n xs
我嘗試了幾種不同的型別類迭代，使用 OVERLAPS 甚至 INCOHERENT，但我無法修復它。HLS 還告訴我模式匹配不完整，說我不匹配(SSucc SZero) Niland (SSucc (SSucc _)) Nil。
但是，如果我嘗試寫：
test = take (SSucc SZero) Nil
它正確錯誤Couldn't match type ‘'Zero’ with ‘'Succ 'Zero’，表明我的問題特別出在函式定義中，因為從一些測驗來看，該函式的 API 似乎是正確的。
最后，有人建議我為此使用一個型別族，這樣做：
type (>=~) :: Nat -> Nat -> Bool
type family m >=~ n where
m >=~ Zero = True
Succ m >=~ Succ n = m >=~ n
_ >=~ _ = False
type m >= n = m >=~ n ~ True
哪個確實有效，但我試圖使用 Haskell 實體解決這個問題。作為一個附帶問題，一個比另一個有什么好處嗎？
uj5u.com熱心網友回復：
問題是您的>=類的介面并沒有以任何方式表達一個數字至少與另一個數字一樣大的含義。
為此，我建議重構單例型別以明確區分兩種可能的情況：
data SZero (n :: Nat) where
SZero :: SZero 'Zero
data SPositive (n :: Nat) where
SSucc :: SNat n -> SPositive ('Succ n)
type SNat n = Either (SZero n) (SPositive n)
此外，我們需要有一種方法來表示回滾型別級別的歸納步驟。這里我們需要一個型別族，但它可以比你的簡單得多>=~：
type family Pred (n :: Nat) :: Nat where
Pred ('Succ n) = n
請注意，這不是全部！沒關系：型別族可以安全地指向 nowhere。您仍然可以在編譯器可以推斷出適用的子句的背景關系中使用它們。
現在我們可以制定類。您注意到缺少的關鍵定理是，在這種Succ情況下，您可以對前輩應用歸納。更準確地說，我們只需要知道n是正數，以便能夠將m ≥ n屬性降級為兩個數的前身。即數學陳述是
m≥n∧正（n）?pred（m ） ≥pred （n）。
我們現在可以準確地表達這一點，使用 CPS 技巧將蘊含箭頭降級為值級別：
class m>=n where
atLeastAsPositive :: SPositive n -> (Pred m >= Pred n => r) -> r
對于這種Zero情況，這個定理甚至不適用，但這沒問題——我們知道無論如何都沒有合適的單例，所以我們可以安全地使用空大小寫匹配：
instance m >= 'Zero where
atLeastAsPositive s = case s of {}
有趣的情況是正數之一。通過我們制定型別的方式，編譯器可以輕松地連接執行緒：
instance m >= n => ('Succ m >= 'Succ n) where
atLeastAsPositive (SSucc _) φ = φ
take最后，我們在您的函式中呼叫該定理：
take :: ? m n a . (m >= n) => SNat n -> Vec m a -> Vec n a
take (Left SZero) _ = Nil
take (Right s@(SSucc n)) (x `Cons` xs)
= atLeastAsPositive @m s (x `Cons` (take n xs))
轉載請註明出處，本文鏈接：https://www.uj5u.com/ruanti/490526.html