Open riaqn opened 8 months ago
I actually had an intern working on this subject two years ago. The main issue is that recursive types in OCaml are not inductive, so the function you described is not equivalent to the identity:
let rec loop = Foobar (loop, loop)
let v = just_id loop (* doesn't terminate *)
You can even create examples where a function is the identity on all non-cyclic structures but must not be allowed to terminate on (some) cyclic ones.
On the other hand, if we could solve this issue the rest is easy, so maybe we could try adding inductivity annotations to types to forbid recursive values, and then make use of that for detecting identity functions.
Example:
Produced
cmm
:I imagine the
just_id
should just be optimised into%id
.