reperiendi

I finally understand the state transformer monad!

Posted in Category theory by Mike Stay on 2008 October 29

It’s the monad arising from the currying adjunction between FX = X \times Y and GZ = Y \multimap Z.  GF attaches an environment Y to X:

GFX = Y \multimap (X \times Y)

This is the type of a function that takes a state of type Y and outputs a result of type X and a new state of type Y. So G is the ability to depend on state and F is the ability to change the state.

The natural transformation \epsilon:FG \Rightarrow 1, is evaluation:

\epsilon_X:(Y \multimap X) \times Y \to X

takes a function and an input point and evaluates the function at that point.  So we get

\mu:GFGF \Rightarrow GF

by evaluating the FG in the middle, while the unit

\eta:1 \Rightarrow GF

is just the curried identity on pairs:

\begin{array}{rl}\eta_X:X & \to Y \multimap (X \times Y) \\ x & \mapsto \lambda y.(x,y)\end{array}

Advertisements

I’m wishing

Posted in Uncategorized by Mike Stay on 2008 October 29

Wonderful talk on applying game design to app design

Posted in Uncategorized by Mike Stay on 2008 October 27

I had an idea like this for training users on a capability-based UI.

http://lostgarden.com/2008/10/princess-rescuing-application-slides.html

You’ve got to believe me…

Posted in Uncategorized by Mike Stay on 2008 October 21

William’s witticisms

Posted in Uncategorized by Mike Stay on 2008 October 18

I was running an I jumped over a plate an I dint crack my head! I’n’t that amazing? I went weeeooo squlksh an I falled in some applesauce.

I have a swim head. My head pops off an I have a swim body.

(William rubs Bruce’s feet.)
Bruce: That feels good!
William: You say funny words!

Wm: Ba’guys punch people.
MJ: Are you a bad guy? You kicked Aidan.
Wm: Ba’guys don’t kick.

Marty (pretending to sword fight): ching ching! Ching!
Wm: (sings) Ching, ching, ching! I love to ching!

Wm (running downstairs to us): I’m NAKED!
MJ: We noticed.
Wm: Yeah. It’s funny. HA HA HA HA!

Mike (noticing Martin’s blue lip): Did you drink the gatorade we told you not to drink?
Marty: William gave it to me and said I should drink it and I drank it.

PhD

Posted in Uncategorized by Mike Stay on 2008 October 10

I’ll be categorifying the lambda calculus.  The nicest way of doing this would be to develop a good notion of a 2-theory, of which “the theory of a cartesian closed category” would be one example.  It’s already known how to do this for cartesian categories: the kind of 2-theory has products itself, and has one type, C; a morphism C \times C \to C for the product in C and a morphism I \to C for the unit; and several 2-morphisms for the diagrams.

Closed categories, however, need some notion of “op,” which is contravariant.  Figuring out the nicest way of doing this will be some fun research.  Paul Mellies has some ideas.

Hopefully, this kind of 2-theory will also let me talk about things like the blue calculus or Tyler Close’s web calculus (where objects are web services and POST is method invocation; lambda terms are stateless objects responding to the unique “call” method) that he uses in waterken.