BayHac2013/BayHac2013/Denotative Programming
Jump to navigation
Jump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
- The Next 700 Programming Languages:
- By Peter Landin in 1966. Enormously important figure in improving our understanding of programming languages.
- Prime move with Algol, about which Tony Hoare said “Here is a language so far ahead of its time that it was not only an improvement on its predecessors but also on nearly all its successors.”
- Realized that lambda calculus can model PLs.
- Worked out how to mechanically evaluate lambda calculus.
- The seminal paper on DSELs
- Led to the lambda-calculus-based languages, including Scheme, ML, and Haskell.
- Recommends replacing the fuzzy terms “functional”, “declarative”, and “non-procedural” with the substantive “denotative”.
- “… gives us a test for whether the notation is genuinely functional or merely masquerading.”
- By Peter Landin in 1966. Enormously important figure in improving our understanding of programming languages.
- Denotative:
- Give meaning by mapping to a mathematical type
- Meaning of a composite is a function of the meanings of the components
- Applies to:
- Programming languages
- Programming libraries:
- Give your data type a meaning (model). Examples:
Image
means function of space;Animation
means function of time;Sequence
means list. - Everything operation your data type must be explainable via the meaning.
- Guides API, and defines correctness.
- Reason on meanings, not on implementations.
- For instance:
- Is append on tricky-sequences associative?
- Is my type a monoid, functor, applicative, etc?
- Give your data type a meaning (model). Examples:
- Strong & simple (practical) foundation for (correct) reasoning
- What about Haskell?
- “Purely functional”? Ill-defined question.
- “Purely denotative”? If not, what parts are and what parts are not?