haskell - 像其他 Sing 实例一样使用 Data.Singletons 中的 SNat？

Question

我可以使用 SomeSing 来动态生成单例，然后对它们进行模式匹配，从而能够做一些有趣的事情，效果很好

> let x = SomeSing SFalse :: SomeSing ('KProxy :: KProxy Bool)
-- pretend x is dynamically generated using IO or something
> case x of SomeSing SFalse -> blah blah
            SomeSing STrue -> blah blah

但是，我不太确定如何使用 SNat 执行此操作，它是 Sing Nat 的数据系列实例。我遇到的一个问题是，即使导入所有相关模块( SNat 、 Data.Singletons 、 Data.Singletons.TypeLits 等)并启用扩展(即使 Data.Singletons.Prelude 构造函数显示)，我也无法在范围内获取 SNat 数据构造函数当我使用 :browse 和 :i Sing 时)

...我遇到的另一个问题是...没有任何单独的构造函数可以匹配，例如 SFalse 和 STrue ...只有一个构造函数! :O 我该如何以同样的方式使用它？

Answer 1

我认为问题在于有两种自然数单例类型都称为SNat。您似乎找到了与 GHC typelits 搭配的那个。它的构造函数不是从定义模块导出的，但它下面是一个Integer。您可以访问该整数，但整个事情对于证明来说似乎几乎没有用处。另一个 SNat 版本涉及经典的 Peano 自然色。它可以用于证明，但运行时会很慢。我还没有看到 Haskell 在证明和速度方面都具有天然优势。