31

作为对各种依赖类型形式化技术进行调查的一部分，我遇到了一篇论文，提倡使用单例类型（有一个居民的类型）作为支持依赖类型编程的一种方式。

根据这个来源，在 Haskell 中，运行时值和编译时类型之间存在分离，当使用单例类型时，由于引入的类型/值同构，它们可能会变得模糊。

我的问题是：在这方面，单例类型与类型类或引用/具体化结构有何不同？

对于使用单例类型的类型理论重要性/优势以及它们在多大程度上可以模拟一般依赖类型，我还特别感谢一些直观的解释。

4

1 回答 1

32
于 2013-04-15T15:22:27.630 回答