The Problem with Subtle Shades of Mu

This post was provoked by a real event,

unlike many of my posts which are born of pure imagination.

Javascript distinguishes between null and undefined. A cursory Google suggests that null is meant to be used by the programmer to represent an intentional null value and undefined is supposed to be a value that “doesn’t exist”. But this is a pretty vaguely worded distinction, and it lives entirely in the programmer’s mind and culture. The compiler has no idea what the difference between the two use cases is.

I was using a webpage a while ago and noticed that one of their buttons didn’t work. (It was a pretty important button too, rendering the page completely unusable.) On a whim, I decided to open up the Firefox dev tools console and see whether there was some kind of error. Sure enough, TypeError: paymentMethod is undefined showed up in the log, with a handy line number attached. I clicked on the line number and scanned through the code, wondering if the fix would be obvious, and… wait a minute, they’re checking whether paymentMethod is undefined just a few lines above! Control flow should never hit here unless paymentMethod has a value…

Oh wait. The check is paymentMethod !== null. And sure enough, undefined == null evaluates to true, but undefined === null evaluates to false. They checked to make sure paymentMethod wasn’t null, and then acted as if they knew paymentMethod was neither null nor undefined — relying on assumptions that were not provided by the check they made.1

if (x !== null) ... is an insidious mistake, because it looks like within its scope you should be safe. Even an experienced programmer could be forgiven for allowing their eyes to gloss over it, and proceeding to assume that in the following code block x has a value.

Some language features can demand an unreasonable amount of your attention.

A vast maze of choice

Clojure has two falsy values, false and nil. false is a pretty straightforward boolean; nil is a bizarre mashup of falsity, failure, every kind of empty sequence, and Java’s null.

It just so happens that idiomatic Clojure uses a lot of functions that return “either nil or some non-nil value” as pseudo predicates, since you can conditionally branch on any kind of value.

But nil corresponds to null on the Java side, so it generally shouldn’t be used with Clojure’s java interop. I once had to write (if x x false)2 instead of x, because we had a function that called out to Java and therefore wasn’t allowed to return nil. (I’m lucky the function’s docstring said as much, or it could have taken me weeks to figure out what was going wrong.)

And then there’s the fact that a lot of Clojure data is represented by key-value maps. What’s the difference between {:some-property false}, {:some-property nil}, and {}?3 Are they all allowed? Do you prefer one form over the others? You decide!

Or well, you try to decide. But it’s not really your choice: it’s your codebase’s choice. Every time someone checks to see whether a given map has :some-property or not, they’re making an implicit choice as to what those three things mean. And if sometimes people are sloppy, because in the heat of the moment one interpretation was obvious and the others never even came to mind… well, you just have to hope that all of these accidental, unconscious choices happened to match up.

(Even though you know in your heart that they don’t. They never do, for the universe is cruel.)

Whatever shall we do?

If you’ve been reading my blog for very long, you might expect me to now embark on a rant about how Haskell does it better. This is, in fact, what I’m going to do.4

For very simple sources of failure, there’s the Maybe type, which I have probably written a lot about (and if it doesn’t have its own dedicated blog post it will probably get one eventually). Maybe is useful when there’s only one kind of failure possible (or there might as well be only one for all you care), and when you want to respond to that failure just by abandoning the control flow that led to the error. When you’re in this situation, you can use Maybe to introduce a single failure value, guaranteed to be distinct from any of the “success” values, which basically has the behavior of causing control flow to be abandoned whenever something tries to operate on it.

What about when you want to have multiple failure values, with subtle distinctions between them?

Well, first of all, think twice. Dealing with subtly different shades of mu can be a huge headache.

But if you really need to, Haskell has an idiomatic way of easing the headache. First, define an explicit data type enumerating the ways something might have failed: data Error = KeyboardNotFound | SegmentationFault | PEBKAC. Then you use the Either type, which is like Maybe except that instead of one failure value there are many. (In particular, Either errorType introduces as many failure values as there are values of errorType). But while there are many different failure values, there’s a bastion of order and sanity for you to cling to: all of the different ways of failure are guaranteed to have the same effect on control flow (namely, the abortion of control flow). And it is guaranteed to be distinct from the effect of successful values on control flow, which are in turn all the same as each other.

