Tequila!

Here are some recordings from my birthday session and a recent session. Both feature Devon DeJohn on the guitar. The 8/16 session was sans Evan, who was busy with his anniversary.

• 2008-07-17 01
• 2008-07-17 02
• 2008-08-16 01 - Tequila!
• 2008-08-16 02
• 2008-08-16 03

All these tracks are good. Well, the last one is good in its own way… Enjoy!

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 x₁ ⊇ x₂ ⊇ …, ∩_i f[x_i] = f[∩_i x_i]

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 x₁ ⊑ x₂ ⊑ …, sup_i f(x_i) = f(sup_i x_i).

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:

import Control.Arrow (first)

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?

The Deserted City

SNW had a session last Sunday, featuring Nolan McFadden on guitar. Here are some select tracks.

• 01 - A long, laid-back jam, featuring Nolan rapping Jabberwocky at the end (here is a clip of just the rap)
• 02 - energetic
• 03 - The Deal
• 04 - As Long as You Let Me Have Some
• 05 - The Stampin’ Gran’ Express
• 06
• 07 - The Compassionate Track (by Nolan)
• 08 - The Deserted City with an improv story by me! :-)

My favorite is no. 8, and it still would be even without the story. Nos. 2, 3, 4, and 5 are quite excellent as well. It was a good session.

Upon reflection though, I notice a lack of melodic content in these. These songs have many interesting and solid textures, good solos, but not really any primary melody. I guess that’s something to focus on for next time.

Semantic Design

Here’s a post I’ve been wanting to write for a while. This is an exposition of a unique, powerful, and (retrospectively) obvious software design approach. I owe the whole of the Haskell language for helping me toward this philosophy, but it is much broader in scope than Haskell. In particular I owe Conal Elliott for being explicit about it with the Anygma team earlier this month: spelling out a reason I see beauty in Haskell and in FRP, and laying out a technique for designing systems with that sort of beauty.

This is not an alternative to eg. waterfall or agile. I see it as orthogonal to those, and more technical. I’d say it’s an alternative to Design Patterns. However, I ask readers to approach it as something new to be incorporated rather than a replacement or attack on Design Patterns.

I’ll just start with the big idea: make the types and objects in your program mean something. Usually there is some rhyme and reason for creating classes the way we do—eg. list is not just a convenient grouping of procedures, it conceptually represents a list. Semantic Design takes that to the extreme. We first decide exactly what a list is, and then we make sure that every operation we expose is consistent with that idea.

To demonstrate, I’ll use the example that Conal used when he presented this to us (in seminar form): images. Here’s an exercise for you: define “image” precisely. What is the essence of an image? I’m talking about the concept itself, not the way you would represent it in memory (but if you actually think of the concept of an image as a 2D array of pixels, that’s valid).

Here is a small selection of the examples we came up with in the “seminar”:

1. A rectangular array of colors (for a suitable definition of color);
2. A function taking a pair of real numbers and returning a possibly transparent color;
3. A list of colored geometric primitives (polygons, lines, circles), where objects later in the list are shown on top of objects earlier;
4. Any object with a draw method (our formalization of this very software-oriented concept was a function from screens to screens)

Hopefully these examples hinted at the idea that these are conceptual or mathematical definitions, not software ones. The only reason I say “mathematical” is because I view math mostly as a tool for talking with precision; I don’t see defining your concepts in terms of classic real numbers, vector spaces, functions as necessary, just convenient.

A bit of jargon: one of these concepts is called a semantic domain (of Image). The semantic domain is the conceptual analog to the software abstraction we’re creating.

With each of these semantic domains, we can start to imagine what kinds of operations we’d like to do with them. In considering these operations, another big idea enters the picture: The semantic domain should be composable. This is the hardest one of the axioms for me to explain the meaning of. Roughly it means we should be able to build more complex objects from simpler ones. This gives us an exponential increase in the expressibility of our system, so we don’t have to implement much to get a lot of power.

A straightforward composition operation on images is to put one on top of another. Imagine what that would look like for each of the semantic domains:

1. The resulting image at coordinate (x,y) is an appropriate blend of the bottom image at (x,y) and the top image at (x,y).
2. Same as above, except x and y are real numbers.
3. The resulting image is the bottom image concatenated with the top image.
4. The resulting image’s draw() method is { bottom.draw(); top.draw(); }.

We would also like translation, because that together with composition gives us a fair amount of power (we can now composite images together in any layout). Here are definition sketches for translation in each of the semantic domains (where (tx,ty) is the amount we wish to translate):

1. The pixel at (x,y) in the resulting image is a blend of the pixels around (x-tx,y-ty) (if we can translate by non-integral amounts) if it is in the array’s range. If not, it’s transparent.
2. The resulting image at coordinate (x,y) is the original at coordinate (x+tx, y+ty).
3. Translate each of the primitives in the list by (tx,ty).
4. Unclear how to define translation in this domain!

Let’s stop analyzing operations for now. Usually I just do this quickly in my head, nothing formal (which is why I didn’t write it in formal mathematical language). But it seems like we have eliminated model no. 4 just by looking at the operations we want. Translation doesn’t mean anything when an image is defined by its draw method. This is an interesting development, since it would typically not be considered bad style to start writing an image library thusly:

abstract class Image {
    public void Draw();
}

(Or an interface—six of one, half dozen of the other)

To carry on with no. 4, we would have to expand our semantic domain. Maybe no. 4 would become “any object with a draw method and a translate method”. But this is obviously getting out of hand without getting us anywhere semantically. Why is it important to get somewhere semantically? This gets us to our last axiom: The semantic domain should be as simple as possible.

