Roman,
> Has anybody made proofs with the IO monads?
> What kind of program transformation is possible with monads?
> Are there new ways to think about monad-based programs?
Not much has been done on reasoning specifically about IO monads. The IO
monad in the new version of Haskell is only defined informally so no formal
proofs are possible. In my thesis, now available as a book
http://www.cl.cam.ac.uk/users/adg/fpio.html
the last chapter deals with a monad that incorporates state, character I/O and
exceptions, and I showed formally how to do some simple program
transformations.
Reasoning about monads in general is more established. Moggi's computational
lambda-calculus or Pitts' evaluation logic are two early frameworks.
@article{moggi89a,
author="Eugenio Moggi",
title="Notions of Computations and Monads",
journal=TCS, year=1989, volume=93, pages="55--92",
note="Earlier version in LICS'89"}
@InProceedings{pitts90,
author = "Andrew M. Pitts",
title = "Evaluation Logic",
editor = "G. Birtwistle",
booktitle = "IVth Higher Order Workshop, Banff 1990",
publisher="Springer Verlag", series="Workshops in Computing",
year=1991, pages="162--189"}
See http://theory.doc.ic.ac.uk/tfm/papers/PittsAM/
Also, as you probably know, there's been a good deal of work on monads
for lazy functional programming. But as far as I know, very little of this
work is concerned with proving facts about the resulting programs; instead the
thrust has been on showing that monads let you cleanly incorporate state.
Hence the questions you raise are good directions for future research.
Andy Gordon.
Phone: (+44) 1223 334411 University of Cambridge Computer Laboratory,
Fax: (+44) 1223 334679 New Museums Site, CAMBRIDGE CB2 3QG, UK.
Email: [EMAIL PROTECTED]
Web: http://www.cl.cam.ac.uk/users/adg/
