I’m working on a Gamebook unroller in Haskell currently, and one of the things that entails is generating a world with a finite number of states. The state type itself need not actually be bounded, it’s fine if there’s a Set, Integer or a Map if the gamebook only allows a subset of those to ever be generated.

One thing I ended up doing a few times was I had a number representing something like how many potions you’ve drank or how much a character likes you, and I saturated the arithmetic just in case there’d be a cycle. And in fact from a gameplay standpoint this works quite well, having the person react to recent actions shifting themselves between 0 and 5, is more fun than allowing you to cycle to a hatred of -20 and not being able to get out.

At first I wrote a helper to saturate an operation on the Integer type, but then I realized that you have to track the correct maximum values in the calls. All across the game you’d end up with something like¹:

let
  _ = roomAction $ saturatingIncrement state 4
  _ = roomAction $ saturatingIncrement state 4
  _ = roomAction $ saturatingIncrement state 5

Which is ugly and very error-prone. So I realized that there’s a library which creates vectors that have type-level bounds. So a Vec 3 Int always has a length of 3 and is a different type from Vec 4 Int. And the way this is done is actually not that difficult.

DataKinds🔗

In GHC (the main Haskell implementation) you have many extensions, one of which is called DataKinds. I’ve spoken about it in length in a Lang Talk.

Taking it slightly further, you can also retreive the value of a type-level natural number via the use of natVal:

natVal (Proxy :: Proxy 5) == 5

vecLength :: forall len. (KnownNat len) => Vec len -> Int
vecLength = natVal (Proxy :: Proxy len)

Ignoring the machinery behind it, this is actually a very nice interface. So it’s easy to make a type like this:

newtype SatNat (max :: Natural) = SatNat {unSat :: Natural}

With a Num instance implementing saturating versions of addition, subtraction, etc.

And the gamebook can use it:

data GameState = S
  { martinHappiness :: SatNat 5
  , knowledgeGained :: SatNat 10
  -- etc.
  }

The questions remains… did I write them correctly?

Liquid Haskell🔗

“Liquid” stands for “Logically Qualified”, it’s a good pun, though slightly confusing name. It brings dependent types of sorts into the world of Haskell.

The sad part is I have not found a way to actually make LH interact with datakinds. So our elegant solution as far as I know can’t be used and we have to opt for the value level… which I don’t love… but it’ll be verified anyways so let’s give it a go.

Let’s start with the data definition (top since max is taken):

data SatNat = SatNat
{ top :: Integer
, value :: Integer
}

Now for the liquid type:

{-@
data SatNat = SatNat
  { top :: Integer
  , value :: {value:Integer | (value <= top) && (value >= 0)}
  }
@-}

Now already, if we jot down placeholders for the functions of Num we get some helpful advice:

fromInteger v = SatNat 0 v

