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 

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.

Project Serpent: Day 1

My work today mainly involved planning out Serpent’s features in more detail. I decided on the screens that would be featured and, on the options screen, what gameplay parameters can be tweaked. In my Day 0 post I referred to these parameters as a “Bastion-style difficulty system”, but from now on I’ll be referring to them as mutators — ways to change the game. A rough outline of what I came up with is available at spec.txt in the git repository.

Once I’d decided on the game rules and the relationships that would exist between various screens of the game, I wrote a small description of them in Idris. (This doesn’t involve any implementation yet, just stating relationships and enumerating the actions available from each screen.) You can see the results of this in Spec.idr in the git repository (the relevant definitions are Phase and Serpent), but this part merits further explanation:

The standard way to do game programming (or anything else that you might think of as having a “main loop”) in a functional language is like this. You define a data type for storing the game state, and instead of a traditional main loop you have a function from game states to game states. (In Haskell-like languages, this might return an IO GameState instead, or it might be a pure function that also takes a representation of the user input state like I used in Pong.) And then you just recursively call this function forever, and that’s the equivalent of a game loop.

The method encouraged by chapter 6 of this Effects tutorial is a refinement of the standard one. Instead of having all game states be the same type, you introduce an additional layer of categorization: a game state that represents the player looking at the main menu might be a different type from one that represents a player in the middle of a game. The reason for this is to encode the notion that some actions only make sense in certain situations: you can only “turn left” if you’re in the middle of actually playing a game and haven’t paused. The Effects library lets us make these kinds of statements known to the compiler.

Here’s the categorization of game states I ended up using, and a brief explanation of my reasoning:

  • First, Playing, which represents actually being in a game. Playing states are further divided into paused and unpaused, which I represent as Playing True and Playing False respectively. In unpaused states, the player can pause or issue commands to the snake; in paused states, the options are unpausing, restarting, or quitting to the main menu. I thought of storing extra information in this category, such as the length of the snake and how many free spaces or pieces of food were on the board, but I decided against it for the moment because the way these things change is heavily influenced by mutators. I might factor these into the categorization if I find a neat way of doing so.
  • Next, the MainMenu. Here, the player can click one of a set number of buttons, such as “new game” or “change mutators”. Since I have a pretty good idea of what the buttons are going to be, this category doesn’t have any internal structure. All game states representing the main menu have the same type.
  • Subsidiary Menus (of which my current design calls for only one, the mutator menu, but there could conceivably also be a sound/graphics options menu) are further sub-categorized by the set of inputs available, where an “input” might be a named toggleable button or numerical slider. The available actions are then to update one of the inputs (the first half of Spec.idr is concerned with describing the different ways to do this) or to exit the menu with or without saving.
  • Finally, the GameOver screen. Like the MainMenu, game-over states are not further categorized: from any game over screen, the available actions are to restart or quit to the main menu.

None of this says anything about what information any kind of game state should contain, or how to apply one of the actions once the player has chosen one to reach another game state — so that’s what I’ll be doing tomorrow.

Project Serpent: Day 0

As phase two of teaching myself the skill of finishing things, I’m going to be working on a well-defined project for a week or two, spending at least a couple hours each day. I plan to begin this project tomorrow, which means I need to get ready today.

So here’s the project: I’m going to be writing a Snake clone (and I’ll call it Serpent, because why not?). By itself, this is probably another Pong-level task that I could do in 48 hours. There are two ways I’d like to make it a bit more interesting:

  • I want to use Idris’s Effects library to write a specification of the game’s rules as a type, which will then be checked by the compiler. I didn’t do this last time because I’d never used Effects before and I didn’t have time to learn it, but I really love the idea of the library and I think it could be a helpful tool for organizing programs!
  • I will incorporate what I like to refer to as a “Bastion-style difficulty system”, which might require some explanation. In the game Bastion, there is a “shrine” at which you can defy various in-game deities, incurring their wrath and making enemies a bit stronger. The effects of this can range from just making enemies hit faster and harder, to making them phase through attacks randomly, to making them explode on death. This is a lot more interesting than the usual “easy/medium/hard” difficulty slider that you find in a lot of games, so I’d like to try something similar.

I’m going to spend today going over some of the lessons I learned from my Pong jam and practice taking advantage of them — I’ll write a simple library for describing the callback structure I was using and try to learn a bit more HTML. Tomorrow, I’ll try to write up a specification and translate it into Idris!