BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Kleisli Arrows of Outrageous Fortune - Conor McBride\, University 
 of Strathclyde
DTSTART:20110211T140000Z
DTEND:20110211T150000Z
UID:TALK28507@talks.cam.ac.uk
CONTACT:Bjarki Holm
DESCRIPTION:When we program to interact with a turbulent world\, we are to
  some extent at its mercy. To achieve safety\, we must ensure that program
 s act in accordance with what is known about the state of the world\, as d
 etermined dynamically. Is there any hope to enforce safety policies for dy
 namic interaction by static typing? This talk answers with a cautious `yes
 '.\n\nMonads provide structure and a type discipline for effectful program
 ming\, mapping value types to computation types. If we index our types by 
 data approximating the `state of the world'\, we refine our values to witn
 esses for some condition of the world. Ordinary monads for indexed types g
 ive a discipline for effectful programming contingent on state\, modelling
  the whims of fortune in way that Atkey's indexed monads for ordinary type
 s do not. Arrows in the corresponding Kleisli category represent computati
 ons which a reach a given postcondition from a given precondition: their t
 ypes are just specifications in a Hoare logic!\n\nBy way of an elementary 
 introduction to this approach\, I present the example of a monad for inter
 acting with a file handle which is either `open' or `closed'\, constructed
  from a command interface specfied with Hoare-style pre- and postcondition
 s. An attempt to open a file results in a state which is statically unpred
 ictable but dynamically detectable. Well typed programs behave accordingly
  in either case. Haskell's dependent type system\, as exposed by the Strat
 hclyde Haskell Enhancement preprocessor\, provides a suitable basis for th
 is simple experiment.\n\n
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR