Programming Language Theory: Difference between revisions
| Line 113: | Line 113: | ||
* Church suggested explicit type annotations on all terms | * Church suggested explicit type annotations on all terms | ||
* Curry suggested inferred types | * 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. | 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]] (especially in the presence of type inference) lead to most functional programming languages making use of a strict typing system. | ||
===Logic Programming=== | ===Logic Programming=== | ||