Open FranklinChen opened 6 years ago
This is in fact a special case of checking the correctness of "kind of quantity" as defined by the ISO 80000 standard. See this introduction for more details.
Checking kind-of-quantity is unfortunately much more complicated than basic dimensional analysis because there are no rules for arithmetic. Meaningful combinations of kinds-of-quantities must be stored in some database together with the kind-of-quantity corresponding to the result.
I'm not sure that there's a desirable way in Haskell to address "the well-known tricky cases such as making both Hz and Bq compatible with 1/s but not with each other", because the Haskell type system doesn't have subtyping in favor of better inference (among other benefits).
It might be possible to address the kind-of-quantity situation with a second layer of newtypes. I've sketched it below, using a terrible name in the hope that someone can come up with a better one:
newtype KQuantity (k :: Symbol) (s :: ExactPi') (d :: Dimension) a = KQuantity (SQuantity s d a)
deriving (...)
type Frequency' s a = KQuantity "Frequency" s DFrequency a
type Frequency a = Frequency' One
type RadioactiveActivity' s a = KQuantity "RadioactiveActivity" s DFrequency a
type RadioactiveActivity a = RadioactiveActivity' One
You could then use coerce
to go back and forth between quantities of the same dimension, but not between dimensions. So that would be cool.
I'm not opposed to this if all the details can be worked out. Probably involves splitting the dimensional arithemetic operators into typeclasses, which I've been considering anyway. Also would involve finding a good list of quantity names, for which the ISO standard may be a source. This may also lead to a solution for #23? But the amount of churn this would introduce could be considerable. And there is a question of whether to allow named quantity synonyms for "bare" quantity types, or only for these second-level newtypes. If you do allow it, you potentially have two confusingly similar types named Frequency
and no real reason to ever use the two-level one. If you don't allow it, almost all functions that include arithmetic would need a coerce
to unpack and repack the second-level newtypes.
In a discussion of dimensional units at https://disqus.com/home/discussion/khinsen/there_is_no_such_thing_as_software_development/?utm_content=read_more#comment-3900504830 it was noted that there is the question of "the well-known tricky cases such as making both Hz and Bq compatible with 1/s but not with each other" and I checked and
dimensional
does not handle this becausebut
DActivity
is just an alias toDFrequency
.