Mar 30, 2012, 1:38:33 AM3/30/12
There were just Larry and me.
We gleaned (is this the right verb?) over Alex' paper re: arrows, looked into arrows as defined in Haskell, then switched the topic.
I had recently found a nice boolean 2-valued topos with an example of a monad that is not applicative. It is Set^Z2 (s ets with an action of Z2 group).
The problem we were trying to solve is expressing this topos, or this logic, in the terms of types. The types would be sets, like in Hask, but with an attached involution. Sure functions should preserve involution.
While Larry had gradually moved to the idea of having involution defined on types (not on type members), we have not come to any definite theory.
I wonder if anybody knows anything.
This topos, Set^Z2 is especially interesting because it is boolean, but without the AC. So there. Seems like AC, in a weak form probably, is required for the applicativity of monads. Cannot prove though.