haskell - 如何定义适合证明的类型级列表索引？

Question

{-# language GADTs, KindSignatures, DataKinds, TypeApplications, TypeOperators,
    TypeFamilies, PolyKinds, UndecidableInstances, RankNTypes, AllowAmbiguousTypes #-}

import GHC.TypeLits

我想用类型级别 Nat 索引类型级别列表:

type family Index (xs :: [a]) (k :: Nat) where
    Index (x:xs) 0 = x
    Index (x:xs) k = Index xs (k - 1)

请注意，我正在使用 GHC.TypeLits.Nat而不是说 data Nat = Z | S Nat ，因为实际参数来自 SNat我想避免在运行时将数字存储在一元中。
此定义适用于具体类型:

*Main> :k! Index [Int, Double, String] 1
Index [Int, Double, String] 1 :: *
= Double

但是，在我的一些函数中，我需要证明Index v n ~ Index (a:v) (n+1) . GHC 本身无法解决这个问题:

prf :: Index v n -> Index (a:v) (n + 1)
prf x = x

    • Couldn't match expected type ‘Index (a : v) (n + 1)’
                  with actual type ‘Index v n’
      NB: ‘Index’ is a non-injective type family
    • In the expression: x
      In an equation for ‘prf’: prf x = x
    • Relevant bindings include
        x :: Index v n (bound at Minimal.hs:11:5)
        prf :: Index v n -> Index (a : v) (n + 1)
          (bound at Minimal.hs:11:1)

是否可以证明这种类型相等？如果没有，我的选择是什么？

Answer 1

Is it possible to prove this type equality?

不幸的是，据我所知，您在这里实际证明任何事情都不走运。您可以对 Nat 执行算术运算s，但 GHC 实际上对它们一无所知。作为一个简单的例子:

> :k! forall n. n + 1 - 1
forall n. n + 1 - 1 :: Nat
= (n + 1) - 1

换句话说，GHC 无法分辨 n + 1 - 1 ~ n .仅从这一点来看，您的定义使用 +而你的字体家族使用 -不会工作。但是，您实际上遇到了更大的麻烦。因为您使用的是 GHC 的 Nat而不是一元的，你已经把你的类型族写成一个封闭的类型族:

type family Index (xs :: [a]) (k :: Nat) where
    Index (x:xs) 0 = x
    Index (x:xs) k = Index xs (k - 1)

为了让 GHC 使用第二种情况，毫无疑问，它必须知道第二个参数不是 0 .但请记住，GHC 对 Nat 上使用的“数学”一无所知。 .例如，它不知道 n + 1永远不会成为 0 .那个+没有真正的数学，它只是一个类型族，GHC 不理解其中的任何逻辑。 GHC 只知道 n + 1是不能减少的类型族应用，所以没有证据表明n不是 0 , 所以 Index不能减少。

If not, what are my alternatives?

嗯，有一个你不喜欢的，那就是使用 data Nat = Z | S Nat .不再有明显的数学，只有构造函数和模式匹配，您甚至不需要关闭类型族就可以使其工作。
您可以做的下一件事是使用类型检查器插件，它实际上了解一些数学知识。虽然我相信这是可行的，但我不知道有任何插件可以做到这一点。也许其他人可以推荐一个，或者你可以自己写一个。
最后一个选择是自己写一些数学公理并使用 unsafeCoerce作为你的“证明”。它远非优雅，但如果它使您的库以您想要的方式工作，那么就去做吧。
在这种情况下，您可以很容易地编写:

prf :: Index (a:v) (n + 1) -> Index v n
prf = unsafeCoerce

并且有很高的信心不会出错。使用 constraints图书馆，你也可以尝试写这样的东西:

axiom1 :: forall a v n. Dict (Index (a:v) (n + 1) ~ Index v n)
axiom1 = unsafeCoerce $ Dict @()

prf :: forall a v n. Index (a:v) (n + 1) -> Index v n
prf = case axiom1 @a @v @n of
  Dict -> id

在这里，我们的 axiom1断言这两种类型是等价的。在 prf ，我们提取出 Dict ，这为我们提供了证据，因此我们可以定义 prf如 id .