Anonymous

Programming Language Theory: Difference between revisions

From dankwiki
Line 113: Line 113:
* 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])
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. More complicated systems (''second-'' and higher-''order  λ-calculi'') such as System F (aka Girard-Reynolds polymorphic λ-calculus) exist; they can be explored along Barendregt's [http://en.wikipedia.org/wiki/Lambda_cube λ-cube], should one feel so inclined.
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. More complicated systems (''second-'' and higher-''order  λ-calculi'') such as System F (aka Girard-Reynolds polymorphic λ-calculus) exist; they can be explored along Barendregt's [http://en.wikipedia.org/wiki/Lambda_cube λ-cube], should one feel so inclined (I don't particularly recommend it, unless you like to stare at things like F<sub>&lt;:</sub><sup>ω</sup>).


===Logic Programming===
===Logic Programming===