有了這個問題的答案，我能夠在女巫中定義一個串列，長度是型別的一部分：
{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
data Nat = Z | S Nat
data ListF (n :: Nat) a where
Nil :: (ListF 'Z a)
Cons :: a -> ListF m a -> ListF ('S m) a
我希望能夠將普通串列轉換為此類串列。如果做這些：
toListF :: [a] -> ListF n a
toListF [] = Nil
toListF (x:xs) = Cons x (toListF xs)
它不進行型別檢查，因為要[a] -> ListF n a進行型別檢查，函式應該回傳Nat呼叫者需要的任何內容：
ListF.hs:11:14: error:
? Couldn't match type ‘n’ with ‘'Z’
‘n’ is a rigid type variable bound by
the type signature for:
toListF :: forall a (n :: Nat). [a] -> ListF n a
at ListF.hs:10:1-27
Expected type: ListF n a
Actual type: ListF 'Z a
? In the expression: Nil
In an equation for ‘toListF’: toListF [] = Nil
? Relevant bindings include
toListF :: [a] -> ListF n a (bound at ListF.hs:11:1)
|
11 | toListF [] = Nil
| ^^^
Failed, no modules loaded.
我認為它的邏輯型別toListF類似于exists n. [a] -> ListF n aor [a] -> (exists n. ListF n a)，但當然這些不是有效的 haskell 型別。
有可能在haskell中做我想做的事情嗎？如何？
uj5u.com熱心網友回復：
Haskell中有存在型別。
{-# LANGUAGE DataKinds, GADTs, KindSignatures, RankNTypes #-}
data Nat = Z | S Nat
data ListF (n :: Nat) a where
Nil :: (ListF 'Z a)
Cons :: a -> ListF m a -> ListF ('S m) a
data SomeListF a = forall n . AList (ListF n a)
您可以從常規串列轉換為SomeListF：
fromList :: [a] -> SomeListF a
fromList [] = AList Nil
fromList (x:xs) = someCons x (fromList xs) where
someCons x (AList zs) = AList (Cons x zs)
您也可以ListF 從中恢復SomeListF，但只能在受限范圍內。ninforall n不能逃脫，所以你不能有類似的東西
toListF :: SomeListF a -> ListF n a
但你可以有這個：
withSomeList :: (forall n . ListF n a -> b) -> SomeListF a -> b
withSomeList f (AList zs) = f zs
在f引數內部，n是已知的，您可以例如映射您的串列，結果的長度靜態已知與引數的長度相同。這是一個愚蠢的例子：
zipF :: ListF n a -> ListF n b -> ListF n (a, b)
zipF Nil Nil = Nil
zipF (Cons y ys) (Cons z zs) = Cons (y, z) (zipF ys zs)
mapF :: (a->b) -> ListF n a -> ListF n b
mapF _ Nil = Nil
mapF f (Cons z zs) = Cons (f z) (mapF f zs)
zipMapF :: (a->b) -> ListF n a -> ListF n (a, b)
zipMapF f zs = zipF zs (mapF f zs)
zipMapAny :: (a->b) -> ListF n a -> SomeListF (a, b)
zipMapAny f zs = AList (zipMapF f zs)
nums = fromList [1,2,3,4,5]
numsAndSquares = withSomeList (zipMapAny (\x -> x * x)) nums
zipMapAny“知道”其中所有串列的長度是相同的，但它不能將該長度泄漏到結果中。例如，您不能擁有，withSomeList (zipMapF (\x -> x * x)) nums因為n會逃脫。
轉載請註明出處，本文鏈接：https://www.uj5u.com/qukuanlian/494281.html
標籤：哈斯克尔