Cryptol.Transform.MonoValues

This module implements a transformation, which tries to avoid exponential slow down in some cases. What's the problem? Consider the following (common) patterns:

fibs = [0,1] # [ x + y | x <- fibs, y <- drop`{1} fibs ]

The type of fibs is:

{a} (a >= 1, fin a) => [inf][a]

Here a is the number of bits to be used in the values computed by fibs. When we evaluate fibs, a becomes a parameter to fibs, which works except that now fibs is a function, and we don't get any of the memoization we might expect! What looked like an efficient implementation has all of a sudden become exponential!

Note that this is only a problem for polymorphic values: if fibs was already a function, it would not be that surprising that it does not get cached.

So, to avoid this, we try to spot recursive polymorphic values, where the recursive occurrences have the exact same type parameters as the definition. For example, this is the case in fibs: each recursive call to fibs is instantiated with exactly the same type parameter (i.e., a). The rewrite we do is as follows:

fibs : {a} (a >= 1, fin a) => [inf][a] fibs = {a} (a >= 1, fin a) -> fibs' where fibs' : [inf][a] fibs' = [0,1] # [ x + y | x <- fibs', y <- drop`{1} fibs' ]

After the rewrite, the recursion is monomorphic (i.e., we are always using the same type). As a result, fibs' is an ordinary recursive value, where we get the benefit of caching.

The rewrite is a bit more complex, when there are multiple mutually recursive functions. Here is an example:

zig : {a} (a >= 2, fin a) => [inf][a] zig = [1] # zag

zag : {a} (a >= 2, fin a) => [inf][a] zag = [2] # zig

This gets rewritten to:

newName : {a} (a >= 2, fin a) => ([inf][a], [inf][a]) newName = {a} (a >= 2, fin a) -> (zig', zag') where zig' : [inf][a] zig' = [1] # zag'

zag' : [inf][a] zag' = [2] # zig'

zig : {a} (a >= 2, fin a) => [inf][a] zig = {a} (a >= 2, fin a) -> (newName a <> <> ).1

zag : {a} (a >= 2, fin a) => [inf][a] zag = {a} (a >= 2, fin a) -> (newName a <> <> ).2

NOTE: We are assuming that no capture would occur with binders. For values, this is because we replaces things with freshly chosen variables. For types, this should be because there should be no shadowing in the types. XXX: Make sure that this really is the case for types!!

Documentation

rewModule :: Module -> Module

Note that this assumes that this pass will be run only once for each module, otherwise we will get name collisions.