I have recently started messing around with DataKinds in order to have compile-time scientific units for arithmetic. I have more or less figured out a way to do what I want but I feel like it could be a lot cleaner.
I needed integers that could potentially be negative (m^-1) so I decided to use integers rather than naturals. But as it turns out when you do :k 5 it gives you GHC.Types.Nat which does not fit my needs. I ended up instead making my own custom algebraic integer type. As well as defining addition and subtraction type families to use with it.
But this all seems very indirect, it seems like there is no good reason why I can't just directly use all the existing functions for manipulating data at compile time within type families.
Basically I want the following to essentially be generated automatically:
type family (a :: Int) + (b :: Int) :: Int where
-- Should be automatically derivable from (+) applied to Int
Is that possible, if not then why not?
Also is there an easy way to obtain a runtime value back from a type? Specifically when writing a Show instance for all these types I basically just want to pull in the phantom type representing the unit combination and convert it to a string. All the ways I can think of doing that right now seem really verbose.
It looks like the answer to this question is simply that you cannot currently do either of those things automatically. Hopefully it won't take too long before this kind of thing becomes possible.