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… 

2 thoughts on “Adding New Dependent Types

    1. Yeah, it’s an exciting application! Part of the reason I’m doing this in Idris rather than Haskell or Elm is to see if dependent types used in this manner can actually be helpful, rather than just aesthetically pleasing, so running into a problem where they should be able to help me is encouraging!


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s