BayHac2013/Denotative Programming

From HaskellWiki
Jump to navigation Jump to search
  • 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.
        • Every operation on 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?