**** LIQUID: UNSAFE ************************************************************
app/Gamebook/LHUtils.hs:19:28: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Num.Integer.Integer | v == v##a22Y}
    .
    is not a subtype of the required type
      VV : {VV##1597 : GHC.Num.Integer.Integer | VV##1597 <= (0 : int)}
    .
    in the context
      v##a22Y : GHC.Num.Integer.Integer
    Constraint id 29
   |
19 |   fromInteger v = SatNat 0 v
  |                            ^

I’ve heard somewhere that Liquid types aren’t exactly easy to read, but in this case it should be apparent, our type of v is not constrained by the <= 0, which makes sense, if I pass in anything other than zero we violate our property.

And in fact, I wanted to just do this:

fromInteger v = SatNat v v

But I got a failure since v might be smaller than zero. I didn’t even think of that because I was still thinking in Naturals.

Addition and subtraction are pretty straightforward, it’d be fine to not even include any liquid type at all, however one could then try to add two differently bounded SatNats so we constrain them to be the same:

{-@ satNatAdd :: x:SatNat -> {y:SatNat | top x == top y} -> {z:SatNat | top y == top z } @-}
satNatAdd x y =
  SatNat
    (top x)
    (min (value x + value y) (top x))

{-@ satNatSub :: x:SatNat -> {y:SatNat | top x == top y} -> {z:SatNat | top y == top z } @-}
satNatSub x y =
  SatNat
    (top x)
    (max (value x - value y) 0)

If I accidentally use 1 instead of 0 somewhere, or swap the + and - I get notified by LH, awesome.

You might notice that I’m misusing the Integer type here to first do unbounded arithmetic and then decide what to do based on that, this is kinda ugly and we can do better.

Ada SPARK🔗

SPARK is a formally verifiable subset of the legendary Ada language. It allows us to verify both that the code can produce no runtime errors as well as its behaviour.

It already includes a range type with arbitrary lower and upper bounds (accessed with 'First and 'Last) so the datatype is taken care of. Now for the saturating math:

generic
   type T is range <>;
package SatNat with SPARK_Mode => On is

   function Saturating_Subtract (X, Y : T) return T
     is (if Y > X then T'First else X - Y);

   function Saturating_Add (X, Y : T) return T
     is (if (X <= T'Last - Y) then X + Y else T'Last);

end SatNat;  

This is a generic package over some range type T, which contains two functions and has SPARK verification turned on.

We can instantiate it with any range type:

type Happiness is range 0 .. 5;

package Happiness_Arithmetic is new SatNat (Happiness);

-- ...

Happiness_Arithmetic.Saturating_Add (2, 3);

The nice thing is that SPARK will be verifying that the arithmetic doesn’t (over/under)flow outside the given range, so we are forced to do this properly. In fact the gnatprove tool already has plenty of idioms it’ll give you in reaction to an unverifiable operation.

If we just write this naively:

function Saturating_Add (X, Y : T) return T
  is (X + Y);

#+begin_example

Ada SPARK🔗

SPARK is a formally verifiable subset of the legendary Ada language. It allows us to verify both that the code can produce no runtime errors as well as its behaviour.

It already includes a range type with arbitrary lower and upper bounds (accessed with 'First and 'Last) so the datatype is taken care of. Now for the saturating math:

generic
   type T is range <>;
package SatNat with SPARK_Mode => On is

   function Saturating_Subtract (X, Y : T) return T
     is (if Y > X then T'First else X - Y);

   function Saturating_Add (X, Y : T) return T
     is (if (X <= T'Last - Y) then X + Y else T'Last);

end SatNat;  

This is a generic package over some range type T, which contains two functions and has SPARK verification turned on.

We can instantiate it with any range type:

type Happiness is range 0 .. 5;

package Happiness_Arithmetic is new SatNat (Happiness);

-- ...

Happiness_Arithmetic.Saturating_Add (2, 3);

The nice thing is that SPARK will be verifying that the arithmetic doesn’t (over/under)flow outside the given range, so we are forced to do this properly. In fact the gnatprove tool already has plenty of idioms it’ll give you in reaction to an unverifiable operation.

If we just write this naively:

function Saturating_Add (X, Y : T) return T
  is (X + Y);

gnatprove provides us with this message:

satnat.ads:6:10: medium: range check might fail, cannot prove upper bound for X + Y, in instantiation at adalearn.adb:21
    6 |   is (X + Y);
      |       ~~^~~
  reason for check: returned value must fit in the result type of the function
  possible fix: add precondition (X <= Lim'Last - Y) to subprogram at line 5, instance at adalearn.adb:21
    5 |   function Saturating_Subtract (X, Y : T) return T
      |            ^ here

Eat your heart out Rustaceans, this is an amazing message, since we want to work with that precondition just check it in code not in a contract. This leads us absolutely trivially to the former code.

Even if you try to write it yourself and mess up, SPARK will notify you of your mistake:

satnat.ads:13:36: high: range check might fail, cannot prove upper bound for X + Y, in instantiation at adalearn.adb:21
   13 |   is (if (X <= T'Last + Y) then X + Y else T'Last)
      |                                 ~~^~~
  e.g. when X = 5
        and Y = 1
  reason for check: result of addition must fit in the type of the qualification
  possible fix: add precondition (X <= Lim'Last - Y) to subprogram at line 12, instance at adalearn.adb:21
   12 |   function Saturating_Add (X, Y : T) return T
      |            ^ here

Remember the Integer workaround? It arguably created more “apparently correct” code than this, but we can have our cake and eat it too. SPARK can have let’s say “unbounded arithmetic” in its contracts that describe the behaviour, and the original code then gets verified:

generic
   type T is range <>;
package SatNat with SPARK_Mode => On is

   function Saturating_Subtract (X, Y : T) return T
     is (if Y > X then T'First else X - Y)
     with
       Post =>
         (Saturating_Subtract'Result
          = (if X - Y < T'First then T'First else X - Y));

   function Saturating_Add (X, Y : T) return T
     is (if (X <= T'Last - Y) then X + Y else T'Last)
     with
       Post =>
         (Saturating_Add'Result
          = (if (X + Y) < T'Last then X + Y else T'Last));

end SatNat;  

So we can describe the behaviour of: “If the sum is smaller than the upper bound then the result is the sum otherwise it is the upper bound.”. Directly in code, yet the implementation is more efficient in its execution.

This is one of the most trivial cases for this technology yet I’m still blown away.

C++26 Contracts🔗

C++26 adds support for contracts as well, so I figured I’d play around with them to try to get this same behaviour. And I found out that checking them at compile-time without constevaling is not ready… shame, looking forward to it.

Footnotes🔗

¹ Actually nothing like this since I love Lenses