[Haskell-cafe] Is it possible to do type-level arithmetic without
paul at cogito.org.uk
Fri Jun 5 17:58:27 EDT 2009
This is a bit beyond my normal level of expertise, but if I understand
it correctly the type checker is normally limited to type functions that
are "primitive recursive"
(http://en.wikipedia.org/wiki/Primitive_recursive_function). This means
that they are guaranteed to terminate, but on the other hand the
resulting language is not Turing complete.
Setting UndecidableInstances lifts the Primitive Recursive restriction,
making the type checker Turing Complete, but also creating the potential
for endless loops.
So yes, you can do type arithmetic without UndecidableInstances,
provided you limit yourself to the Primitive Recursive axioms. The
Wikipedia page lists them, and turning them into Haskell type classes
shouldn't be more than a few milli-Olegs.
More information about the Haskell-Cafe