And most importantly, there is a single way to check for this composite notion of failure, and this check is easy to remember and doesn’t hide in a room full of distracting wrong alternatives.

  1. this is one of the more important, nonobvious things a static type system can give you. A really good type checker can, to some degree, infer what assumptions a code block relies on and what properties a dynamic check verifies. If these things don’t match up, as in this javascript case, you can get an error at compile time. ↩
  2. I now realize that this could be replaced by the equally horrible but more compact (or x false). ↩
  3. It gets even worse if you think about lists instead of booleans. false vs nil vs “not present” works out the way you’d expect barring occasional subtle interactions, but [] vs () vs {} vs #{} vs “not present” requires a lot more care — especially since almost all functions that act on collections return seqs5 (like ()) regardless of what the input was, and because nil can be treated to some extent like an empty collection of any built-in collection type. ↩
  4. note, however, that this section glosses over a few things. It is in praise of Haskell’s ideal philosophy, which I do believe is closer to perfection than any language before it, but which Haskell does not unfailingly embody. I’m happy to talk about the various unfortunate departures Haskell makes, but in this section of this blog post a lengthy discussion of such would merely distract from the point. ↩
  5. except, ironically, for seq, which coerces the input collection to a seq unless the input was empty in which case it returns nil. ↩
Advertisement

Static Function Arglist Mismatch

An unsettling amount of my time working at Prismatic has been spent looking for errors whose ultimate cause turns out to be a function statically applied to the wrong number of arguments. By this I mean that you can tell that the function is applied to too many or few arguments just by looking at the function definition and call site, without doing any sophisticated control flow analysis or reasoning about the values of any variable. For example:

(defn foo [x y z] ...)
...
(foo x)

Things aren’t always this easy, of course. If we want to be able to check something like this trivially, there are a few wrinkles:

Declaration site

The function needs to have a static number of arguments at the declaration site — variadic functions are harder to check. If the declaration looks like (defn foo [x y z] ...), the compiler should be able to know exactly how many arguments the function takes. But if it’s like (defn foo [x y z & rest]) instead, knowing whether a given number of arguments is an appropriate input is much harder and probably impossible in general.

Call site

The function also needs to be called with a static number of arguments — which is to say, we need to provide an argument list in the source code rather than using a list variable. (foo 5 6 7) is statically applied to three arguments, so if its declaration statically requires three arguments we know this code is wrong. But something like (apply foo list-of-arguments) applies foo to a dynamic number of arguments, and we have to find out the length of list-of-arguments to know whether the call is correct. This is of course impossible in general.

The entire codebase

This one is probably less of an issue in practice than the other two, but it’s much harder to check for, and I expect that it is the main reason function argument counting is not usually implemented.

Basically, suppose we have something like this:

(defn foo [x y z] ...)
(defn foo [x y] ...)
(foo 5 6)

This is perfectly legal in Clojure and in most other languages, and it means that we can’t just nominate a single declaration form as the definitive place to find foo‘s argument count. And while in this particular case it’s pretty obvious that the function being called has an arity of exactly 2, there are obfuscations we can do to make it less clear whether a function has been redefined between its first definition and any particular call site. So whereas with the other two restrictions you can check whether they apply and turn off the static checking, it is certainly very difficult and maybe impossible to determine whether a definition has been superseded, and that means that static argument counting can disallow valid code.

(defn foo [x y z] ...)
;; something here that redefines foo
;; so that it can take two arguments
(foo 5 6) ;; this is valid!

If the compiler can’t tell that this unspecified code in the middle is redefining foo… it will disallow this code even though it’s technically valid and won’t crash.

So does this mean that in a dynamic language we can’t have the extremely helpful sanity checking of counting a function invocation’s arguments and comparing that to the definition? Actually, no!

