Monthly Archives: August 2008

Slicing open the belly of the IO monad in an alternate universe

I’ve been looking for a way to do the pieces of I/O that are well-defined in the framework of FRP. For example, fileContents "someFile" is a perfectly good function of time, why should we be forced to drop into the semantic fuzziness of the IO monad to get it?

Well, after a long talk with the Anygma folks about it, getting not very far in the practical world, I decided to do something else to quench my thirst for the time being since software needs to get written. I’m going to have the FRP program request actions by sending sinks to the top level, and then have the results of those requests come back via futures. So:

type Sink a = a -> IO ()
type Pipe = forall a. (Future a, Sink a)
data Stream a = a :> Stream a

liftFRP :: Sink a -> IO a -> IO ()
liftFRP sink a = a >>= sink

Okay, that’s nice, but how do we prevent uses of these things from becoming a tangled mess. Input always needs to communicate with output, and it seems like it would just be a pain to coordinate that. It turns out we can stick it in a monad:

newtype StreamReaderT v m a = SRT { runSRT :: StateT (Stream v) m a) }
    deriving (Functor, Monad, MonadTrans)
readNext = SRT $ do
    (x :> xs) <- get
    put xs
    return x

type IO' = StreamReaderT Pipe (WriterT (IO ()) Future)
-- using the IO () monoid with mappend = (>>)

liftFRP :: IO a -> IO' a
liftFRP io = do
    (fut,sink) <- readNext
    tell (io >>= sink)
    (lift.lift) fut

unliftFRP :: IO' a -> IO a
unliftFRP m = do
    stream <- makePipeStream  -- a bit of magic here
    ((fut,_),action) <- runWriterT (runStateT (runSRT m) stream)
    action
    return $! futVal fut

It looks like IO’ has the very same (lack of) semantics as IO. liftFRP and unliftFRP form an isomorphism, so we really can treat them as pulling apart the IO monad into something more versatile, and then putting it back together.

Also we get nice fun parallel version of liftFRP. I can’t decide if this should be the common one or not.

liftParFRP :: IO a -> IO' a
liftParFRP io = do
    (fut,sink) <- readNext
    tell (forkIO (io >>= sink))
    (lift.lift) fut

So using the liftFRP and unliftFRP, we are no longer “trapped in IO” as some folks like to say. We can weave in and out of using IO as we’re used to and using requests and futures when convenient. For example, it’s trivial to have a short dialog with the user via the console, and have the real time program ticking away all the while. Fun stuff!

All functions are continuous, always

Dan Piponi and Andrej Bauer have written about computable reals and their relationship to continuity. Those articles enlightened me, but only by way of example. Each of them constructed a representation for real numbers, and then showed that all computable functions are continuous on that representation.

Today, I will show that all functions are continuous on every representation of real numbers.

This article assumes some background in domain theory.

I’m going to use the following definition of analytic continuity:

f is continuous if for any chain of open sets x1 ⊇ x2 ⊇ …, i f[xi] = f[∩i xi]

Where ∩ denotes the intersection of a set of sets, and f[x] denotes the image of f under x (the set {f(z) | z in x}).

This means that for a continuous function, the intersection of a bunch of images of that function is the same as the image of the intersection of the sets used to produce those images (whew!). It might take you a little while to convince yourself that this really means continuous in the same way as it is normally presented. The proof is left as an exercise to the reader (yeah, cop-out, I know).

I chose this definition because it is awfully similar to the definition of Scott continuity from domain theory, which all computable functions must have.

A monotone function f is scott-continuous if for any chain of values x1 ⊑ x2 ⊑ …, supi f(xi) = f(supi xi).

Where ⊑ is the “information” partial ordering, and sup is the supremum, or least upper bound, of a chain. Analogous to the last definition, this means that the supremum of the outputs of a function is the same as the function applied to the supremum of the inputs used to create those outputs.

What I will do to show that every computable function is continuous, no matter the representation of reals, is to show that there is a homomorphism (a straightforward mapping) from Scott continuity to analytic continuity.

But first I have to say what it means to be a real number. It turns out this is all we need:

fromConvergents :: [Rational] -> Real
toConvergents :: Real -> [Rational]

These functions convert to and from infinite convergent streams of rationals. They don’t need to be inverses. The requirement we make is that the rational at position n needs to be within 2-n of the actual number represented (the same as Dan Piponi’s). But if a representation cannot do this, then I would say its approximation abilities are inadequate. To make sure it is well-behaved, toConvergents(fromConvergents(x)) must converge to the same thing as x.