The motivation for this should be obvious. The simpler the semantic domain, the easier it is to reason about the implementation, both from the outside and from the inside. From the outside (the user of a library, for example), you can predict the behavior of everything you’re doing since the semantic domain is easy to understand, and we coded our library to correspond exactly to the domain. From the inside, it is easy to verify that our implementations match the semantic definitions, since they are simple. I felt like I went around in a circle in that paragraph, but I hope this is obvious.

This metric excludes no. 4 from our list of candidates, since the semantic domain gets more and more complicated with each new operation we want. Further, I argue it excludes no. 1. I used the informality “appropriate blend”, and while practitioners will know what I mean, the fact that it was too inconvenient to specify exactly is a red flag. On the other hand, nos. 2 and 3 both a simple exact specification.

Investigating operations further, it becomes clear that no. 2 is simpler than no. 3. Scaling a function by (sx,sy) is simple: (x,y) → (x/sx,y/sy), whereas scaling a primitive needs a switch on the primitive type, and consideration of its position and size. In most cases we could have intuited this just by looking at the domains themselves and not the operations, since the domain of no. 2 is simpler. No. 3 has to talk about primitives, and a precise definition would have to list the properties of each primitive, whereas no. 2 is just a function.

I’m not saying no. 2 is the best, this is just the kind of reasoning we do in Semantic Design. There could be a better domain for images, but I think no. 2 is the best of these four. We must be creative in coming up with these, and we must take care that they are expressive enough for our requirements.

Once a semantic domain is settled on, we can implement. The implementation’s representation may be very similar to the semantic domain, or it may be very different. Sometimes we have to play all sorts of tricks to get an efficient implementation. But the point is that whatever representation we choose, and however we implement the operations on it, those operations must all have precise, meaningful definitions in the semantic domain. For example, if we choose no. 2, then it is meaningless to talk about an operation that returns the number of pixels in the image, because our domain has no idea what a pixel is. That doesn’t stop our representation from being a rectangular array (but other things, like supporting accurate arbitrary zooming, do).

But it is reasonable not to expose the full power of the semantic domain through the code interface. You can imagine that if this image library is for drawing on hardware using OpenGL, then supporting an arbitrary function from reals to colors may be a speed nightmare, so we just won’t expose that. The operations we expose simply need be a subset of the operations expressible on the domain.

In summary, my interpretation is: Semantic Design is about creating abstractions that don’t leak. It gives me confidence that the approach can be taken to the very extreme, where you model your semantic domain in a proof checker and prove that your code matches it. In typical software design we cannot begin to prove code is correct, because we haven’t any idea what “correct” means! If the abstractions leak, then your implementation has a bug—a place where it does not correspond to the semantic domain. Thus, when done correctly, a semantically designed abstraction cannot leak.

There’s still plenty to say on the subject, but this post is already too long. This was an informal introduction, and most of this stuff can be formalized for the more mathematically-minded. In addition, there is another beautiful closely related concept (also due to Conal) called “typeclass morphisms”, which at the moment have a very Haskell-centric interpretation. But I think I’m close to a more general meaning for those (probably will end up being something from category theory).

Remember the principles: objects and types mean something, the semantic domain should be composable, and the semantic domain (and operations) should be as simple as possible.

Free Improvisation

The Anygma office had a MIDI keyboard lying around. Today I was hanging around at the office, and in my boredom I decided to look for the parts necessary to hook it up. A half hour later, I had a piano set up!

I haven’t played for two weeks, so this is a little rusty, but it’s okay. A 25 minute free improvisation. I also extracted the middle section which I thought was the strongest in case 25 minutes is too much. I’m actually quite fond of the latter.

Oh yeah, this was an interesting exercise, too, since this keyboard doesn’t have a sustain pedal.

The Curry-Howard isomorphism and the duality of → and ×

To people who are familiar with the Curry-Howard isomorphism, this post will probably be trivial and obvious. However, it just clicked for me, so I’m going to write about it. I had passively heard on #haskell that → and × (functions and tuples) were dual, so I played with types a bit, finding dual types, and it never really came together.

I’m not actually sure what I’m talking about here is exactly the CH isomorphism. I’ve been thinking about dependent types, and converting propositional formulae into that calculus. But if it’s not, it’s close.

Let’s use some sort of type bounded quantification in our logic. I was thinking about the following formula:

The corresponding type is:

In other words, the proposition “for every natural, there is a twin prime greater than it” corresponds to the type “a function which takes a natural and returns a twin prime greater than it”. × corresponds to existentials, because it is the proof: it tells you which thing exists. The first element of the tuple is the thing, the second element is the proof that it has the desired property.

It’s interesting that ∀ corresponds to →, since logical implication also corresponds to →. The difference is that the former is a dependent arrow, the latter is an independent one. Beautifully in the same way ∃ corresponds to ×, and so does ∧.

Oh right, the duality. Knowing this, let’s take the above type and negate it to find its dual.

i didn’t bother expanding the encoding of not on the inner levels, because it doesn’t really make anything clearer.

The dual is a pair: a number n and a function which takes any number and returns one of three things: a proof that it is no greater than n, a proof that it is not prime, or a proof that the number two greater than it is not prime. Intuitively, n is a number above which there are no twin primes. If this pair exists, the twin prime conjecture is indeed false.

So yeah, that’s how → and × are dual. It’s pretty obvious now, actually, but it took a while to make sense.