The thing that really prevents us from performing this check is the third caveat, simply because it’s difficult to detect whether the caveat is applicable or not. But this caveat doesn’t inescapably apply to all dynamic languages: it’s a side effect of tying the top level namespace to the execution model. If top-level functions were immutable1, there wouldn’t even be the possibility of caveat 3, and we could safely protect programmers from passing the wrong number of arguments.

Of course, if you’re not willing to disallow the redefinition of top-level names, there are still ways to perform the check. They’re not quite as obvious, and I don’t actually know any of them, but I’m certain it’s possible because the SBCL compiler for Common Lisp can very often emit warnings if you call a function with too few arguments.

It would be really nice if languages like Clojure and Python could take a leaf out of SBCL’s book and start doing some straightforward checking of function argument count. It’s not applicable in every case, but where it doesn’t work it can just be disabled with no downside. And over the rest of my life, I calculate that it will save me seven years and seven days of trouble.

  1. technically, if top-level variables were immutable. Clojure functions already are in the sense that once you have a reference to a function it’s set in stone, but if you’re calling a function by name (which is what happens almost all of the time), the referent of that name (and hence the meaning of the function call) can still change. ↩

Failing, Simplicity, and Failing Again

As you might have noticed, Project Serpent has stalled. Between work, the errands of daily life, and other recreational pursuits, I’ve simply spent enough time choosing not to work on Serpent that it has fallen away from the top of my mind.

And that’s not the only thing that has fallen away. Without Serpent updates to post, I’ve had only a few scattered programming-related thoughts, each of which would have taken a lot of effort to turn into a blog post. Ideally I’d put in that effort, but lately I haven’t. And due to the title of this blog, I’ve been reluctant to write posts about the various non-programming things I’ve been thinking about. (I might change the title of the blog in light of this… but it can stay for now.)

So I haven’t been working on my projects, and I haven’t been writing blog posts. I’m not happy with this, and I’m trying to change my behavior.

The first, easiest, and most obvious thing is to write a blog post. That’s simple enough that with a little discipline I can just decide to do it, and it’s done. So here we are. Let’s hope I do this again next Sunday.

Getting back to work is harder. It’ll need discipline too, but pure discipline isn’t enough. I need a plan that compliments my willpower.

The best idea I have now for rekindling my motivation is to go back to something simple. In fact, since my goal is still to return to Project Serpent, I decided I’d go with something even simpler and quicker to build than Pong. I set myself the constraint of making a one-button game that I could feasibly finish in a single day.

Since thinking is a lot easier than programming, I even put some thought into what that game would be like on the train to work. The standard concept for a “one-button game that still manages to be enjoyable” is an obstacle course to jump around, like Canabalt. But I don’t find this model compelling, and I wanted to do something that I hadn’t seen before.

My first few ideas were impractical, either deriving their interestingness from monumental complexity or turning out not to make sense for a one-button game. Eventually I hit on the idea of a rhythm game as the primary mechanic; and that doesn’t fulfill the “something I haven’t seen before” criterion but at least it’s an example of something that isn’t a running game.

And in fact, a slight mutation of this gave me my major breakthrough. It occurred to me that I could throw multiple objects at the player at once by giving each one a kind of “resonant frequency”, and then the player can decide which object to react to at any given time by tapping in resonance with them. Then, the game is about (1) deciding which of a bunch of random enemies to deal with, (2) eyeballing the target frequency of those enemies, and (3) tapping out that frequency to get rid of them.

This felt perfect — it was still based on simple concepts in the spirit of a one-button game, but the idea seemed to open up deep and engaging gameplay, and most importantly I was finding myself motivated to make the game. I wanted to see how it would play. I wanted to play it myself.

So I mentally prepared myself, for the rest of last week, to spend a day on this project. I was excited to finish and see how the idea worked. I thought about showing it to my coworkers at Prismatic (and I’m still planning to be able to do that soon).

I even woke up early on Saturday, and booted up my laptop and text editor and started typing.

