[Boston Agda] April 1st 7-9pm in the MIT CSAIL Meeting Room

[Edward Kmett]

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

http://groups.google.com/group/bostonagda

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 

https://github.com/pumpkin/categories

Particularly easy-to-follow theorems include the interchange law, which he was able to prove with only 9 universes

https://github.com/pumpkin/categories/blob/master/Category/NaturalTransformation.agda#L133

and the associativity of horizontal composition for natural transformations, which only required 12 different universes

https://github.com/pumpkin/categories/blob/master/Category/NaturalTransformation.agda#L98

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/

If you have any questions or concerns, please feel free to email the mailing list here at boston...@googlegroups.com or contact me personally at ekm...@gmail.com.

-Edward Kmett

[Isaac Dupree]

But we can't tell how much of your message is an April Fools joke. And
we certainly can't *prove* it, as Agda would suggest we try. I think
we'll have to try harder to become a *successful* Agda community. ;-)

But seriously is whether there's actually a meeting planned on April
1st... a difficult day to arrange anything because people make false
statements regarding it all the time, but then again lots of people try
to do serious things on that day anyway :-(

Cue the suspense...

-Isaac is going outside, where it's warm and summery and has a different
relation to intellectualism.

P.S. I "accidentally" send this to the whole group instead of just Ed
Kmett because of the list's reply-to-list default behaviour, & poke fun
at that default, because it's OBVIOUSLY better than changing the To:
field ;-)

[Edward Kmett]

On Fri, Mar 18, 2011 at 5:04 PM, Isaac Dupree <i...@isaac.cedarswampstudios.org> wrote:

But we can't tell how much of your message is an April Fools joke.  And we certainly can't *prove* it, as Agda would suggest we try.  I think we'll have to try harder to become a *successful* Agda community. ;-)

 

But seriously is whether there's actually a meeting planned on April 1st... a difficult day to arrange anything because people make false statements regarding it all the time, but then again lots of people try to do serious things on that day anyway :-( 

 

In all seriousness, there will be a meeting on that day and the candidate topic descriptions are all accurate -- I even have a real library for semigroupoid theory!

http://hackage.haskell.org/package/semigroupoids

The date was (almost) completely accidental, pigeonholed by the fact that I wanted something two weeks out so people had time to mark their calendars, the availability of speakers, the fact that it should be soon, since we haven't had a meeting in a couple of months, and the fact that I'll be in Bermuda for much of early April.

-Edward

[Rishiyur Nikhil]

The Agdaburg Hemispheres were the first to demonstrate the power of artificial vacuum.

:-)

Nikhil

--
You received this message because you are subscribed to the Google Groups "BostonHaskell" group.
To post to this group, send email to boston...@googlegroups.com.
To unsubscribe from this group, send email to bostonhaskel...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/bostonhaskell?hl=en.