Fun with Type Functions
Fun with Type Functions
复制标题
类型函数的乐趣
DOI：
10.1007/978-1-84882-912-1_14
复制
发表时间：
2010
影响因子：
6.2
通讯作者：
Chung
中科院分区：
文献类型：
--
作者：
O. Kiselyov;S. Jones;Chung
Tony Hoare一直是编写和证明程序性质的领导者。为了自动证明程序的属性，目前使用最广泛的技术是无处不在的类型检查器。唉，静态类型系统不可避免地排除了一些好的程序，而允许一些坏的程序。因此，我们描述了我们在Haskell中获得的一些乐趣，通过使类型系统更具表达性，而不会失去自动证明和紧凑表达的好处。具体来说，我们提供了一个程序员对所谓的类型家族的参观，这是Haskell的一个最新扩展，它允许类型上的函数像值上的函数一样直接表达。这种功能使程序员更容易通过编写在类型检查期间执行的函数式程序来有效地扩展编译器。所有示例的源代码都可以在http://research.microsoft.com/simonpj/papers/assoc-types/fun-with-type-funs.zip上获得。
Tony Hoare has always been a leader in writing down and proving properties of programs. To prove properties of programs automatically, the most widely used technology today is the ubiquitous type checker. Alas, static type systems inevitably exclude some good programs and allow some bad ones. Thus motivated, we describe some fun we have been having with Haskell, by making the type system more expressive without losing the benefits of automatic proof and compact expression. Specifically, we offer a programmer’s tour of so-calledtype families, a recent extension to Haskell that allows functions on types to be expressed as straightforwardly as functions on values. This facility makes it easier for programmers to effectively extend the compiler by writing functional programs that execute during type checking. Source code for all the examples is available at http://research.microsoft.com/simonpj/papers/assoc-types/fun-with-type-funs.zip.