Except… I didn’t feel it pulling together. Everything felt so much more effortful than I was used to, code failed to typecheck, and I started to question my model and how it would be used to implement the game I was envisioning. And after a few hours I realized I’d made no progress and decided I couldn’t do it.

That was not this past weekend, but the 10th and 11th.

I have a few ideas for getting started again. My ideas don’t often seem to work… but I remember Pong, and I know I can do this somehow. What can I do but keep trying?

When the Mood Strikes

My mental model for how I should finish Project Serpent is that I shouldn’t bother too much with forcing myself to work on it when I don’t feel like it, because that will just make me miserable. My ultimate goal is to develop the ability to finish projects that I can exercise for the rest of my life, so it’s pretty important that whatever procedure I end up with is not one that tends to make me miserable. So according to this model, I should wait until I am in the mood for programming, and only then should I program.

This actually worked pretty well for about a week after I started working for pay. After that, my programming moods seemed to slow down significantly — I haven’t felt up to programming in a week or two at this point. And so I’ve done no work.

While waiting until I can program without stress would seem to be the ideal strategy if it would get me to my goal… it’s clear at this point that completionism is more difficult than that. If I actually want to finish this, it will take some discipline: I’m going to need to force myself to start working even when I don’t feel like it, at least sometimes.

I would love to instantly become my ideal self, who can be perfectly comfortable at all times and still produce interesting, finished things. But that’s not an option. The only way forward is incremental improvement, and it seems that the most productive incremental improvement is to learn to finish things, even if it hurts.

Type-directed termination

I’ve been distracted from Serpent lately, not just by work but by a fascinating theoretical idea.

The Inspiration

A couple months ago I came across this great paper1 detailing a way to do guardedness checking in a type system.

(A quick detour, because there are going to be a lot of strange words here. “Coprogramming” is a fancy way to talk about programs that are supposed to be infinite loops (like an operating system or game). “Guardedness” is a property of coprograms that can be used to test whether your coprogram is “productive”, which is a particular way for it to be well-behaved. For more information, see previous posts, and if I ever find a nice introductory article I will announce it somewhere.)

Anyway. Type-directed guardedness checks are great because traditional productivity checkers are based on syntactic guardedness, which means (roughly) they just consider the program’s text without thinking about what’s actually happening in the program. This is okay in the sense that it never produces any false positives: if a syntactic guardedness check returns “true” for your program, then your program is definitely “well-behaved” (in the specific sense of productivity). But failing to take into account the program’s semantics means we misclassify a lot of well-behaved things as badly behaved. Usually false negatives can be rescued by rewording them so that the guardedness is obvious to the compiler, but this often produces code that is harder to write and harder to read.

Atkey and McBride’s framework doesn’t directly take program semantics into account, but it does bring productivity checking into the type system, which is almost as good. Basically, each infinite structure has a type that represents “how much of it has already been completed”, and this allows the type system to control how much of the structure you’re allowed to use. Basically, an incompletely constructed infinite sequence has a type that only supports accessing the pieces that have already been definitely placed, but after you’ve constructed it (i.e. outside the definition) it has a type that supports retrieving arbitrary pieces. This ensures that information never depends on Information From The Future, which means your infinite data structure is “productive” or well-behaved.

So that’s why Atkey and McBride’s paper is exciting. What’s this idea of mine that I mentioned in the introduction?

Termination checking

So, it turns out that termination checking (proving that a computation that isn’t supposed to be an infinite loop, well, isn’t an infinite loop) is also traditionally done using syntactic checks. This has the same drawbacks as productivity checking: lots of false negatives, and rewriting the false negatives so that the checker can see they’re well-behaved gives you code that’s a lot uglier and more distracting.

Now it might be obvious from the way we name these things that type theorists consider recursion and corecursion to be closely related. (Precisely, in category theory the relationship is called being “dual” to each other. As I am not an expert category theorist, I won’t go too far into that in this post.) The relationship is pretty simple to verbally define, but its implications are not necessarily easily to grasp: I can’t quite visualize what arrows I need to flip to transform one into the other. But I have the powerful intuition that, if I can figure out how to “flip the arrow” to turn recursion into corecursion, I can use the same “arrow-flipping” procedure on the productivity checking method described in this paper and get…

