内容简介：Robin Milner's type system with parametric polymorphism was a significant advance over the systems of Russell and Church. Arguably it is the ability to use type-variables that makes higher order logic a practical vehicle for proving non-trivial theorems. T
Robin Milner's type system with parametric polymorphism was a significant advance over the systems of Russell and Church. Arguably it is the ability to use type-variables that makes higher order logic a practical vehicle for proving non-trivial theorems. The Hindley-Milner algorithm is used to automatically infer types in theorem provers and in several other functional programing languages.
The algorithm, the type system, and some of the logical background are explained inthis tutorial, along with an implementation in standard ML.
This implementation is purely functional and is intended to show the algorithm as clearly as possible. The image above is meant to show that functional languages can be used to express mathematics and logic in such a way that the correspondence between the mathematical and the programmatic expressions may be as exact as one wishes.
This has practical consequences. In implementing the algorithm in ML I found several errors and ambiguities in the mathematical expression. These were cleared up in the process of constructing the mechanical expression of the algorithm. The errors would have been detected by the syntax and type-checking of the compiler, and the ambiguity is resolved by the specification of standard ML semantics which is more precise than any informal description of mathematical notation that I have ever seen. Because ML is equally expressive but more exact, I argue that the ML program is a a better description of the algorithm than the mathematical one.
Standard ML is Milner's language which uses this parametric polymorphic type system. The core of the implementation of the type inference algorithm consists in some 250 lines of code. It does not include any explicit type annotation at all, yet the type of each and every expression is inferred (and thereby checked) by the same algorithm which is part of the compiler.
The algorithm was proved sound and complete by Damas and Milner in 1982 and the proof is outlined in Principal type-schemes for functional programs which I have re-keyed because the paper is so well-written and deserves to be more widely read.
The source code is available as a plain text SML source file and as html formatted standard ML .
以上就是本文的全部内容，希望本文的内容对大家的学习或者工作能带来一定的帮助，也希望大家多多支持 码农网
猜你喜欢:
本站部分资源来源于网络，本站转载出于传递更多信息之目的，版权归原作者或者来源机构所有，如转载稿涉及版权问题，请联系我们。
Python编程实践
Jennifer Campbell、Paul Gries、Jason Montojo、Greg Wilson / 唐学韬 / 机械工业出版社华章公司 / 2011-12-31 / 49.00元
Python是当今世界流行的编程语言之一。本书共15章，通过一些短小精悍的交互式Python脚本帮助学生进行练习，并在这个过程中掌握诸如数据结构、排序和搜索算法、面向对象编程、数据库访问、图形用户界面等基本概念以及良好的程序设计风格。本书既是一本注重科学的计算机科学专业教材，也是一本目标明确的Python参考书。 本书语言风格言简意赅，图表丰富，简单实用，是一本优秀的Python入门级读物，......一起来看看 《Python编程实践》 这本书的介绍吧!
