Drawbacks of Dimensions being Kind, and closed type families

[bjornbm]

Well, the drawback is that they are both closed. This makes it impossible to drop in a replacement system of dimensions, such as those from the CGS or Extensible modules, or to experiment with, e.g., making angles an eighth dimension.

Any thoughts on the tradeoffs?

[dmcclean]

Personally I'm strongly tempted to make it an explicit non-feature, because the complexity cost is pretty high to any of my other ideas, and the benefits don't accrue to me personally. ;)

I also think the ideal answers to the CGS and Extensible concepts might be different.

For extensible, I've always thought that it would be nice if instead of modelling Dimension as a type-level 7-tuple of naturals it was modeled as a type-level finite map from String (or some other open data kind, if we had them) to Nat with the obvious multiplication and division operators. ("If you liked dimensional-tf, but thought the error messages were a little short, come on down to Doug's Bad Ideas Emporium!")

This gets you apples and oranges at the cost of a flat global namespace with absolutely no policing or hygiene. An open data kind Symbol would clean it up nicely, and might be something you could reasonably hope to achieve. Leaving the parameter at kind * and using EmptyDataDecls is also an option, but feels like a step backwards.

For a CGS implementation, I'd almost like to see either an entirely parallel CgsDimension kind with type families for converting back and forth (putting in and out your vacuum permittivity and such noise all over the place depending on the Dimension side of things). You could generalize to the point of having only one (*) which works within any whatever-kind-this-concept-is, say DimensionSystem or something, but the complexity goes up and up.

[bjornbm]

The issue I see with having e.g. CgsDimension be a different kind is that libraries that could be polymorphic across systems of units (e.g. linear algebra) will not be if they have the Dimension sprinkled everywhere, and (*) etc are a closed type family with only Dimension instances.

Probably some other things would need to change for a LinAlg lib, such as Done being polymorphic too:

type family DOne a :: *
type instance DOne SI = Dim Zero Zero Zero Zero Zero Zero Zero
type instance DOne CGS :: CgsDim Zero Zero Zero

_1 :: (Num a) => Quantity (DOne s) a
_1 = Dimensional 1
...

I'm not sure who's problem it would be solving, though. I don't expect to use any system beside SI myself, and clearly the tradeoff is added complexity and likely horrendous error messages. But it is an interesting problem so I will probably not be able to keep myself from wasting time on some thinking and prototyping anyway.

[dmcclean]

This thought is only half baked, but what happens with

type CgsDimension l m t = Dim l m t Zero Zero Zero Zero

[bjornbm]

I think that would make it far too easy to have your CGS quantities polluted by accidental multiplication with an SI quantity. You'll also need to redefine lots of “quantities” and units (e.g. ampere) in only CGS dimensions.

[bjornbm]

“Won't fix.”

[bjornbm]

Actually, your idea of type CgsDimension l m t = Dim l m t Zero Zero Zero Zero might not be too bad. An insight I had a while back that all you really need for CGS is a redefinition of (*~) and (/~). E.g.

type family SiToCGS (d::Dimension) :: Dimension where ...
type family CgsToSI (d::Dimension) :: Dimension where ...

siToCGS :: Quantity d a -> Quantity SiToCGS a
siToCGS (Dimensional x) = Dimensional x

cgsToSI :: Quantity d a -> Quantity CgsToSI a
cgsToSI (Dimensional x) = Dimensional x

(*~) :: a -> Unit d a -> Quantity (SiToCGS d) a
(*~) = siToCGS . D.(*~)

(/~) :: Quantity d a -> Unit (CgsToSI d) a -> a
(/~) = D.(*~) . cgsToSI

where the tricky part is obviously the type family instances.

You will run into trouble if you mix the CGS quantities with SI quantities (and forget to convert them with siToCGS first), but other than that it should work well and allows re-use of all the existing SI units.

[dmcclean]

SIToCGS isn't injective, though, and so CgsToSI is multi-valued. Which SI dimension do you pick?

Also there are several competing flavors of SIToCGS depending on how you decide to treat the electrical units. see http://en.wikipedia.org/wiki/Centimetre%E2%80%93gram%E2%80%93second_system_of_units#Various_extensions_of_the_CGS_system_to_electromagnetism et seq.

[bjornbm]

Ah, yes. My intention was that it would work as in Numeric.Units.Dimensional.CGS where the desired SI dimension is inferred (e.g. by the Unit passed to (/~) above). But now that you point it out that clearly wouldn't work with a type family as drafted; would have to use a MPTC I think.

As for competing CGS flavors I guess they would have to be separate modules (EsuCGS, EmuCGS, …).

[dmcclean]

What about adding another phantom type to represent what unit basis a dimensional value is in?

data Dimensional (s :: *) (v :: Variant) (d :: Dimension) (a :: *) = Dimensional a

Now EmptyDataDecls for SIBasis, CGSEsuBasis, ... (chosen over another data kind to leave it open, it would be nice if there were open data kinds for this sort of symbolic thing).

Ideally you would want the kind of the d parameter to be chosen by a kind family that was parameterized by s, but I don't think that is possible in today's world (although there have been papers talking about it). (Didn't try it.)

I still think the sweet spot is to ignore the whole issue entirely. In fact, if we did have this mechanism, I would be more inclined to use it to have a basis where angles aren't dimensionless than to use CGS units. (That says more about my applications than it does about the mechanism, though.)

[bjornbm]

In terms of optimizing the value of our (at least my) time spent I absolutely agree with the first sentence of the last paragraph. :)