考虑 zip
的这个定义对于由 Peano 数字索引的通常向量长度:
{-# 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
关于haskell - 如何将归纳推理应用于 `GHC.TypeLits.Nat` ?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/51917531/