How does Unison compute the hashes of recursive functions?

user_7594226 0
Viewed 42

In Unison, functions are identified by the hashes of their ASTs instead of by their names.

Their documentation and their FAQs have given some explanations of the mechanism.

However, the example presented in the link is not clear to me how the hashing actually works:

They used an example

f x = g (x - 1)
g x = f (x / 2)

which in the first step of their hashing is converted to the following:

$0 = 
  f x = $0 (x - 1)
  g x = $0 (x / 2)

Doesn't this lose information about the definitions.

For the two following recursively-defined functions, how can the hashing distinguish them:

# definition 1
f x = g (x / 2)
g x = h (x + 1)
h x = f (x * 2 - 7)

# definition 2
f x = h (x / 2)
g x = f (x + 1)
h x = g (x * 2 - 7)

In my understanding, brutally converting all calling of f g and h to $0 would make the two definitions undistinguishable from each other. What am I missing?

unison-lang
1 Answers

The answer is that the form in the example (with $0) is not quite accurate. But in short, there's a special kind of hash (a "cycle hash") which is has the form #h.n where h is the hash of all the mutually recursive definitions taken together, and n is a number from 0 to the number of terms in the cycle. Each definition in the cycle gets the same hash, plus an index.

The long answer:

Upon seeing cyclical definitions, Unison captures them in a binding form called Cycle. It's a bit like a lambda, but introduces one bound variable for each definition in the cycle. References within the cycle are then replaced with those variables. So:

f x = g (x - 1)
g x = f (x / 2)

Internally becomes more like (this is not valid Unison syntax):

$0 = Cycle f g ->
  letrec
   [ x -> g (x - 1)
   , x -> f (x / 2) ]

It then hashes each of the lambdas inside the letrec and sorts them by that hash to get a canonical order. Then the whole cycle is hashed. Then these "cycle hashes" of the form #h.n get introduced at the top level for each lambda (where h is the hash of the whole cycle and n is the canonical index of each term), and the bound variables get replaced with the cycle hashes:

#h.0 = x -> #h.1 (x - 1)

#h.1 = x -> #h.0 (x / 2)

f = #h.0

g = #h.1
user_34340
Related