Dependently typed programming with singletons
Dependently typed programming with singletons
复制标题
使用单例进行依赖类型编程
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Stephanie Weirich
中科院分区：
文献类型：
--
作者：
R. Eisenberg;Stephanie Weirich
Haskell程序员已经使用巧妙的编码来实现了至少十年来尝试使用依赖类型的类型。但是，这些编码的聪明也是它们的主要缺点。尽管这些想法受到依赖类型程序的启发，但该代码看起来显着不同。结果，GHC实施者对Haskell类型系统（例如GADTS，Type系列和数据类型促销）进行了响应。但是，在Haskell中的编程和依赖类型的语言中的编程之间仍然存在显着差异。 Haskell在运行时值和编译时类型之间执行相位分离。因此，单胎类型对于表达价值和类型之间的依赖性是必需的。这些Singleton类型为程序员介绍了开销和冗余。
本文介绍了Singletons库，该库生成了使用GHC依赖类型编程所需的样板代码。为了与全光谱语言进行比较，我们提供了一个基于AGDA接口的扩展示例，用于安全数据库访问。本文以详细的讨论进行了详细的讨论，该论点介绍了GHC当前的功能，以进行相关键入的编程和未来扩展的建议，以更好地支持这种编程风格。
Haskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limits of the Haskell type system. However, the cleverness of these encodings is also their main drawback. Although the ideas are inspired by dependently typed programs, the code looks significantly different. As a result, GHC implementors have responded with extensions to Haskell's type system, such as GADTs, type families, and datatype promotion. However, there remains a significant difference between programming in Haskell and in full-spectrum dependently typed languages. Haskell enforces a phase separation between runtime values and compile-time types. Therefore, singleton types are necessary to express the dependency between values and types. These singleton types introduce overhead and redundancy for the programmer.
This paper presents the singletons library, which generates the boilerplate code necessary for dependently typed programming using GHC. To compare with full-spectrum languages, we present an extended example based on an Agda interface for safe database access. The paper concludes with a detailed discussion on the current capabilities of GHC for dependently typed programming and suggestions for future extensions to better support this style of programming.