在 Haskell 中处理涉及 CmpNat 和单例的证明

Question

我正在尝试创建一些函数来处理以下类型。以下代码使用 GHC-8.4.1 上的 singletons and constraints 库：

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Constraint ((:-))
import Data.Singletons (sing)
import Data.Singletons.Prelude (Sing(SEQ, SGT, SLT), (%+), sCompare)
import Data.Singletons.Prelude.Num (PNum((+)))
import Data.Singletons.TypeLits (SNat)
import GHC.TypeLits (CmpNat, Nat)

data Foo where
  Foo
    :: forall (index :: Nat) (len :: Nat).
       (CmpNat index len ~ 'LT)
    => SNat index
    -> SNat len
    -> Foo

这是一个包含长度和索引的 GADT。索引保证小于长度。

编写一个函数来创建 Foo:

很容易

createFoo :: Foo
createFoo = Foo (sing :: SNat 0) (sing :: SNat 1)

但是，我在编写一个递增 len 同时保持 index 相同的函数时遇到了问题：

incrementLength :: Foo -> Foo
incrementLength (Foo index len) = Foo index (len %+ (sing :: SNat 1))

失败并出现以下错误：

file.hs:34:34: error:
    • Could not deduce: CmpNat index (len GHC.TypeNats.+ 1) ~ 'LT
        arising from a use of ‘Foo’
      from the context: CmpNat index len ~ 'LT
        bound by a pattern with constructor:
                   Foo :: forall (index :: Nat) (len :: Nat).
                          (CmpNat index len ~ 'LT) =>
                          SNat index -> SNat len -> Foo,
                 in an equation for ‘incrementLength’
        at what5.hs:34:17-29
    • In the expression: Foo index (len %+ (sing :: SNat 1))
      In an equation for ‘incrementLength’:
          incrementLength (Foo index len)
            = Foo index (len %+ (sing :: SNat 1))
    • Relevant bindings include
        len :: SNat len (bound at what5.hs:34:27)
        index :: SNat index (bound at what5.hs:34:21)
   |
34 | incrementLength (Foo index len) = Foo index (len %+ (sing :: SNat 1))
   |                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

这是有道理的，因为编译器知道 CmpNat index len ~ 'LT（根据 Foo 的定义），但不知道 CmpNat index (len + 1) ~ 'LT.

有什么方法可以让这样的东西发挥作用吗？

可以使用 sCompare 做这样的事情：

incrementLength :: Foo -> Foo
incrementLength (Foo index len) =
  case sCompare index (len %+ (sing :: SNat 1)) of
    SLT -> Foo index (len %+ (sing :: SNat 1))
    SEQ -> error "not eq"
    SGT -> error "not gt"

然而，当我知道它们永远不会匹配时，我不得不为 SEQ 和 SGT 编写案例似乎很不幸。

此外，我认为可以创建如下类型：

plusOneLTProof :: (CmpNat n m ~ 'LT) :- (CmpNat n (m + 1) ~ 'LT)
plusOneLTProof = undefined

但是，这会产生如下错误：

file.hs:40:8: error:
    • Couldn't match type ‘CmpNat n0 m0’ with ‘CmpNat n m’
      Expected type: (CmpNat n m ~ 'LT) :- (CmpNat n (m + 1) ~ 'LT)
        Actual type: (CmpNat n0 m0 ~ 'LT) :- (CmpNat n0 (m0 + 1) ~ 'LT)
      NB: ‘CmpNat’ is a non-injective type family
      The type variables ‘n0’, ‘m0’ are ambiguous
    • In the ambiguity check for ‘bar’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        bar :: (CmpNat n m ~  'LT) :- (CmpNat n (m + 1) ~  'LT)
   |
40 | bar :: (CmpNat n m ~ 'LT) :- (CmpNat n (m + 1) ~ 'LT)
   |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

我猜这是有道理的，因为 CmpNat 是非单射的。但是，我知道这个含义是正确的，所以我希望能够编写这个函数。

我想回答以下两个问题：

有没有一种方法可以将 incrementLength 写成只需要匹配 SLT 的地方？我可以更改 Foo 的定义以使这更容易。
有没有办法写成plusOneLTProof，或者至少是类似的东西？

Update：我最终使用了 Li-yao Xia 的建议来编写 plusOneLTProof 和 incrementLength，如下所示：

incrementLength :: Foo -> Foo
incrementLength (Foo index len) =
  case plusOneLTProof index len of
    Sub Dict -> Foo index (len %+ (sing :: SNat 1))

plusOneLTProof :: forall n m. SNat n -> SNat m -> (CmpNat n m ~ 'LT) :- (CmpNat n (m + 1) ~ 'LT)
plusOneLTProof SNat SNat = Sub axiom
  where
    axiom :: CmpNat n m ~ 'LT => Dict (CmpNat n (m + 1) ~ 'LT)
    axiom = unsafeCoerce (Dict :: Dict (a ~ a))

这需要您将两个 SNat 传递给 plusOneLTProof，但不需要 AllowAmbiguousTypes。

Answer 1

编译器拒绝 plusOneLTProof 因为它的类型不明确。我们可以使用扩展 AllowAmbiguousTypes 禁用该约束。我建议将它与 ExplicitForall 一起使用（这由 ScopedTypeVariables 暗示，无论如何我们肯定需要，或者 RankNTypes）。那是为了定义它。具有不明确类型的定义可以与 TypeApplications.

一起使用

然而，GHC 仍然不能对自然数进行推理，所以我们不能定义 plusOneLTProof = Sub Dict，更不用说 incrementLength，不安全。

但是我们仍然可以用 unsafeCoerce 凭空创建证明。这实际上就是 constraints 中的 Data.Constraint.Nat 模块的实现方式；不幸的是，它目前不包含任何关于 CmpNat 的事实。强制转换有效是因为类型等式中没有运行时内容。即使运行时值看起来不错，断言不连贯的事实仍然会导致程序出错。

plusOneLTProof :: forall n m. (CmpNat n m ~ 'LT) :- (CmpNat n (m+1) ~ 'LT)
plusOneLTProof = Sub axiom
  where
    axiom :: (CmpNat n m ~ 'LT) => Dict (CmpNat n (m+1) ~ 'LT)
    axiom = unsafeCoerce (Dict :: Dict (a ~ a))

为了使用证明，我们对其进行特殊化（TypeApplications）并对其进行模式匹配以在上下文中引入 RHS，检查 LHS 是否成立。

incrementLength :: Foo -> Foo
incrementLength (Foo (n :: SNat n) (m :: SNat m)) =
  case plusOneLTProof @n @m of
    Sub Dict -> Foo n (m %+ (sing :: SNat 1))

在 Haskell 中处理涉及 CmpNat 和单例的证明

working with proofs involving CmpNat and singletons in Haskell

haskell

constraints

type-families

type-level-computation

singleton-type