As far as I know, Idris (a dependently-typed purely functional language which is very close to Haskell) deals with this in a quite straightforward way. Compiler is aware of Nat
s and Fin
s (upper-bounded Nat
s) and replaces them with machine integer types and operations whenever possible, so the resulting code is pretty effective. However, that’s not true for custom types (even isomorphic ones) as well as for compilation stage (there were some code samples using Nat
s for type checking which resulted in exponential growth in compile-time, I can provide them if needed).
In case of Haskell, I think a similar compiler extension may be implemented. Another possibility is to make TH macros which would transform the code. Of course, both of options aren’t easy.