# Programming Language Theory: Difference between revisions

From dankwiki

Line 110: | Line 110: | ||

===Typed Functional Programming=== | ===Typed Functional Programming=== | ||

Two | Two agenda were proposed for adding types to the λ-calculus: | ||

* Church suggested explicit type annotations on all terms (simply-typed λ-calculus (λ<sub>→</sub>), "simple" due to single type constructor →) | * Church suggested explicit type annotations on all terms (simply-typed λ-calculus (λ<sub>→</sub>), "simple" due to single type constructor →) | ||

* Curry suggested inferred types (now implemented via techniques such as [http://en.wikipedia.org/wiki/Hindley-Milner_type_inference Hindley-Milner]) | * Curry suggested inferred types (now implemented via techniques such as [http://en.wikipedia.org/wiki/Hindley-Milner_type_inference Hindley-Milner]) |