a method of termination checking. One that’s type-directed rather than relying on dumb syntactic checks.

This is pretty exciting, because when programming in Idris I upset the termination checker a lot more often than the productivity checker. It’s exciting because here is an academic problem that I don’t know the answer to, and it’s been a while since I’ve seen one of those. It’s exciting because as far as I can tell from a cursory Google Scholar search, no one has done this yet.

A part of me would really love to reread this paper a couple more times, until I understand exactly what they’ve done and (hopefully) how they came up with the idea. That part of me would go on to perhaps do some research on the category-theoretic formulation of recursion and corecursion, so that she can visualize the arrow to flip to turn one into the other. That part of me would be ecstatic if it turned out there was a publishable paper somewhere in here, but even if it turns out someone else has already done it, she’d feel that the independent discovery was worth her time, if only as a recreational activity.

Harsh Reality

Perhaps my intuition is mistaken, and there is no straightforward transformation of this productivity checker into a termination checker. But before I even think about that, I need to remember Serpent.

If I really wanted to, I’m sure I could convince myself that abandoning Serpent is the right choice here. And I’m sorely tempted, but… I’m trying to set a precedent for myself. There are important skills that I need but don’t have, and I’m not going to develop those skills by returning to my old ways of abandoning projects every time I come across an idea that excites me.

So as much as I’d love to drop back into type theory, and think about clock variables and flipping arrows… I think it’s pretty important that I finish Serpent first.

  1. Atkey and McBride, Productive Coprogramming with Guarded Corecursion ↩

Adding New Dependent Types

The snake in Serpent now moves around in response to user input, but there are bugs. Specifically, two bugs whose causes I don’t know:

  • When the snake turns from facing-right to facing-up, or from facing-down to facing-left, the head doesn’t quite connect to the tail.
  • Every time the snake turns, its length increases by one.1

That second actually sounds like a fun mutator, but it certainly shouldn’t be enabled by accident, and the first is just ugly. My normal approach to bugs like this is to just stare at the code until I know what’s going on, but that takes a focused amount of time that I don’t have anymore.

Instead, I thought I’d try something that I’ve been waiting to do for a while: making my types for the snake more expressive. In particular, there are two invariants I’d like to express, which will neatly cover the two bugs I’m having:

  • Extending a snake moves its head by one space in the appropriate direction. Retracting a snake leaves its head in the same place. This will ensure that the head never jumps discontinuously.
  • Extending a snake produces a snake whose length is increased by one, and retracting a snake produces a snake whose length is decreased by one. Since normal motion is a result of extending and then contracting a snake, this will ensure that motion preserves length (unless the snake is supposed to grow).

To track these two invariants, I need a snake type indexed by length and head position — you can see this in the Typed namespace of GameState.idr. This allows me to state in the types of Typed.extend and Typed.retract how the length and head position change (or don’t). I’ve also added a function to convert a typed snake back to the “list of segments” representation, because for some things (such as drawing the snake) the extra type information isn’t needed.

I haven’t yet integrated this typed version of the snake representation into the game code — that will take a bit more work, including indexing Playing phases by snake length (which I’ve been meaning to do for a while) and then just updating all the code to use the new functions (which shouldn’t be very hard, because the new functions have the same names as the old ones). After that, if my code still compiles and the bugs haven’t disappeared, I’ll have ruled out every possible location for them except the drawing code.

  1. Actually, in the course of writing this blog post I realized one of the causes of this and fixed it. There’s still something wrong though… ↩

Project Serpent, Day I-lost-track

On day 8 (which I believe was Sunday), I announced that I was happy with the progress I was making, and that I was confident enough in my ability to finish that I would treat the end of this next week as a deadline.

And then the next day I went to work, and realized that perhaps my pronouncement was premature.

