无法推断前任 Nat 的 SingI

Posted 2023-05-08

【中文标题】无法推断前任 Nat 的 SingI

【英文标题】：Could not deduce SingI of predecessor Nat

【发布时间】：2017-01-10 14:39:06

【问题描述】：

我正在尝试为有限的整数集编写一个weaken 函数。我正在使用singletons 包。我已经定义并推广了加法、减法和前驱函数，并证明了它们的一些方程以帮助类型检查器。但我得到的错误与这一切完全无关。

weaken :: forall n m k . (SingI n, SingI m, SingI k, (Minus m n) ~ NatJust k) => Fin n -> Fin m
weaken ZF =  gcastWith (apply Refl $ plus_minus sm sn sk) ZF
  where sn = sing :: SNat n
        sm = sing :: SNat m
        sk = sing :: SNat k
weaken (SF n) = gcastWith (apply Refl $ succ_pred sm) (SF (weaken n))
  where sn = sing :: SNat n
        sm = sing :: SNat m
        sk = sing :: SNat k

我得到的错误是在weaken (SF (weaken n)) 的递归调用上，如下：Could not deduce (SingI n1)，其中n1 被正确推断为类型n 的类型级前身.我可以添加一个SingI (Pred n) 约束，但这只会将问题向下移动一个级别（GHC 现在说它无法推断出(SingI (Pred (Pred n))) 的等价物）。

我如何让 GHC 相信 SingI (Pred n) 来自 SingI n（为什么 singletons 包没有这样做）？

【参考方案1】：

GHC.TypeLits，最终为我们提供了类型级别的非负Integer-s，不导出任何可以让我们进行单例运行时操作的函数。例如，给定KnownNat a 和KnownNat b，没有标准函数可以在运行时生成KnownNat (a + b)。

singletons 通过不安全地实现singleton Nat operations 解决了这个问题。

singletons 减法函数对负数结果抛出一个错误（并且不会像我们希望的那样截断为 0），所以我们不能为 pred 重用它，必须自己实现它：

-# language TypeApplications #- -- plus all the usual exts

import Data.Singletons.Prelude
import Data.Singletons.TypeLits
import Unsafe.Coerce

type family Pred (n :: Nat) :: Nat where
  Pred 0 = 0
  Pred n = n :- 1

sPred :: Sing n -> Sing (Pred n)
sPred sn = case fromSing sn of
  0 -> unsafeCoerce (sing @_ @0)
  n -> case toSing @Nat (n - 1) of
    SomeSing sn -> unsafeCoerce sn

您可以使用sPred 获取Sing (Pred n)，然后使用withSingI 或singInstance 将其转换为SingI (Pred n)。

但是，您可能不应该在weaken 中使用SingI。 SingI 的目的是在除了将它们转发给其他函数之外不将它们用于任何事情的上下文中自动插入单例参数。相反，只需使用Sing，您就可以避免sing 并键入注释噪音。以我的经验，Sing 在大约 90% 的时间用于 singletons 编程比 SingI 更可取。