考虑由Peano数字索引的通常矢量长度的zip的定义:
{-# language DataKinds #-}
{-# language KindSignatures #-}
{-# language GADTs #-}
{-# language TypeOperators #-}
{-# language StandaloneDeriving #-}
{-# language FlexibleInstances #-}
{-# language FlexibleContexts #-}
module Vector
where
import Prelude hiding (zip)
data N
where
Z :: N
S :: N -> N
data Vector (n :: N) a
where
VZ :: Vector Z a
(:::) :: a -> Vector n a -> Vector (S n) a
infixr 1 :::
deriving instance Show a => Show (Vector n a)
class Zip z
where
zip :: z a -> z b -> z (a, b)
instance Zip (Vector n) => Zip (Vector (S n))
where
zip (x ::: xs) (y ::: ys) = (x, y) ::: zip xs ys
instance Zip (Vector Z)
where
zip _ _ = VZ
-- ^
-- λ :t zip (1 ::: 2 ::: 3 ::: VZ) (4 ::: 5 ::: 6 ::: VZ)
-- zip (1 ::: 2 ::: 3 ::: VZ) (4 ::: 5 ::: 6 ::: VZ)
-- :: (Num a, Num b) => Vector ('S ('S ('S 'Z))) (a, b)
-- λ zip (1 ::: 2 ::: 3 ::: VZ) (4 ::: 5 ::: 6 ::: VZ)
-- (1,4) ::: ((2,5) ::: ((3,6) ::: VZ))
输入一元数会很麻烦(即使我对此有一个宏)。幸运的是，这里有
GHC.TypeLits。让我们使用它:module Vector
where
import Prelude hiding (zip)
import GHC.TypeLits
data Vector (n :: Nat) a
where
VZ :: Vector 0 a
(:::) :: a -> Vector n a -> Vector (n + 1) a
infixr 1 :::
deriving instance Show a => Show (Vector n a)
class Zip z
where
zip :: z a -> z b -> z (a, b)
instance Zip (Vector n) => Zip (Vector (n + 1))
where
zip (x ::: xs) (y ::: ys) = (x, y) ::: zip xs ys
instance Zip (Vector 0)
where
zip _ _ = VZ
- 但不是:
• Illegal type synonym family application in instance:
Vector (n + 1)
• In the instance declaration for ‘Zip (Vector (n + 1))’
|
28 | instance Zip (Vector n) => Zip (Vector (n + 1))
| ^^^^^^^^^^^^^^^^^^^^
因此，我将类替换为普通函数:
zip :: Vector n a -> Vector n b -> Vector n (a, b)
zip (x ::: xs) (y ::: ys) = (x, y) ::: zip xs ys
zip VZ VZ = VZ
-但是现在我不能再使用归纳推理了:
Vector.hs:25:47: error:
• Could not deduce: n2 ~ n1
from the context: n ~ (n1 + 1)
bound by a pattern with constructor:
::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + 1) a,
in an equation for ‘zip’
at Vector.hs:25:6-13
or from: n ~ (n2 + 1)
bound by a pattern with constructor:
::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + 1) a,
in an equation for ‘zip’
at Vector.hs:25:17-24
‘n2’ is a rigid type variable bound by
a pattern with constructor:
::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + 1) a,
in an equation for ‘zip’
at Vector.hs:25:17-24
‘n1’ is a rigid type variable bound by
a pattern with constructor:
::: :: forall a (n :: Nat). a -> Vector n a -> Vector (n + 1) a,
in an equation for ‘zip’
at Vector.hs:25:6-13
Expected type: Vector n1 b
Actual type: Vector n2 b
• In the second argument of ‘zip’, namely ‘ys’
In the second argument of ‘(:::)’, namely ‘zip xs ys’
In the expression: (x, y) ::: zip xs ys
• Relevant bindings include
ys :: Vector n2 b (bound at Vector.hs:25:23)
xs :: Vector n1 a (bound at Vector.hs:25:12)
|
25 | zip (x ::: xs) (y ::: ys) = (x, y) ::: zip xs ys
| ^^
我没有观察到明显的东西吗？这些
TypeLits不能没有用吗？..它应该如何工作？ 最佳答案
TypeLits上没有任何归纳法，默认情况下确实使它们几乎无用，但是您可以通过两种方式改善这种情况。
使用 ghc-typelits-natnormalise 。这是一个GHC插件，它在类型检查器中添加了算术求解器，并使GHC认为许多相等的Nat表达式相等。这非常方便，并且与下一个解决方案兼容。您的zip可以立即使用。
假定您需要的任何属性。 为了避免潜在的内存安全问题，应仅假定真实语句的证明，并且仅假定相等性或其他与计算无关的数据类型的证明。例如，您的zip可以通过以下方式工作:
{-# language
RankNTypes, TypeApplications, TypeOperators,
GADTs, TypeInType, ScopedTypeVariables #-}
import GHC.TypeLits
import Data.Type.Equality
import Unsafe.Coerce
data Vector (n :: Nat) a
where
VZ :: Vector 0 a
(:::) :: a -> Vector n a -> Vector (n + 1) a
lemma :: forall n m k. (n :~: (m + 1)) -> (n :~: (k + 1)) -> m :~: k
lemma _ _ = unsafeCoerce (Refl @n)
vzip :: Vector n a -> Vector n b -> Vector n (a, b)
vzip VZ VZ = VZ
vzip ((a ::: (as :: Vector m a)) :: Vector n a)
((b ::: (bs :: Vector k b)) :: Vector n b) =
case lemma @n @m @k Refl Refl of
Refl -> (a, b) ::: vzip as bs