Investigate encoding recursive demand types
@jmct brought up an interesting point in #12364 (comment 122148) that I just came to remember today: Instead of cutting off strictness/usage/nested CPR analysis information at some arbitrary cut-off in fixed-point iteration, we should try to encode the recursive nature in the lattice instead. If all went well, we are able to encode the subset of regular recursive types (in the sense of i.e. TAPL 21.8. Here's the gist of it), for which I'm pretty confident we can define equality and lattice operations. According to the comment above, we'll have problems with polymorphic recursion, but I'm not ready to give in on this yet.
Implementing recursive lattices would allow faster termination of fixed-point iteration, while also providing the perfect amount of information! To make this more concrete, let's say we augment the nested CPR lattice with
data Cpr
= ...
| CprVar Unique
| CprFix Unique Cpr
Apart from introducing all kinds of well-formedness problems, here's an example that shows their usefulness (there are probably more compelling examples somewhere out in the wild):
repeat :: a -> [a]
repeat x = x : repeat x
repeat
has an infinitely deep CPR property, captured by μX.(-,X)
. I'm using some new syntax from my nested CPR branch here, where -
encodes Top and (,)
a constructed pair. The term above would correspond to CprFix 42 (CprProd [CprTop, CprVar 42])
in our embedding. This is at the same time much more expressive than cutting off at depth, say, 3, corresponding to (-,(-,(-,-)))
, and also more efficient, since fixed-point iteration will stabilise after the second iteration. Here's the trace of repeat
s CprType over each fixed-point iteration, under the assumption we introduced a fresh variable X standing for repeat
:
initially:
. -> . -> μX.X <-- this is probably similar/equivalent to bottom?! Not sure about the scope of X
after iteration #1:
. -> . -> μX.(-, X)
after iteration #2, reaching the fixed-point:
. -> . -> μX.(-, X)
Turns out I'm not really able to express the proper formalism/lattice here, so this needs some more thinking. But I think this should be the general story.