Skip to content

Exact usage and branching

This thread from @dorchard inspired me to re-use the exact-usage hack of Idris2 to see if I could implement this particular feature of Granule.

By the way, granule is a great project full of great ideas and I strongly encourage you to take a look! Try downloading the examples and play with them, the project comes with a very nice tutorial.

To make this work in Idris, we're going to use the same Copies data structure than in 01. Emulating exact-usage in Idris2. More precisely, we need to make 1 copy of the value def if the value is missing and 0 if the value is present (since we're not going to use it). fromMaybe would then take the value def and the number of Copies we get depend on the Maybe value, we're going to call it m.

So we need a way to get 0 or one depending on m, let's write this function and call it NotFound

NotFound : Maybe a -> Nat
NotFound Nothing = 1
NotFound (Just x) = 0

And now fromMaybe takes a value m, a default value def and a number of copies of def equal to the number returned by NotFound:

fromMaybe : (1 m : Maybe a) -> (0 def : a) -> {auto 1 defs : Copies (NotFound m) def} -> a
fromMaybe Nothing {defs = (More def Done)} def = def
fromMaybe (Just x) {defs = Done} def = x

and it works as expected! With this type signature it is impossible to implement the wrong function as the argument def won't be available if the value m is Just x.

It turns out we can generalise this approach to other branching operators. For example an if function would use its first branch if the condition is true and its second branch if the condition is false. In our case it would mean that the number of copies for the first branch is equal to 1 for True and 0 for False and likewise (but reversed) for the second branch:

IfTrue : Bool -> Nat
IfTrue True = 1
IfTrue False = 0

IfFalse : Bool -> Nat
IfFalse True = 0
IfFalse False = 1

ifQty : (1 switch : Bool) -> (0 tt, ff : b)
     -> {auto 1 trues : Copies (IfTrue switch) tt}
     -> {auto 1 falses : Copies (IfFalse switch) ff} -> b
ifQty False tt ff {trues = Done} {falses = (More ff Done)} = ff
ifQty True tt ff {trues = (More tt Done)} {falses = Done} = tt

In case you find it weird to pass an argument that's never used but a proof that is used, you can do the opposite and make the value implicit and the proof explicit:

ifQty' : (1 switch : Bool) -> {0 tt, ff : b}
     -> (1 trues : Copies (IfTrue switch) tt)
     -> (1 falses : Copies (IfFalse switch) ff) -> b
ifQty' False Done (More ff Done) = ff
ifQty' True (More tt Done) Done = tt

It makes it slightly less ergonomic since you have to write ifQty' True (More br1 Done) Done instead of ifQty True br1 br2.

In both cases we've achieved the same: An implementation of if that cannot possibly be implemented wrong.

Since we can deal with if we can also deal with Either, we're going to need a linear version of it because otherwise the usage annotations don't line up:

data LEither : (a, b : Type) -> Type where
  LLeft : (1 _ : a) -> LEither a b
  LRight : (1 _ : b) -> LEither a b

IsRight : LEither a b -> Nat
IsRight (LLeft _) = 0
IsRight (LRight _) = 1

IsLeft : LEither a b -> Nat
IsLeft (LLeft _) = 1
IsLeft (LRight _) = 0

either : (0 f : (1 _ : a) -> c) -> (0 g : (1 _ : b) -> c) -> (1 e : LEither a b)
      -> {auto 1 lefts : Copies (IsLeft e) f}
      -> {auto 1 rights : Copies (IsRight e) g} -> c
either f g (LLeft x) {lefts = (More f Done)} {rights = Done} = f x
either f g (LRight x) {lefts = Done} {rights = (More g Done)} = g x

The first post 01. Emulating exact-usage in Idris2 taked about a well-typed implementation of map on vector while counting usage. In this case we can do the same with LEither only using the function when the value is a Right and never when it's a Left:

mapEither : (0 f : (1 _ : a) -> b) -> (1 e : LEither c a) -> {auto 1 fn : Copies (IsRight e) f} -> LEither c b
mapEither f (LLeft x) {fn = Done } = LLeft x
mapEither f (LRight x) {fn = More f Done} = LRight (f x)