IO with integrated constraint

[aspiwack]

As I was typing the file handle example, I realised that it may be a bit annoying to design a do-notation desugaring which would both handle IO (a .<= c) and IO a. Maybe we should just bake in the constraint in IO directly.

Something like:

data IO c a = RealWorld ->. (RealWorld, a .<= c)

(plus some complication so that a can be either linear or unrestricted)

We can always use IO () a for the standard case.

[kcsongor]

This would mean that >>= needs to change both a and c, right?

We would need something along the lines of
(>>=) :: IOL c a -> (c =>. a -> IOL d b) -> IOL d b

If we have a bind like that, then we need to be careful about how the constraint resolution works out for the bound functions. To be concrete, say we have some classes

class A
class B

and some foo :: IOL (A, B) Int, i.e. a computation that "outputs" an A and a B.

and some function f :: A =>. Int -> IOL () Char, i.e. it consumes an A constraint.
I think we should be able to bind foo into f!

foo >>= f :: IOL B Char

so the constraint solver ought to work out that A =>. a .<= () is a "subtype" of (A, B) =>. a .<= B. This doesn't seem to hard, as the relationship is covariant in both inputs and outputs.

This means that the desugaring would be quite simple in that functions always consume all linear constraints, and possibly pass some of them on to the next computation.

[aspiwack]

(sorry about the delayed response)

This would mean that >>= needs to change both a and c, right?

Yes. The way I think of it is that c =>. (a .<= c') is sort of an indexed monad (so here, we are using the index monad transformer corresponding to it, I suppose), albeit a very convenient one to use. I'd imagine that we want to use a do notation to thread the classes around (instead of explicitly casing on a .<= c all the time).

so the constraint solver ought to work out that A =>. a .<= () is a "subtype" of (A, B) =>. a .<= B. This

Well, if you want to do it in a point-free notation, it may well be. But if you write

do
x <- foo
f x

Then, my intention is that the A, and B constraints are made available when x is bound (like what happens when we pattern-match on Dict).