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… 
Advertisements

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!

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. 

Project Serpent: Day 4

Halfway through my first week, and it looks like unless things pick up I’m going to be taking a second. That’s fine though, just as long as I keep working.

Right now I have a very preliminary “step game” function that allows the snake to move around, maintaining its length, but doesn’t do any collision detection (including whether it has eaten any food). The obvious thing to do here would be to detect collisions and remove food (code is already in place to grow the snake if the collision detection signals that food has been eaten), but instead I’ve decided to take a little break to switch to working on the front end.

What have I been doing on the front end? Well, as in everything, there are degrees to this, and I’ve only been working on the “middle” front end so far — actual rendering and user input aren’t coming yet, but I’m one abstraction level closer to that. I am writing code that is “aware” that user input and frame rates exist and must be taken into account.

I’ve been handling this as follows. There are a few rough “parts” to the Effects library: the specification itself (defined in Spec.idr), the “resources” that are required to back those effects (which I define in GameState.idr), and “effectful programs” that make use of the operations defined in the specification to manipulate the resources. The great thing about effectful programs is that they can have a list of effects available, and can use operations from any of them. So for example, I’m writing programs right now with access to [GAME (Playing False rules), FPS 5]: I can manipulate a game that’s unpaused, and… hey, this FPS thing is new!

FPS is an effect I wrote yesterday night when I realized that if I’m writing code that will run on every browser frame, I shouldn’t necessarily have that code run a simulation tick every time. The coordinates I’m planning to use in Serpent are relatively low resolution, and moving forward by an entire “square” every frame would be way too much. So the FPS effect manages a little counter that can be queried to say “Hey, this much time has passed since I last talked to you. Should I run another simulation tick yet?”. Currently I have it set up to run 5 ticks per second, but that can be easily adjusted later.

Of course, 5 ticks per second is fine for the game clock, but a UI that runs at 5 FPS is going to be annoying. I plan to solve this using tagged effects: [FPS 5] represents the ability to respect a clock that runs at 5 ticks per second, but ['GameClock ::: FPS 5, 'UIClock ::: FPS 60] represents the ability to respect both a game clock that runs at 5 frames and a UI clock that runs at 60 frames per second. This is similar to how many RTS games run on a coarse-grained clock used for the simulation and a finer-grained clock so that nice animations can be shown between the game’s relatively abrupt state transitions.

And finally, right now I’m just writing a function from user inputs to effectful programs with access to [GAME (Playing False rules), 'GameClock ::: FPS 5, 'UIClock ::: FPS 60], but I plan to soon write an effect representing input as well. After that, I hope to be able to write code like this:

if !('GameClock :- tick delta)
  then turn !getDirectionCommand
  else pure False
if !('UIClock :- tick delta)
  then {- draw a new frame somehow -}
  else pure False

Of course, I’m not quite there yet. But I think I should be by the end of today!

Project Serpent: Day 3

Yesterday I spent some time improving my MenuInput data type. I realized I haven’t mentioned that at all in this series of posts, so I’ll talk about it a little.

A MenuInput basically describes an editable entry in an options menu. Simple menu inputs might be things like NatBox "Number of heads" 3. This represents an input box that can contain a natural number, labeled “Number of heads”, and whose default value is 3. Similarly, FloatBox "Game speed" 1 is a box called “Game speed” that contains a floating point number defaulting to 1. There are also selection boxes, like Options "Hair color" ["blue", "green", "red"] "green", which means that there are three choices for hair color defaulting to green. And finally, there are toggle options with additional configuration available if they’re toggled “on”: Toggle "Gravity" [FloatBox "Strength" 9.8, Options "Direction" ["up", "down", "left", "right"] "down"] means that gravity can be either on or off, and if it’s on you can also configure its strength and select one of the four cardinal directions for it.

Every kind of menu input has a type of values that it accepts. A NatBox accepts natural numbers, a FloatBox accepts floating point numbers, an Option accepts one of the available strings from the list of choices1, and a Toggle can either be “off” or it can be “on” with a list of values for the extra configuration options. Because Idris is a dependently typed language, we can actually encode this statement as a function from MenuInputs to Types, and that’s exactly what valueFor does in Spec.idr.

So part of my time yesterday was spent writing additional utilities for working with lists of menu inputs and the values they can take. For example, I have a function to apply an update2 to a particular entry in a menu, or to get the value of a certain entry.

Anyway, that is one system I have developed that I hope to get a lot of use out of when I get to programming the menus. So far, I’m not there yet, but I’m getting there: the other thing I spent time on yesterday was my skeleton implementation of the game state, with a focus on states in the “in-game” phase. Right now I’m working on what you might call the meat of the game: stepping a game state by moving the snake, doing collision detection, and possibly growing it or ending the game.

Today I’ll finish writing functions for stepping the game state, and hopefully by tomorrow I’ll be ready to start hooking those functions up to some kind of UI!


  1. we represent these in Idris as strings paired with proofs that they’re in the list of available options. 
  2. I also have a function mapping MenuInputs to the kinds of updates you can perform on them: for example, a Toggle can be toggled and a NatBox can be incremented or decremented, and any input can be set to an exact value. See updateFor in Spec.idr for details. 

Project Serpent: Day 2

Yesterday I only barely got my four hours in — a reminder, I suppose, that even in the wake of my accomplishment, finishing larger projects will still be difficult for me. I’ll have to be more careful about starting to work a bit earlier in the day.

Once I did get started working, I think I got a reasonable amount done. I started by defining a type for the concrete game state (parameterized by the “phase” category I talked about yesterday), which should store everything that’s necessary to represent and evolve the game. After that I wrote a skeleton implementation of a handler for every command I defined in Spec.idr. But while working on this, I realized that my types were looser than they needed to be.

I took a break to think about this and ended up storing in all Phases the set of active mutators and their parameters. For now, this mostly lets me specify the menus more tightly: the Reset command, for example, now states in the type that it resets all mutators to their default states, and the SaveMenu command states that it does some validation checking and then either stays at the menu without changing anything or returns to the main menu with the new parameters in effect. All the other commands also state that they don’t change the set of active mutators.

Making the mutator state available to this set of rules also opens the way for a much more dramatic change later: I’ll be able to add to the Playing phase parameters like the snake’s length and score, so that rules about how the snake grows can be encoded in types too!

Of course, with all this type fun, I’ve still done little work on the game’s implementation. I’ll have to pick up the pace soon.