如何将归纳推理应用于`GHC.TypeLits.Nat`？

Question

考虑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不能无用吗？它应该如何工作？

Answer 1

没有感应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