Lambda the Ultimate

Presentations

Besides the expected language designer presentations -

J. Gutknecht
• Criteria for Exclusion of a Construct
• Superfluous, covered by existing construct
• Problematic, contibution to problem set is
  larger than contribution to solution set
• Hidden overhead, no straightforward and
  efficient mapping to runtime exists
• Criteria for Inclusion of a Construct
  • Is extremely useful
  • Has generic character
  • Adds to completeness

and slide 9 "Complexity of syntax of programming languages" in Niklaus Wirth's presentation,

Tkachov (physicist as-end-user/programmer) provides a different perspective

and Brega's robotic art...

Epigram: practical programming with dependent types

Find the type error in the following Haskell expression:

if null xs then tail xs else xs

Found it? Of course you haven't. But this program is obviously nonsense! Unless you're a typechecker, that is. The trouble is that only certain computations make sense if the null xs test is True, whilst others make sense if it is False. However, as far as the type system is concerned, the type of the then branch is the type of the else branch is the type of the entire if . . . then . . . else . . ..

Statically, the test is irrelevant. Which is odd, because if the test really were irrelevant, we wouldn't bother doing it.

We mentioned this issue in discussions. LtU recently featured Epigram with emphasis on its interactive programming abilities, but I would like to add that Conor McBride's papers are mostly about practical use of dependent types for programming. They are also fun to read, though I can easily imagine how his experiments with presentation, like this one, can annoy some people.