Feature Proposal: Monetary Units

[ryantrinkle]

It would be great to be able to express units other than SI units, such as dollars. This would allow the type checker to manipulate amounts like "USD/day" in a type-checked way.

[dmcclean]

This is an interesting request. Other people have mentioned wanting to have arbitrary counting units as well, e.g. "cars / year".

Our current approach has a lot of merits, but ease of supporting this is not one of them. The problem is that we need to be able to use type families to take the type-level product of our type-level dimension type.

Ideally instead of representing type-level dimensions by 7-tuples of integers, we could represent them by finite maps from Symbol (or another open data kind) to integer, basically the free group on infinitely many generators indexed by symbols. But getting GHC's current level of type-level programmability to do that seems like a significant challenge to me.

@adamgundry's uom-plugin library does tackle this, AIUI by using only a type-checker plugin to compute in the equational theory of units (for us it would be dimensions, not units, but again AIUI his library statically tracks units and not dimensions), as opposed to trying to program it in GHC Haskell's type system.

[adamgundry]

There's also @goldfirere's units package, which supports arbitrary user-defined units (with * as the open kind) using lots of clever type-level programming.

[dmcclean]

It would be really nice if we had the ability to declare new open kinds and inhabitants of them. The current way with EmptyDataDecls and convention is a good workaround, but it does ruin the documentation value of kind signatures. We'd never put up with the term-level equivalent. I know there is a GHC trac ticket but I can't find it at the moment.

I was thinking this same thing while listening to a presentation at Boston Haskell last week about servant, which uses the * thing a lot for tracking type level content types among other things.

Symbol (or "newkind" wrappers around it) is a useful alternative for some things, but it introduces the potential for name collisions.

[goldfirere]

I'm unaware of any Trac ticket for this feature, but I very much think we should have it. And it would be easy to implement, I believe. The closest thing to a Trac ticket is https://ghc.haskell.org/trac/ghc/ticket/9840#comment:6 but that was me hijacking another ticket.

I'm afraid I don't have the bandwidth to champion this now, though. But do please post a ticket and I'll support it!

[dmcclean]

Will do.

I agree with your suspicion that it's easy to implement, although I've certainly been wrong about that sort of thing in the past. Do you have any thoughts on what concrete syntax I should propose for declaring types that are in an open kind other than *? Or for the kinds themselves?

[goldfirere]

How about, for example, data open Unit? It doesn't roll off the tongue, exactly. But it steals no more syntax than data family does. And it leaves open (no pun intended) the possibility that we'll allow open unions at the term level someday.

What's more difficult is the syntax for declaring inhabitants of an open kind. data fits with the hacks that folks have used up until now, but it's exactly wrong. Unless: data constructor Meter :: Unit. Ooh. I quite like that. To consider the possibility of term-level use, names declared with data constructor would indeed be in the term-level namespace, even though they could only be used in types for now.

[dmcclean]

On the second bit, I checked and KindSignatures already allows declaring the result kind of a data declaration, as data A (b :: * -> *) :: *, it's just that it enforces that if the result kind is declared then it must be *.

Would simply relaxing this restriction be enough to solve the syntax for declaring inhabitants of an open kind, yielding data Length :: Dimension? It seems to me that it would; after all * is an open kind. But that may be because I don't understand your point regarding the term-level interpretation of your data constructor ... proposal.

[goldfirere]

Yes, what you propose would work syntactically. But it's bogus semantically.

The problem is that in data Length :: Dimension, you're not declaring a datatype anywhere! The data keyword is used to define datatypes. Instead, this declares a constant Length that is equal only to itself. But we have a word for such things: data constructors.

For the term-level ideas: Right now, every (normal, non-promoted) datatype is closed. We declare all of its constructors all at once. But I've seen a desire to relax that restriction and allow for open datatypes. What we're discussing here is the same idea, one level up. I just want to future-proof the concrete syntax so that it will work if we ever work out the details one level down.

[dmcclean]

Ahh, I get it now. I just had a lightbulb go on about wanting the same thing one level down (a need sort of met by Data.Unique in some circumstances, but not really because of the IO requirement, although I have seen some hacks for getting around that for top-level declarations). I came here to say so and you already had.

OK, got it. I will propose this on GHC trac with these syntax suggestions and post the link here.

[dmcclean]

See https://ghc.haskell.org/trac/ghc/ticket/11080 in which I hope I explained this adequately.

[dmcclean]

I am closing this as out of scope for now.

We may revisit that if and when a solution of open data kinds or full dependent types makes another model for dimension possible and even allows abstracting the whole library over a kind of dimensions.