Now we will make a homomorphism H from these Reals (lifted, so they can have bottoms in them) to sets (precisely, open intervals) of actual real numbers.

Range will be a function that maps lists to a center point and an error radius.

Range(⊥) = ⟨0,∞⟩
Range(r:⊥) = ⟨r,1⟩
Range(r:rs) = ⟨r’,e/2⟩ where ⟨r’,e⟩ = Range(rs)

And now H:

H(x) = (r-e,r+e) where ⟨r,e⟩ = Range(toConvergents(x))
H(⊑) = ⊇
H(sup) = ∩
H(f) = H ° f ° fromConvergents ° S, where S(x) gives a cofinal sequence of rational numbers less than x that satisfies the error bound requirement above.

The hard part of the proof is H ° f ° fromConvergents = H(f) ° H ° fromConvergents for fully defined inputs; in other words that the homomorphism does actually preserve the meaning of the function. It boils down to the fact that H ° fromConvergents ° S is the identity for fully defined inputs, since Range(x) is just {lim x} when x is fully defined. I expect some of the details to get a bit nasty though. Left as an exercise for a reader less lazy than the author.

And that’s it. It means when you interpret f as a function on real numbers (namely, H), it will always be continuous, so long as the computable real type you’re using has well-behaved toConvergents and fromConvergents functions.

Intuitively, H maps the set of convergents to the set of all possible numbers it could represent. So ⊥ gets mapped to the whole real line, 0:⊥ gets mapped to the interval (-1,1) (all the points within 1 of 0), etc. The analytical notion of continuity above can be generalized to any function on sets, rather than just f[] (the image function of f). This means we can define continuity (which is equivalent to computability) on, for example, functions from Real to Bool.

This was a fairly technical explanation, where I substituted mathematical reasoning for intuition. This is partially because I’m still trying to truly understand this idea myself. Soon I may post a more intuitive / visual explanation of the idea.

If you want to experiment more, answer: what does it mean for a function from Real -> Bool to be continuous?

Mindfuck: The Reverse State Monad

Someone in the #haskell IRC channel mentioned the “reverse state monad” explaining that it used the state from the next computation and passed it to the previous one. Well, I just had to try this!

First, a demonstration: we will compute the fibonacci numbers by starting with them and mapping them back to the empty list.

-- cumulativeSums [1,2,3,4,5] = [0,1,3,6,10,15]
cumulativeSums = scanl (+) 0

computeFibs = evalRState [] $ do
    -- here the state is what we want: the fibonacci numbers
    fibs <- get
    modify cumulativeSums
    -- now the state is the difference sequence of
    -- fibs, [1,0,1,1,2,3,5,8,13,...], because the
    -- cumulativeSums of that sequence is fibs.  Notice
    -- that this sequence is the same as 1:fibs, so
    -- just put that to get here.
    put (1:fibs)
    -- And here the state is empty (or whatever else
    -- we want it to be, because we just overwrite it on
    -- the previous line -- but we defined it to be
    -- empty on the evalRState line)
    return fibs

And sure enough:

>>> take 15 computeFibs
[0,1,1,2,3,5,8,13,21,34,55,89,144,233,377]

And now the implementation:

newtype RState s a = RState { runRState :: s -> (a,s) }
evalRState s f = fst (runRState f s)

