Given that Haskell is not sufficiently practical for real world programming, we will be renaming ourselves to Boston Agda. Please be patient during the transition. We have yet to figure out how to automatically transfer the membership of this list to the much higher traffic
bosto...@googlegroups.com mailing list.
In the meantime, feel free to sign up on your own at
In unrelated news, the next Boston Agda meeting will be Friday, April 1st from 7pm to 9pm at our usual location, the MIT CSAIL Reading Room (32-G882, which is a room on the 8th floor of the Gates Tower of the MIT's Stata Center at 32 Vassar St in Cambridge, MA).
Keegan McAllister will be talking about his Haskell hdis86 bindings to libudis86. We eagerly await an Agda port.
Then either Derek Elkins will be talking about fibrations -- possibly in Agda -- or I will be talking about how I've completely rebuilt category-extras in terms of semigroupoid theory, eliminating all of those inconvenient identity arrows while stripping the largely superfluous 'return' and 'pure' from Monad and Applicative. Sadly I have not had time to port things to Agda. In the meantime, you may want to familiarize yourself with Dan Peebles' gentle introduction to category theory from
Particularly easy-to-follow theorems include the interchange law, which he was able to prove with only 9 universes
and the associativity of horizontal composition for natural transformations, which only required 12 different universes
Sadly, he has yet to convert his work to semigroupoid theory.
There will be refreshments provided during the break and of course, if you'd like to stick around, a number of us tend to head down to the CBC afterwards and socialize. http://www.cambrew.com/
-Edward Kmett