1 blob is equal to 1 lbf⋅s2/in, or 12 slugs.
In their paper, the researchers developing the thoralf-plugin
suggest that it could match the uom-plugin in units of measure typechecking
capability. That's the challenge for this refactoring of both plugins.
Under the hood, the thoralf-plugin uses Z3 to solve equational theories. The
uom-plugin solves trivial equations, rewrites and simplifies constraints and
makes substitutions.
The uom-plugin depends on ghc-tcplugins-extra and
units-parser. It defines a quasiquoter for writing units with
measures, such as [u| 9.8 m/s^2 |].
The thoralf-plugin ships with one small units example, calculating distance in
m from velocity in m/s and time in s. The uom-plugin has a large number
of unit tests.
Initial goals:
✅ Identify, refactor and extract commonality in both unit plugins.
✅ Use the unit quasiquoter with the thoralf-plugin.
✅ Pass all units tests of the uom-plugin with the thoralf-plugin except for those involving unit conversions.
Stretch goals:
✅ Fix a longstanding bug with the uom-plugin (a bonus goal, stumbled on by accident 1).
❌ Add the experimental unit conversions of the uom-plugin to the thoralf-plugin.
- Added ghc-corroborate,
a new package exposing a flattened subset of GHC's API needed for typechecking
plugins as a single API across multiple GHC versions. It uses cabal
conditionals and mixins and avoids use of the
CPPlanguage extension and predefined macros for switching between GHC versions. - Used the same techniques for avoiding
CPPwith ghc-tcplugins-extra. - Moved the tracing of the
thoralf-pluginto ghc-tcplugins-trace.
The general idea with this was to rearrange the modules of each plugin for similarity between both (so that I could see that) and to split the packages up so that they could be shared between both.
- Moved the quasiquoter of the
uom-plugintouom-th. - Moved the units of measure (UoM) theory from the
thoralf-pluginand much of theuom-plugininternals touom-quantity. - Split the
thoralf-plugininto:thoralf-encodethoralf-pluginthoralf-plugin-rowsthoralf-plugin-uom
- Split the units of measure features of the thoralf plugin from the rest so
that we have
thoralf-plugin-uomfor units andthoralf-plugin-rowsfor the rest.
Find the new plugin in thoralf-uom/ and new versions of the existing
plugins in thoralf/ and in uom/.
We've not yet settled on final packaging but there are three potential options:
⑴ All plugins are in the one plugins-for-blobs package.
⑵ Plugins are in one of three packages; thoralf, uom or thoralf-uom.
⑶ Each plugin is in its own package, such as thoralf-plugin and uom-plugin.
> tree -L 2 -d
. ⑴ plugins-for-blobs.cabal
├── thoralf ⑵ thoralf.cabal
│ ├── encode ⑶ thoralf-encode.cabal
│ ├── plugin ⑶ thoralf-plugin.cabal
│ ├── plugin-rows ⑶ thoralf-plugin-rows.cabal
│ └── theory ⑶ thoralf-theory.cabal
├── thoralf-uom ⑵ thoralf-uom.cabal
│ ├── defs ⑶ thoralf-uom-defs.cabal
│ └── plugin ⑶ thoralf-uom-plugin.cabal
└── uom ⑵ uom.cabal
├── defs ⑶ uom-plugin-defs.cabal
├── examples ⑶ uom-plugin-examples.cabal
├── plugin ⑶ uom-plugin.cabal
├── quantity ⑶ uom-quantity.cabal
├── th ⑶ uom-th.cabal
└── tutorial ⑶ uom-plugin-tutorial.cabal
Plugins load modules from packages but while we're in transition with packaging
the function findModule has a set of known package names that it tries first.
knownPkgs = ["plugins-for-blobs", "thoralf", "uom", "thoralf-uom"]> cabal-plan tred --hide-exes --hide-builtin
thoralf-plugin-defs
└─ thoralf-plugin-uom
├─ thoralf-plugin
└─ uom-th
thoralf-plugin-rows
└─ thoralf-plugin
thoralf-plugin
└─ thoralf-encode
└─ thoralf-theory
└─ ghc-tcplugins-trace
uom-plugin-defs
└─ uom-plugin
└─ uom-th
uom-th
└─ uom-quantity
├─ ghc-tcplugins-trace
└─ units-parser
ghc-tcplugins-trace
└─ ghc-corroborate
└─ ghc-tcplugins-extra
└─ simple-smt
- Added
-ddump-tc-tracetracing to thethoralf-plugin-uom(theuom-pluginalready has this). - Added configuration for what to trace from the
thoralf-plugin-uom. There are two combination of these that are useful; a TOML style layout and an SMT2 style layout. The later output can be fed directly and unaltered into Z3 and is full of useful comments to help follow along. The SMT2 output for various unit tests can be found in the smt2/ghc-x.y folders, such as smt2/ghc-8.10.
I saw that the uom-plugin operated in two phases; (1) looking for unpacks and
(2) solving equations. This package now has 3 plugins:
Plugins.UoMthat combines the two phases as before.Plugins.UoM.Unpackthat does only the unpacking.Plugins.UoM.Solvethat does only the solving.
I pulled unit definitions out of uom-plugin and put these into
uom-plugin-defs. Also added a similar thoralf-plugin-defs package with the
same set of unit definitions.
I've shortened names of the plugins.
-- {-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}
++ {-# OPTIONS_GHC -fplugin Plugins.UoM #-}-- {-# OPTIONS_GHC -fplugin ThoralfPlugin.Plugin #-}
++ {-# OPTIONS_GHC -fplugin Plugins.Thoralf #-}There are two phases to solving with the uom-plugin, unpacking and solving
constraints. The plugin Plugins.UoM does both. It will unpack if there is any
of that work to do. Only when the unpacks are discharged will it solve. I've
separated these steps so that the unpacking can be used with solver plugins that
don't themselves do unit unpacking.
-
Two ways of solving with plugins from the
uom-pluginpackage.-
Using one plugin that does both unpacking and solving.
{-# OPTIONS_GHC -fplugin Plugins.UoM #-} -
Using one plugin for unpacking and another for solving.
{-# OPTIONS_GHC -fplugin Plugins.UoM.Unpack #-} {-# OPTIONS_GHC -fplugin Plugins.UoM.Solve #-}
-
-
Two ways of solving with plugins from the
thoralf-plugin-uompackage.-
Using one plugin that does both unpacking and solving.
{-# OPTIONS_GHC -fplugin Plugins.Thoralf.UoM #-} -
Using one plugin for unpacking and another for solving.
{-# OPTIONS_GHC -fplugin Plugins.UoM.Unpack #-} {-# OPTIONS_GHC -fplugin Plugins.Thoralf.UoM.Solve #-}With this, we're able to use the
uquasiquoter. Without the unpacking, trying to declare units would fail with:• Could not deduce: IsCanonical (Unpack (Base "byte")) arising from the superclasses of an instance declaration • In the instance declaration for ‘HasCanonicalBaseUnit "byte"’ | __ | declareBaseUnit "byte" | ^
-
A goal of this project is to run the same tests in thoralf-plugin-uom:units as
in uom-plugin:units.
- > cabal test uom-plugin:units --test-show-details=always"
+ > cabal test thoralf-plugin-uom:units --test-show-details=always"
Running 1 test suites...
Test suite units: RUNNING...
- uom-plugin:units
+ thoralf-plugin-uom:units
Get the underlying value with unQuantity
unQuantity 3 m: OK
unQuantity 3 s^2: OK
unQuantity 3 m s^-1: OK
unQuantity 3.0 kg m^2 / m s^2: OK
unQuantity 1: OK
unQuantity 1 (1/s): OK
unQuantity 1 1/s: OK
unQuantity 1 s^-1: OK
unQuantity 2 1 / kg s: OK
unQuantity (1 % 2) kg: OK
Attach units by applying the quasiquoter without a numeric value
m 3: OK
m <$> [3..5]: OK
m/s 3: OK
m s^-1 3: OK
s^2 3: OK
1 $ 3: OK
fmap [u| kg |] read $ "3": OK
fmap [u| kg |] read $ "3.0": OK
Showing constants
show 3m: OK
show 3m/s: OK
show 3.2 s^2: OK
show 3.0 kg m^2 / m s^2: OK
show 1: OK
show 1 s^-1: OK
show 2 1 / kg s: OK
show (1 % 2) kg: OK
Basic operations
2 + 2: OK
in m/s: OK
mean: OK
tricky generalisation: OK
polymorphic zero: OK
polymorphic frac zero: OK
Literal 1 (*:) Quantity _ u
_ = Double: OK
_ = Int: OK
_ = Integer: OK
_ = Rational, 1 *: [u| 1 m |]: OK
_ = Rational, mk (1 % 1) *: [u| 1 m |]: OK
_ = Rational, 1 *: [u| 1 % 1 m |]: OK
_ = Rational, mk (1 % 1) *: [u| 1 % 1 m |]: OK
(1 :: Quantity _ One) (*:) Quantity _ u
_ = Double: OK
_ = Int: OK
_ = Integer: OK
_ = Int: OK
errors when a /= b, (1 :: Quantity a One) (*:) Quantity b u
b = Double
a = Int: OK
a = Integer: OK
a = Rational: OK
b = Int
a = Double: OK
a = Integer: OK
a = Rational: OK
b = Integer
a = Double: OK
a = Int: OK
a = Rational: OK
b = Rational
a = Double: OK
a = Int: OK
a = Integer: OK
showQuantity
myMass: OK
gravityOnEarth: OK
forceOnGround: OK
- convert
- 10m in ft: OK
- 5 km^2 in m^2: OK
- ratio: OK
- 100l in m^3: OK
- 1l/m in m^2: OK
- 1l/m in m^2: OK
- 5l in ft^3: OK
- 2000000l^2 in ft^3 m^3: OK
- 42 rad/s in s^-1: OK
- 2.4 l/h in m: OK
- 1 m^4 in l m: OK
- show via convert
- A 1.01km: OK
- B 1010m: OK
errors
s/m ~ m/s: OK
m + s: OK
a ~ a => a ~ kg: OK
- a ~ b => a ~ kg: OK
- a^2 ~ b^3 => a ~ s: OK
read . show
3 m: OK
1.2 m/s: OK
1: OK
read normalisation
1 m/m: OK
-0.3 m s^-1: OK
42 s m s: OK
- read equality (avoid false equivalences)
- 1 m/m^2 /= 1 m: OK
- 1 m /= 1 m/m^2: OK
- All 84 tests passed (0.00s)
+ All 67 tests passed (0.00s)
Test suite units: PASS
1 of 1 test suites (1 of 1 test cases) passed.> cabal test all:tests
> stack test
To see tests of the uom-plugin with color but no build output to the terminal:
> stack test uom-plugin --no-terminal --test-arguments "--color=always"
We're using hpack-dhall to format
**/package.dhall files and generate **/*.cabal files. There's a shake build
rule cabal-files that does this for every package in this monorepo.
> ./cabal-shake-build.sh cabal-files
The uom-plugin has experimental unit conversions.
-- | Automatically convert a quantity with units @u@ so that its units
-- are @v@, provided @u@ and @v@ have the same dimension.
convert
:: forall a u v
. (Fractional a, Convertible u v)
=> Quantity a u
-> Quantity a v
-- | Calculate the conversion ratio between two units with the same
-- dimension. The slightly unusual proxy arguments allow this to be
-- called using quasiquoters to specify the units, for example
-- @'ratio' [u| ft |] [u| m |]@.
ratio
:: forall a u v (proxy :: Unit -> Type) proxy'
. (Fractional a, Convertible u v)
=> proxy' (proxy u)
-> proxy' (proxy v)
-> Quantity a (u /: v)How this works can be seen in the units tests for this feature.
testGroup "convert"
[ testCase "10m in ft" $ convert [u| 10m |] @?= [u| 32.8 ft |]
, testCase "5 km^2 in m^2" $ convert [u| 5km^2 |] @?= [u| 5000000 m m |]
, testCase "ratio" $ show (ratio [u| ft |] [u| m |]) @?= "[u| 3.28 ft / m |]"
, testCase "100l in m^3" $ convert [u| 100l |] @?= [u| 0.1 m^3 |]
, testCase "1l/m in m^2" $ convert [u| 1l/m |] @?= [u| 0.001 m^2 |]
, testCase "1l/m in m^2" $ convert [u| 1l/m |] @?= [u| 0.001 m^2 |]
, testCase "5l in ft^3" $ convert [u| 5l |] @?= [u| 0.17643776 ft^3 |]
, testCase "2000000l^2 in ft^3 m^3" $ convert [u| 2000000l^2 |] @?= [u| 70.575104 ft^3 m^3 |]
, testCase "42 rad/s in s^-1" $ convert [u| 42 rad/s |] @?= [u| 42 s^-1 |]
, testCase "2.4 l/h in m" $ convert [u| 2.4 l/ha |] @?= [u| 2.4e-7 m |]
, testCase "1 m^4 in l m" $ convert [u| 1 m^4 |] @?= [u| 1000 l m |]
]Units can only be converted if they share a dimension and for that they need to be derived from a base unit with a conversion ratio.
[u| rad = 1 1 |] -- dimensionless unit
[u| m, s |] -- base units
[u| km = 1000m, ha = 10000 m^2, l = 0.001 m^3, ft = 100 % 328 m |] -- derived unitsFootnotes
-
Adam Gundry made changes that got the
uom-pluginworking again withghc-9.0andghc-9.2when the plugin was stuck atghc-8.2, failing with later versions of GHC. I caught a problem with these changes not yet picked up by the unit tests and added a unit test for that. While working on reproducing tests for thethoralf-pluginI noticed that in some cases theuom-plugintests showed failures with unit order reversed. I then backported a fraction of Adam's changes intoghc-corroborate. With just these few changes tocmpTyCon,cmpTypeandcmpTypesthe plugin works again withghc-9.2. I've tested this with flare-timing and nothing bad happens but the fix comes with a core-lint error. ↩