-
Notifications
You must be signed in to change notification settings - Fork 5
Open
Description
I've been thinking about a new design for the API, which does not rely on Symbol
as the kind of base units, and does not require the quasi-quoter to write literals.
The library should provide this:
data UnitKind
type Unit = UnitKind -> Type
Now user code can define empty datatypes representing base units, and type synonyms for units:
data U_m :: UnitKind -> Type
data U_s :: UnitKind -> Type
data U_kg :: UnitKind -> Type
type U_N = U_kg *: U_m :/ U_s ^: 2
and at the value level:
m :: Num a => Quantity a U_m
m = MkQuantity 1
_N :: Num a => Quantity a U_N
_N = MkQuantity 1
thus we can write:
5 *: _N /: m :: Quantity Int (U_N /: U_m)
Metadata
Metadata
Assignees
Labels
No labels