作为对各种依赖类型化形式化技术进行调查的一部分,我遇到了一篇论文,主张使用单例类型(具有一个居民的类型)作为支持依赖类型编程的一种方式.
根据这个来源,在Haskell中,由于诱导类型/值同构,在使用单例类型时,运行时值和编译时类型之间存在分离.
我的问题是:在这方面,单身类型与类型类或引用/具体结构有何不同？
我还特别理解关于使用单一类型的类型 - 理论重要性/优点以及它们一般可以模拟依赖类型的程度的一些直观解释.
我正在阅读一篇关于依赖类型编程的论文,并且发现了以下引用:
"[...]与Haskell的类型类相比,数据类型[...]是封闭的 ",在某种意义上说,如果不扩展数据类型,就无法向Universe添加新类型.
我的新手问题是:Haskell类型类在什么意义上打开？它们如何可扩展？此外,拥有此属性(开放与封闭)的类型理论后果是什么？
谢谢!
我试图找出类型层次结构如何在Agda中工作.
假设我定义了一个集合类型X:
X : Set
然后继续构建归纳型
data Y : X -> Set where
是什么类型的X -> Set？是设置还是类型？
谢谢!