Chr*_*ett 7 haskell type-systems type-theory scala semantics
我正在尝试设计一个本体,例如可以用OWL或Topic Maps定义,包括对多态类型的支持,例如List [T],其中T是Interval Kind In(Nothing,Any)的类型参数,List是功能种类* - >*.最后,我想用语义语言描述一种类型系统本体,它具有足够的细节和严谨性,它可以成为用同一语义语言编写的类型安全软件代码的基础.
考虑到这个目标,我试图弄清楚种类的层次结构,其中类型,区间种类和函数种类都是种类的实例.所有种类的共同"超级"都有正式名称吗？我能提出的最好的术语是"实例".这在类型理论中甚至是一个有意义的概念吗？即使不是这样,我也需要这样一个概念,例如(在Topic Maps术语中)"函数 - 参数 - 类型 - 约束关联有一个角色'允许类型',其播放器必须是'Kind Instance'类型"".
除此之外,我才开始为这个项目开始自学类型理论,在完成它之前我还有很多东西需要学习.我已经阅读了一些关于类型理论的scala相关论文,包括更高级的泛型(http://adriaanm.github.com/files/higher.pdf),并开始通过Scala中的安全类型级抽象工作( http://adriaanm.github.com/files/scalina-final.pdf)和Scala的类型构造函数多态[pdf].我对Haskell的熟悉程度不如Scala,但是我遇到了一些相关的论文,比如System F with Type Equality Coercions [pdf],我需要更深入地掌握Haskell才能理解.如果任何人都可以建议从初学者级别开始学习Haskell类型系统的阅读材料的进展,并一直领导到广义代数数据类型等高级原则,那也是非常值得赞赏的.
最后,如果您知道任何现有尝试用语义本体语言(如OWL或Topic Maps)描述类型系统,或者您对如何执行此操作有任何建议,我也很乐意听到.
Dan*_*ner 10
没有比本杰明皮尔斯的"类型和编程语言"更好的类型理论介绍.我认为上述级别没有标准名称,但"排序"是一种常见的选择.另一个常见的选择是直接跳转到依赖类型并展平层次结构,这样毕竟只有一个级别.在这种情况下添加一个常见的输入规则(当处理其逻辑内容通常不那么重要的日常编程语言时)是"类型:类型"规则,因此,例如,3:Int:Type :类型:类型:...