BayHac2013/BayHac2013/Denotative Programming

• 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.”
• 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?
  • 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?