Talks by Edward Kmett and Cody Roux

We have a super exciting meetup this month. Ed's "get off my lawn" talk should appeal to people of all levels of Haskell, and Cody's will be more technical. I'm listing Cody's talk first because Ed's abstract is so long, but Cody will be talking second.

8:00-9:00: Cody Roux - The Structural Theory of Pure Type Systems

We investigate possible extensions of arbitrary given Pure Type Systems with additional sorts and rules which preserve the normalization property. In particular we identify the following interesting extensions: the disjoint union P+Q of two PTSs P and Q , the PTS &∀P.Q which intuitively captures the “ Q -logic of P -terms” and poly P which intuitively denotes the predicative polymorphism extension of P.

These results suggest a new approach to the study of the meta-theory of PTSs, by examination of the relationships between different calculi and predicative extensions which allow more expressiveness with equivalent logical strength.

7:00-8:00: Edward Kmett - Typeclasses vs. the World

I've decided to do a few "get off my lawn" talks on somewhat more polemic issues, mostly so I can get them off my chest online and in one place, and not have to re-articulate myself from scratch every time I'm asked.

There is an oft-repeated notion that implicits a la Scala (confusingly called typeclasses in Coq, Agda, and Idris), module systems, or even object oriented programming techniques are somehow "just better" than Haskell's notion of typeclasses; they let you locally create and pass anything you want at the use site. Strangely, nobody seems to take the other side of the debate -- except to take a cheap shot at Scala now and again!

We'll look at the differences between typeclasses, implicits and ML-style modules. I'll try to tease apart the use cases for making dictionaries first class and see how to recover the safe implicit use cases with typeclasses without giving up coherence, and what you (and your compiler) give up to get the rest.

I'm also often asked if I'd trade in typeclasses for a real module system™ and draw shocked reactions when I say no. Here matters are less clear cut, modules are good for a remarkable number of things, but I hope to articulate a way to think about typeclasses vs. modules that at least drives home the costs and limitations of purely module-based reasoning in terms of refactoring. Along the way I'll showcase how we might look at the role of a better module system (e.g. Backpack) in Haskell.

Lest I come off completely biased, I'll be taking a few shots at the limitations of typeclasses, and talking about the inherent abstraction ceiling and costs of Haskell's current approach. Haskell is bad at abstraction; everyone else is worse.

Finally, we'll also talk about the space of properties for which these tools are equivalent in expressive power, just in case you don't get to write Haskell for your day job and yet still want to reason about your code.

Speaker Bios:

Cody Roux did a PhD in Nancy, France on termination of functionnal programing
languages, and a postdoc at CMU teaching logic and computation. He now
works in formal methods at Draper Laboratories.

Edward Kmett really needs no introduction.

Food:

Pizzas, salad and soda.

Afterwards:

If you'd like to stick around, a number of us tend to head down to the CBC (http://www.cambrew.com/) or another pub afterwards to socialize. If you would like to give a talk or if you have any questions or concerns, please feel free to follow up here or email one of the organizers.