Difference between revisions of "BayHac2013/BayHac2013/Denotative Programming"
Jump to navigation
Jump to search
(Talk notes) |
(oops. accidental extra indirection.) |
||
| Line 1: | Line 1: | ||
| + | oops. accidental extra indirection. |
||
| − | <ul> |
||
| − | <li><em>[http://www.scribd.com/doc/12878059/The-Next-700-Programming-Languages The Next 700 Programming Languages]</em>: |
||
| − | <ul> |
||
| − | <li>By Peter Landin in 1966. Enormously important figure in improving our understanding of programming languages. |
||
| − | <ul> |
||
| − | <li>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.”</li> |
||
| − | <li>Realized that lambda calculus can model PLs.</li> |
||
| − | <li>Worked out how to mechanically evaluate lambda calculus.</li> |
||
| − | </ul></li> |
||
| − | <li>The seminal paper on DSELs</li> |
||
| − | <li>Led to the lambda-calculus-based languages, including Scheme, ML, and Haskell.</li> |
||
| − | <li>Recommends replacing the fuzzy terms “functional”, “declarative”, and “non-procedural” with the substantive “denotative”.</li> |
||
| − | <li>“… gives us a test for whether the notation is genuinely functional or merely masquerading.”</li> |
||
| − | </ul></li> |
||
| − | <li>Denotative: |
||
| − | <ul> |
||
| − | <li>Give meaning by mapping to a mathematical type</li> |
||
| − | <li>Meaning of a composite is a function of the meanings of the components</li> |
||
| − | <li>Applies to: |
||
| − | <ul> |
||
| − | <li>Programming <em>languages</em></li> |
||
| − | <li>Programming <em>libraries</em>: |
||
| − | <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>Everything operation your data type must be explainable via the meaning.</li> |
||
| − | <li>Guides API, and defines correctness.</li> |
||
| − | <li>Reason on meanings, not on implementations.</li> |
||
| − | <li>For instance: |
||
| − | <ul> |
||
| − | <li>Is append on tricky-sequences associative?</li> |
||
| − | <li>Is my type a monoid, functor, applicative, etc?</li> |
||
| − | </ul></li> |
||
| − | </ul></li> |
||
| − | </ul></li> |
||
| − | <li>Strong & simple (practical) foundation for (correct) reasoning</li> |
||
| − | </ul></li> |
||
| − | <li>What about Haskell? |
||
| − | <ul> |
||
| − | <li>“Purely functional”? Ill-defined question.</li> |
||
| − | <li>“Purely denotative”? If not, what parts are and what parts are not?</li> |
||
| − | </ul></li> |
||
| − | </ul> |
||
Revision as of 02:26, 22 May 2013
oops. accidental extra indirection.