Check out my first novel, midnight's simulacra!
Programming Language Theory: Difference between revisions
From dankwiki
No edit summary |
|||
| Line 6: | Line 6: | ||
===Untyped λ-calculus=== | ===Untyped λ-calculus=== | ||
Two operators (function ''definition'' and ''application'') upon one operand type (λ-expression). | Two operators (function ''definition'' and ''application'') upon one operand type (λ-expression). | ||
* Function definition: <tt>(λ'' | * Function definition: <tt>(λ''boundparam''. body)</tt> | ||
* Function application: <tt>function(''actualparam'')</tt> | * Function application: <tt>function(''actualparam'')</tt> | ||
The body is made up of ''free'' and ''bound'' variables. Those not present in the λ's list of bound variables are free. A λ-expression with no free variables is ''closed''. | |||
The integers (or any countably infinite set) can be represented via the [http://en.wikipedia.org/wiki/Church_encoding Church encoding]: | The integers (or any countably infinite set) can be represented via the [http://en.wikipedia.org/wiki/Church_encoding Church encoding]: | ||
* <tt>n ≡ λf. λx . f<sup>n</sup>x</tt> | * <tt>n ≡ λf. λx . f<sup>n</sup>x</tt> | ||
Revision as of 05:58, 7 December 2009
Applicative/Functional Programming
Expressions compose functions rather than values. Backus proposed three tiers of complexity in his Turing Award lecture:
- Simply functional language (fp): No state, limited names, finitely many functional forms, simple substitution semantics, algebraic laws
- Formal functional system (ffp): Extensible functional forms, functions represented by objects, translation of object representation to applicable form, formal semantics
- Applicative state transition system (ast): ffp plus mutable state and coarse-grained operations thereupon
Untyped λ-calculus
Two operators (function definition and application) upon one operand type (λ-expression).
- Function definition: (λboundparam. body)
- Function application: function(actualparam)
The body is made up of free and bound variables. Those not present in the λ's list of bound variables are free. A λ-expression with no free variables is closed. The integers (or any countably infinite set) can be represented via the Church encoding:
- n ≡ λf. λx . fnx
- plus ≡ λm. λn. λf. λx. m f (n f x) (from f(m + n)(x) = fm(fn(x)))
- succ ≡ λn. λf. λx. f (n f x) (β-equivalent to (plus 1) for a defined 1)
- mult ≡ λm. λn. λf. n (m f) (from f(m * n) = (fm)n)
The Church booleans take two arguments, and evaluate to one of them:
- true ≡ λa. λb . a
- false ≡ λa. λb . b
Common syntactic sugar:
- Left-associative application as implicit parentheses
- Use of definitions (allowing identifiers to stand in as λ-expressions)
- Currying: (λx, y. x + y) rather than (λx. (λy. x + y))
- Numeric literals rather than Church encoding
