Programming Language Theory: Difference between revisions
| Line 109: | Line 109: | ||
===Typed Functional Programming=== | ===Typed Functional Programming=== | ||
Two mechanisms were proposed for adding types to the λ-calculus: | |||
* Church suggested explicit type annotations on all terms | |||
* Curry suggested inferred types | |||
Either way, we lose some properties of the untyped λ-calculus (there's no type for the Y-combinator, for instance!). Nonetheless, the benefits of [[Programming_Language_Theory#Typing typing]] lead to most functional programming languages making use of a strict typing system. | |||
===Logic Programming=== | ===Logic Programming=== | ||