Difference between revisions of "BayHac2013/Denotative Programming"
From HaskellWiki
(talk notes) |
m (Added link to Landin's paper; attempt to clarify grammar) |
||
| Line 1: | Line 1: | ||
<ul> | <ul> | ||
| − | <li><em>[ | + | <li><em>[https://www.cs.cmu.edu/~crary/819-f09/Landin66.pdf The Next 700 Programming Languages]</em>: |
<ul> | <ul> | ||
<li>By Peter Landin in 1966. Enormously important figure in improving our understanding of programming languages. | <li>By Peter Landin in 1966. Enormously important figure in improving our understanding of programming languages. | ||
| Line 23: | Line 23: | ||
<ul> | <ul> | ||
<li>Give your data type a <em>meaning</em> (model). Examples: <code>Image</code> means function of space; <code>Animation</code> means function of time; <code>Sequence</code> means list.</li> | <li>Give your data type a <em>meaning</em> (model). Examples: <code>Image</code> means function of space; <code>Animation</code> means function of time; <code>Sequence</code> means list.</li> | ||
| − | <li> | + | <li>Every operation on your data type must be explainable via the meaning.</li> |
<li>Guides API, and defines correctness.</li> | <li>Guides API, and defines correctness.</li> | ||
<li>Reason on meanings, not on implementations.</li> | <li>Reason on meanings, not on implementations.</li> | ||
Latest revision as of 14:12, 14 October 2021
- 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:
Imagemeans function of space;Animationmeans function of time;Sequencemeans 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?
- 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?