University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Kleisli Arrows of Outrageous Fortune

Kleisli Arrows of Outrageous Fortune

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Bjarki Holm.

When we program to interact with a turbulent world, we are to some extent at its mercy. To achieve safety, we must ensure that programs act in accordance with what is known about the state of the world, as determined dynamically. Is there any hope to enforce safety policies for dynamic interaction by static typing? This talk answers with a cautious `yes’.

Monads provide structure and a type discipline for effectful programming, mapping value types to computation types. If we index our types by data approximating the `state of the world’, we refine our values to witnesses for some condition of the world. Ordinary monads for indexed types give a discipline for effectful programming contingent on state, modelling the whims of fortune in way that Atkey’s indexed monads for ordinary types do not. Arrows in the corresponding Kleisli category represent computations which a reach a given postcondition from a given precondition: their types are just specifications in a Hoare logic!

By way of an elementary introduction to this approach, I present the example of a monad for interacting with a file handle which is either `open’ or `closed’, constructed from a command interface specfied with Hoare-style pre- and postconditions. An attempt to open a file results in a state which is statically unpredictable but dynamically detectable. Well typed programs behave accordingly in either case. Haskell’s dependent type system, as exposed by the Strathclyde Haskell Enhancement preprocessor, provides a suitable basis for this simple experiment.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity