From 2n+1 to n

OCaml relies on a type-agnostic object representation centred around values which unify odd integers and aligned pointers. The last bit of a value distinguishes the two variants: zero indicates a pointer on the OCaml heap, while one encodes a tagged integer n as 2n+1. While this approach provides significant benefits, enabling a powerful foreign-function interface (FFI) and allowing the garbage collector to easily traverse the heap, a significant runtime overhead is also incurred. An operation as simple as the addition of n and m requires two hardware instructions: one to add the two odd numbers forming 2(n+m)+2, followed by another to decrement the result and adjust the tag bit, yielding 2(n+m)+1. In many instances, particularly in the standard library, sequences of such instructions present redundancies that are not properly eliminated by the compiler, despite obvious benefits to both execution time and binary size. In this talk, we discuss a type analysis implemented in the Duplo