instance Monad (RState s) where
    return x = RState $ (,) x
    RState sf >>= f = RState $ \s ->
        let (a,s'') = sf s'
            (b,s') = runRState (f a) s
        in (b,s'')

get = RState $ \s -> (s,s)
modify f = RState $ \s -> ((),f s)
put = modify . const

The important part is the definition of (>>=). Notice how the data (a,b) flows forward, but the state (s,s’,s”) flows backward.

Braid!

I just had my mind blown by the trial of Braid, by Jonathan Blow, which just came out on XBox Live Arcade. This is the most interesting puzzle game I have played in many years. It’s a platformer about playing with time, and in incorporates this very effectively to allow clever solutions to puzzles which seem impossible. Not very many games get my money these days, but this one does!

Bravo!

Composable Input for Fruit

The other day I had an idea for a game which required a traditionalish user interface (text boxes, a grid of checkboxes, …). But I’m addicted to Haskell at the moment, so I was not okay with doing it in C#, my usual GUI fallback. Upon scouring hackage for a GUI widget library I could use, I realized that they all suck—either they are too imperative or too inflexible.

So I set out to write yet another one, in hopes that it wouldn’t suck. The plan is to write it on top of graphics-drawingcombinators, my lightweight declarative OpenGL wrapper, and reactive, the latest (in progress) implementation of FRP. In researching the design, Conal pointed me to a paper on “Fruit”, which is a very simple design for GUIs in FRP. It’s nice (because it is little more than FRP itself), and it’s approximately what I’m going to do. But before I do, I had to address a big grotesque wart in the design:

data Mouse = Mouse { mpos :: Point,
                     lbDown :: Bool,
                     rbDown :: Bool }
data Kbd = Kbd { keyDown :: [Char] }
type GUIInput = (Maybe Kbd, Maybe Mouse)
type GUI a b = SF (GUIInput,a) (Picture,b)

So every GUI transformer takes a GUIInput as a parameter. The first thing that caught my eye was the Maybes in the type of GUIInput, which are meant to encode the idea of focus. This is an example of the inflexibility I noticed in the existing libraries: it is a very limited, not extensible, not customizable idea of focus. But there is something yet more pressing: this input type is not composable. The type of input is always the same, and there is no way to build complex input handling from simple input handling.

I took a walk, and came up with the following:

Scrap GUI. Our interface will be nothing more than pure FRP. But that doesn’t solve the input problem, it just gives it to the users to solve. So to solve that, we build up composable input types, and then access them using normal FRP methods.

We will start with Kbd and Mouse as above. The problem to solve is that when we pass input to a subwidget, its local coordinate system needs to be transformed. So the only cabability input types need to have is that they need to be transformable.

-- A class for invertable transformations.  We restrict to affine transformations
-- because we have to work with OpenGL, which does not support arbitrary
-- transformation.
class Transformable a where
    translate :: Point -> a -> a
    rotate    :: Double -> a -> a
    scale     :: Double -> Double -> a -> a

instance Transformable Point where
    -- .. typical affine transformations on points

-- Keyboard input does not transform at all
instance Transformable Kbd where
    translate _ = id
    rotate _ = id
    scale _ _ = id

-- The mouse position transforms
instance Transformable Mouse where
    translate p m  = m { mpos = translate p (mpos m) }
    rotate theta m = m { mpos = rotate r (mpos m) }
    scale sx sy m  = m { mpos = scale sx sy (mpos m) }

-- Behaviors transform pointwise.  In fact, this is the instance
-- for Transformable on any Functor, but we have no way of telling
-- Haskell that.
instance (Transformable a) => Transformable (Behavior a) where
    translate = fmap . translate
    rotate = fmap . rotate
    scale sx sy = fmap (scale sx sy)

Widgets that accept input will have types like: Behavior i -> Behavior o where both i and o are transformable (o is usually a Drawing, or a Drawing paired with some other output). So we can transform a whole widget at once by defining a transformable instance for functions.

instance (Transformable i, Transformable o) => Transformable (i -> o) where
    translate p f = translate p . f . translate (-p)
    rotate r f = rotate r . f . rotate (-r)
    scale sx sy = scale sx sy . f . scale (recip sx) (recip sy)

The way we transform a function is to inversely transform the input, do the function, then transform the output. This is called the conjugate of the transformation.

And that’s it for composable input: just a class for affine transformations. A typical GUI might look like:

-- Takes a mouse position, returns the "pressed" state and its picture.
button :: Behavior Mouse -> Behavior (Bool,Drawing)

And if we want two buttons:

twoButtons = (liftA2.liftA2) (second over) button (translate (1,0) button)

That is, just transform each subGUI as a whole (rather than separating input and output) and combine appropriately. That’s the theory, at least. For this to actualy work correctly, we would need one of the following:

instance Transformable b => Transformable (a,b)
instance Transformable Bool    -- do nothing

Neither of these rubs me the right way. That seems like the wrong instance of transformable (a,b) to me (however, (a,) is a functor, so it’s consistent with what I said earlier). I don’t like having transformable instances for things that don’t actually transform. I’m thinking about maybe a type like this:

newtype WithDrawing a = WithDrawing (a,Drawing)
instance Transformable (WithDrawing a)

(Or the appropriate WithTransformable generalization)

Thoughts?