.png){kind=icon}
返回
Qualified Types with Boolean Algebras
.png){kind=icon}
PRE
AI
DOI：10.1145/3763096.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
我们提出了一种基于布尔代数的类型限定符。传统的具有类型限定符的类型系统基于格，但格缺乏表达排斥的能力。我们认为，允许排斥的布尔代数是限定符域的一个实用且有用的选择。在本文中，我们介绍了一种演算系统System F-<:B，它扩展了System F-<:，引入了基于布尔代数的类型限定符，并支持否定、限定符多态和次限定。我们阐述了System F-<:B如何作为类型和效果系统System F-<:BE的设计方法，该系统具有效果多态、次效果和效果多态排斥。我们使用System F-<:BE为Flix编程语言的类型和效果系统奠定形式基础。我们还指出了并实现了一种实用的次效果形式：抽象点次效果。实验结果表明，抽象点次效果使我们能够消除当前Flix标准库中存在的所有效果上转型。
Keyword:
Type Systems
Type Qualifiers
Boolean Algebras
System F-<
Flix
期刊
P
IF:
2.8
论文数:
308
被引数:
4.7K
.png){kind=icon}
查看更多内容