4 ms·

Could anyone provide some intuition for what's supposed to be happening in the sample code?

• yorwba 9y ago
  The first few lines define the interface that is going to be used and its monotonicity properties. E.g. getAt :: (m : NatMap, k : Nat) ⇒ Nat[↑ m, ? k] means that when you get the value of key k in the map m, the result is a number that increases as the map increases. Based on the names, I guess that getAt is for value access, joinAt updates an entry of a map with a new value, span returns the maximum key with an associated entry, max is the maximum of two numbers, emptyMap is a map without entries and + and > are the usual mathematical functions. The GCounter type is essentially just a wrapper around maps that will be used to count things, apparently. The function sumCounters they define first unwraps the maps backing the counters and determines the maximum key that will have to be considered. Then there's a helper function sumCell which takes a key k and an accumulator acc containing the intermediate result for all previous keys. The helper function then checks whether all keys have been handled already, and returns the accumulator if that's the case. Otherwise it updates the accumulator with the sum of the entries for the given key in the two input maps. Then it calls itself recursively to handle the next key with the new accumulator. The final line just starts off the helper function with an empty accumulator and the first key.