It turns out it’s really hard to work on anything after coming home from a full day of work. Luckily, I still find it pretty easy to get some work done on Serpent before I leave in the morning, but even so that’s much less time than the four hours I told myself I’d spend. I’m no longer sure I can finish by the end of this week, and even writing up daily progress reports is kind of hard. Some concessions are due.

I will not give up on Serpent, but I’ll make the following modifications to my challenge:

  1. I will work on Serpent for a minimum of 30 minutes each day.
  2. My deadline (which is once again a soft deadline, like the one I set for the first week and unlike the one I meant to set for this week) is December 30.
  3. I will no longer require myself to post progress updates every day, though I’ll still try to do it every couple of days and I will still require myself to stick to my pre-Serpent schedule of one post per week.

Now that the unpleasant concession is out of the way, here is an actual progress update.

This morning I wrote up an abstract effect and handler for operations depending on user keyboard input. This is the next step of my “make everything interactive, thereby increasing my motivation” project: I have a snake that moves around at reasonable speeds, but right now it just plods inexorably toward the right edge of the screen until finally it crosses the threshold, never to be seen again. I don’t even get to see whether I’ve correctly handled cases of the game state evolution and drawing functions for when the snake does not consist of a single segment.

Over the next couple days (hopefully by the end of this week), I’m not going to work on actual collision with walls and eating food, but I hope to have the snake respond to the arrow keys by turning around!

C is declarative, kind of

Inconsequential musing of the day:

If you look at say, a Python file — or Bash or Ruby or almost any other scripting language — you can’t find any information1 about the names defined in a program without actually running the script. This is because in Python, the only way to associate a name with a value is to execute a line of code that causes it to get some value (maybe an assignment statement, maybe a function definition, maybe an eval that contains one of these things). The association of top-level names to values is inherently a procedural process, defined only by the language’s execution model.

Contrast this with the situation in C. C has actual declarations, which associate certain information to a name completely independently of the execution model, and in fact the execution model usually doesn’t2 cause values to become associated with top-level names at all. C’s top-level namespace is specified declaratively: it states directly which names are associated with which values.

Does this matter? In practice, probably not much. In theory, a declarative program layout should be easier to manipulate through automated tooling (for example, to list out the documentation for all of the top-level names defined in a module/file without running any of its code). But most reasonable Python programs are pretty declarative at the top level anyway: you rarely see things like

# webserver.py
turing_machines = [...]

if does_it_halt(turing_machines[0]):
    def post(blah, bleh):
        blee
if does_it_halt(turing_machines[2]):
    def get(bloo):
        bluh

globals()[running_time(turing_machines[1])].__doc__ =
  ''.join(accepted_language(turing_machines[1]))

On the other hand, languages like C do make it a lot easier to catch typos, which I consider to be an appreciable benefit. Not that typos are a particularly difficult to track down class of bug.

But mostly I just found it interesting to think about how C’s model is, in a way, more declarative than lots of more modern languages.

  1. In general. Of course most specific scripts aren’t quite so horrible. ↩
  2. I think there are a couple exceptions to this having to do with extern and/or static top level variables and perhaps also function pointers (can those be defined at the top level?). But the top level of a basic C program consists entirely of function declarations and no assignment. ↩

Project Serpent: Day 8

Somehow Day 7’s post got lost amid my move and starting my first day of work1. My accomplishments for that day are probably smooshed into the post for Days 5 and 6, but I haven’t been paying close enough attention.

Needless to say, I’ve decided to extend my deadline to a second week. This isn’t really a problem, because the point was never to finish something fast, it was just to stick with it until it got finished at all. I think I’m pretty well on track for this (but I do think that this next deadline is going to be stricter: I can’t just pat myself on the back and be content that I’m making progress, so I want to be careful not to let this drag on longer than it needs to).

Anyway, a brief recap. At the end of days 5 and 6 (and maybe 7, I guess?), I had implemented my NONBLOCKING effect and its yield command, which allowed me to write much more natural-looking code. I felt very satisfied with my work, and proud for thinking of it and fighting my way through the type errors until it actually worked the way I wanted it to.

