Suggestions

[ghost]

Hello,

• Are you planning to support SI prefixes? (I guess they could be handled already by writing extra versions of each defined unit manually or with TH)
• What about logarithmic units, that are not always additive? (for example dB + dB = dB; dB + dBm = dBm + dB = dBm; but dBm + dBm makes no sense) Or do you feel these don't belong here / would unnecessarily complicate everything?

[adamgundry]

Many thanks for the suggestions!

Are you planning to support SI prefixes? (I guess they could be handled already by writing extra versions of each defined unit manually or with TH)

At the moment, the only way to deal with SI prefixes is to define them individually as needed, e.g. [u| km = 1000 m |]. I suppose it would be fairly easy to extend the TH code to generate a whole family of prefixed units on request. It would be nicer to have a way of defining the prefixes once, but that would probably require a more substantial redesign, in order to identify the prefixes in advance.

What about logarithmic units, that are not always additive? (for example dB + dB = dB; dB + dBm = dBm + dB = dBm; but dBm + dBm makes no sense) Or do you feel these don't belong here / would unnecessarily complicate everything?

I've not thought about it in detail, but I don't see how to directly generalise the type of +: to cover logarithmic units. I suppose we could add another operator (say +*) that performs addition but has the type of multiplication. I think that would work for your positive examples provided dB was dimensionless. But unless we track the distinction in the types, dBm +: dBm = dBm would typecheck (even if dBm +* dBm = dBm would not). More thought needed here...

[ghost]

Thanks for the plugin! :) It has saved me a lot of trouble already.

I suppose we could add another operator (say +*) that performs addition but has the type of multiplication. I think that would work for your positive examples provided dB was dimensionless. But unless we track the distinction in the types, dBm +: dBm = dBm would typecheck (even if dBm +* dBm = dBm would not).

Seems reasonable. What about a type family

type family Additive (u :: Unit) :: Bool

the types of +: and +* could look like

(+:) :: (Num a, Additive u ~ True) => Quantity a u -> Quantity a u -> Quantity a u
(+*) :: (Num a, Additive u ~ False, w ~~ u *: v) => Quantity a u -> Quantity a v -> Quantity a w

Then the templates would by default declare type instance Additive u = True, with an option to declare it False instead. This does allow dBm +* dBm :: dBm^2, but I guess it's technically not wrong, and would be easily caught by any code that expects a dBm.