Как применить индуктивное мышление к `GHC.TypeLits.Nat`?

Question

Рассмотрим это определение 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 не может быть бесполезным?.. Как это должно работать?

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