And then I called it a day, because it was late, but that meant that I ended that day of development without actually using my triumph to write a natural event loop to evolve and draw the game.

So on Day 8, I spent my time doing that. First, since I was now writing my entire game loop within the Effects DSL, I needed to write an effect that provides drawing commands rather than just using IO actions. I did this.

But I soon discovered that whenever I used these drawing commands, they would grind my game loop to a halt: I had previously put in a console.log every time my yield code fired, and whenever I used my drawing effect I’d get exactly one line of output from it. I worried that perhaps my yield effect wasn’t as composable as I had thought, that my entire architecture was flawed and that if I’d just thought about it more rigorously before spending a day implementing it I would have realized that it couldn’t possibly work, that it was too good to be true.

Actually it turned out to be an embarrassing example of the kind of mistake that doesn’t get caught by a type system. Interpreters for Effects programs are defined in continuations, and the thing that makes this powerful is that you can define when, how, and how many times the continuation is called. For instance, you can call the continuation under a lambda abstraction and pass it values that don’t actually exist. You can call the continuation many times and build up a list of the results.

Or you can call the continuation zero times, simulating a nonlocal exit. The code following a command that doesn’t call its continuation… doesn’t get executed.

Needless to say, this is exactly what I did.

Despite all those problems, I soon ended up with a simple program that just makes the snake run off the edge of the screen. But the program was written entirely in my little Effects DSL, and looks very natural, and I’m confident that it will be easy to write many different variations when it comes time to add more features.

Day 8 was well spent.

  1. I am so excited about this. So much that trying to find the words would distract me unacceptably from Project Serpent, so unfortunately I won’t. ↩

Project Serpent: Days 5 and 6

I didn’t have time to write a blog post yesterday, because I was moving to San Francisco1. I was still doing work though, and today I’ll write a catch up post (in addition to my day 7 post later).

Yesterday (was that the earliest day I haven’t written about? I think so) an enticing thought occurred to me, about how to integrate my [GAME phase, 'GameClock ::: FPS 5] effectful programs into the Javascript model of “compute only in small chunks, so as not to monopolize control of the browser”. The idea was simple and glorious: just write an Effect that provides a “yield” command, and have the handler for that command register the continuation as a JS callback rather than applying it directly!

I spent most of the day thinking about various aspects of this — what type it would need to have and the finer details of how it would work. When I finally got off the plane and arrived at my new home for the next few months, I sat down and started writing some code, and things became much clearer.

Except… they also became a bit less clear in other ways. I don’t recall all the specifics now, but as my ideas started taking shape in the code I was engulfed in a hail of bewildering errors that came about from the specific way that Idris’s Effects library works rather than anything about the semantics of my code. Rather than deal with them late at night, I finally decided to just go to bed and figure out how to massage Idris into accepting my definitions tomorrow.

Likewise, yesterday was mostly spent scrutinizing strange type and inference errors and trying to figure out what I could tell the compiler to make it understand why my code is acceptable. This process was a bit frustrating and took a few long hours, but finally at the end of it all I had shut down the worst of these errors for good, and was able to write this simple program that ticks the gamestate at the correct rate by always sending the snake forward:

dummyGame : { [GAME (Playing False rules), 'GameClock ::: FPS 5, NONBLOCKING] } Eff ()
dummyGame = do
  delta <- yield
  newFrame <- 'GameClock :- tick delta
  if newFrame
     then do collision <- turn Straight
             if collision then playAgain startState else value ()
     else value ()

This piece of code does everything correctly — respecting the frame rate and returning control to the browser after every frame — without having to manually break up the control flow at all. I’m pretty happy with how it turned out!

I still don’t have a way of drawing the game state yet, but that can be solved pretty simply: all I need to do is write an effect that provides drawing commands! I’ll be working on that later today.

  1. actually Berkeley, but I am enough a stranger to the area that I consider them the same. ↩