2

我正在尝试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)， wheren1被正确推断为 type 的类型级前身n。我可以添加一个SingI (Pred n)约束，但这只是将问题降低了一级（GHC 现在说它不能推断出 的等价物(SingI (Pred (Pred n)))）。

我怎样才能说服SingI (Pred n)遵循的GHC SingI n（以及为什么singletons软件包没有这样做）？

4

1 回答 1

3

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

singletons通过不安全地实现单例Nat操作来解决这个问题。

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).

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

于 2016-09-02T13:34:02.043 回答