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

我可以很好地使用SomeSing来动态生成Singleton，然后对它们进行模式匹配，以完成有趣的工作

> 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我应该如何以相同的方式使用它？

最佳答案

我相信问题在于，有两种自然数单身人士类型都称为SNat。您似乎发现的一种与GHC字样有关。它的构造函数不是从定义模块导出的，而是下面的Integer。您可以访问该整数，但是整个过程似乎对于证明没有多大用处。其他SNat版本处理经典的Peano天然元素。它可以用作证明，但运行时会很慢。对于证明和速度，我还没有看到Haskell天生的优势。

关于haskell - 是否像其他Sing实例一样使用Data.Singletons中的SNat？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/32793397/