Robin Milner presented a polymorphic type discipline and its inference algorithm in 1978. Algorithm W derives types from program structure while using unification to satisfy type constraints; suitable let-bound expressions receive reusable type schemes. This work is a foundation of Hindley-Milner type inference.[ref]
A Theory of Type Polymorphism in Programming by Robin Milner. §4.1, Algorithm W; §4.2, syntactic soundness
For example, an identity function has type . Generalizing a let-bound identity permits separate uses at integer and Boolean types, whereas one lambda-bound parameter has one shared type within its scope. The discipline therefore gives precise rules for reuse rather than treating every occurrence as independently polymorphic. Its type-soundness claim concerns specified runtime type errors, not every possible program failure.
Articles by others on the same topic
Robin Milner (1934–2010) was a prominent British computer scientist known for his significant contributions to the fields of programming language design, formal methods, and type theory. He is best known for his work on the development of the ML programming language, which introduced important concepts in functional programming and type inference. Milner also developed the Calculus of Communicating Systems (CCS), a formal language for describing concurrent systems that has had a substantial impact on the study of concurrency in computer science.