静态类型检查的设计模式

Question

静态类型检查的设计模式

10

我目前正在尝试确定我的程序中哪些方面可以由Scala编译器进行静态类型检查。阅读这个问题后，我想到了类型的设计模式。我发现很难理解Scala类型系统可能具有的功能。因此，我想看看实际用途（不是Peano算术或类似的东西）。通常在正常代码中经常出现的简单模式。

有人知道任何处理这个问题的博客甚至书籍吗？最好是用Scala编写的，但对其他语言也可能有用。

- ziggystar

为什么这被标记为Haskell？这些链接可能会有所帮助：http://blog.ezyang.com/2010/08/type-kata-controlled-sharing-of-references/ 和 http://blog.ezyang.com/2010/08/type-kata-newtypes/ - Edward Z. Yang

@Edward 因为Scala的类型系统似乎与Haskell的类型系统相似，而且Haskell的模式（它存在更长时间）可能会转移到Java。 - ziggystar

@Edward 我认为这是有效的，因为Scala类型系统中最具冒险精神的实验似乎来自于具有Haskell背景的人，例如Rúnar的博客和Scalaz团队。 - 0__

1

希望能有一些真正全面的东西，甚至是一本书。现在有这么多针对Scala初学者的书籍，我认为有需求的是一本专门讲解静态类型编程设计模式的高级书籍。 - 0__

2个回答

2

您可以查看Haskell的设计建议，特别是一些最近关于将强属性嵌入类型系统的研究论文：

利用Curry-Howard理论 Tim Sheard，2005年ACM SIGPLAN Haskell研讨会论文集。 Tallinn，Estonia，74-85，2005
基于语言的程序验证通过表达性类型 Martin Sulzmann和Razvan Voicu。在编程语言遇见程序验证（PLPV'06）
函数式编程的类型化合同 Ralf Hinze、Johan Jeuring和Andres Loh。
Haskell中轻量级信息流安全的库 A Russo、K Claessen、J Hughes。

目前还没有标准的方法学，但有很多很好的个别问题示例。

- Don Stewart

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- gasche · Accepted Answer

我认为最值得被称为“设计模式”的最有用的技术之一是“幻影类型”技术。这是一种将静态信息编码到类型参数中的更或多或少系统化的方法。以下是一些示例：

您可能还对相关的Oleg奇技淫巧感兴趣：轻量级静态能力（与Chung-chieh Shan合著）。