Check out my first novel, midnight's simulacra!

Programming Language Theory: Difference between revisions

From dankwiki
Line 111: Line 111:
===Typed Functional Programming===
===Typed Functional Programming===
Two mechanisms were proposed for adding types to the λ-calculus:
Two mechanisms were proposed for adding types to the λ-calculus:
* Church suggested explicit type annotations on all terms (simply-typed λ-calculus (λ<sub>→</sub>))
* Church suggested explicit type annotations on all terms (simply-typed λ-calculus (λ<sub>→</sub>), "simple" due to single type constructor →)
* 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]] (especially in the presence of type inference) 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.