Inspiration struck me tonight and I drafted my own inductive unary integers. I then used them to define quantities tagged by their dimensions, so that the formulae constructed out of them are sound from the point of view of dimensional analysis. The project uses experimental features of GHC here and there, but you should be able to compile this particular file with ghc XUndecidableInstances XTypeFamilies XDataKinds XUnicodeSyntax ℤ.hs
if you would like to.
My numbers sort of work, but it feels like such a waste of effort. Surely there should be a standard library for this sort of thing? I know there are natural numbers in GHC.TypeLits
, but they seem to not be suitable for this task since they are not inductive. And ideally, I suppose we should like to use binary arithmetic and not unary? Then, add some property checks by generating a large number of examples with Template Haskell and seeing if they compile… Not a small work! At the same time, it is not fancy enough to be of interest to the research community — the path is well trodden.
Is anyone else doing this sort of stuff? Does anyone care? What is the grand strategy for standard semifancy types in Haskell?
A cursory search revealed this:

typelevelintegers
. Small and nice, very easy to understand. Provides inductive type level integers that live in their own kind. If I wanted to explain type level programming to a stranger, I should use this one as an example. 
numtypetf
. Despite the name, most of the functionality is written as class instances, not type families. I think this one is more or less obsolete. 
numtypedk
. This one actually uses type families for everything. But it looks as though it simply enumerates a bunch of possible numbers, like literally «1 2 3». 
tfp
. Very fancy, source is not immediate to understand. So fancy that I am actually afraid to voice any value judgements.
None of these packages appear to be frequently used and in any sense «standard». There is so much wisdom in there — why this design choice was made and not the other — but it is not easily accessible.
On a final note — I should really like to have a special notation for type level numbers other than GHC.TypeLits.Nat
. Maybe some sort of a magic two parameter type class can be constructed that witnesses the correspondence of a certain type to a certain Nat
? It would work similarly to how functions toList
and fromList
are used to define overloaded lists, only at the type level. GHC then would use it to convert number literals to any custom kind of integers.
I do not really want to deliver one single message in this post. Rather, I want to start a conversation. Fancy types are a lonely place to be in.