Type-safe Units of Measures in Purescript

Announcements
#1

Hi, for a while I’ve been really exited about possibilities, that PureScripts typesystem opens up with rowtypes, instance-chaining etc. and how people use them.
I wanted to contribute to the growing number of libraries using the typelevel capabilities of PS.

As a result I created a library (https://pursuit.purescript.org/packages/purescript-typelevel-measures) for dealing with values with units of measure (like seconds, meter, kilogram) in a type-safe manner. In other words, the library allows PureScript to do dimentional analysis as part of the typechecking.

The library enables automatic simplification of terms (e.g. 1m²/s³ * 23s³/kg = 23 m²s³/s³/kg, which the library simplifies to 23 m²/kg), the addition of new base-units and still allows PureScript to infer the types of expressions.

Here is an example:

import Type.Data.Units
import Type.Data.Units.SI
import Type.Data.Peano.Int

distance :: Int : Meter' ()
distance = liftV 10 ** meter

> distance -- prints:
10·m¹

avgSpeed :: Int : Meter' () -> Int : Sec' () -> Int : Meter' * Sec N1 * ()
avgSpeed a b = a // b

speedOver10m :: Int : Meter' * Sec N1 ()
speedOver10m = avgSpeed distance (liftV 5 ** sec)

> speedOver10m  -- prints:
2·m¹s⁻¹

energyInBarOfChocolate :: Int : Joule ()
energyInBarOfChocolate = liftV 2_300_000 ** joule

> energyInBarOfChocolate -- prints:
2300000·kg¹m²s⁻²

forceOver5Meter :: Int : Newton ()
forceOver5Meter = energyInBarOfChocolate // (liftV 5 ** meter)

> forceOver5Meter -- prints:
460000·kg¹m¹s⁻²

> :t forceOver5Meter ** liftV 5 ** meter // sec -- what type does it have?
Int : Kg P1 * Meter P2 * Sec N3 * () -- without Type aliases:
Measured Int                                           
  ( kg :: MeasureExp KgT (Pos (Succ Z))                
  , meter :: MeasureExp MeterT (Pos (Succ (Succ Z)))   
  , sec :: MeasureExp SecT (Neg (Succ (Succ (Succ Z))))
  )

-- add Measured:
addedDistances = liftV 1 ** meter ++ liftV 1 ** meter

> addedDistances -- prints:
2·m²

EDIT: Updated example

As a bonus I also created an additional package for typelevel peano numbers, which is compatible with the constructs from typelevel-prelude (like Ordering, Eq). Typevel-peano can also parse symbols to numbers:

parseInt (undefined :: SProxy "-1337") :: (Succ^1337 (... Z)

Please comment and criticize; I’m looking forward to your feedback.

4 Likes
#2

Very interesting way to use the type system.
I don’t see in the repo where kind Measure export is defined near

foreign import kind Measure

Is it in another repo?

I have several suggestions:

  • the examples don’t show the right imports for modules Type.Data.Units and Type.Data.Units.SI
  • I would expect 2 meters with

liftV 1 ** meter ++ liftV 1 ** meter

What is the purpose of (++)?

#3

The imports in the README were outdated. I’ve corrected that.

The kind is defined here and exported at the top of the file. Is that what you’re looking for?

That should be the case. When I use psci I get:

> import Data.Type.Units
> import Data.Type.Units.SI
> liftV 1 ** meter ++ liftV 1 ** meter
2·m²

That might be something related to missing exports. I’ll check that.
EDIT: Even in a new purescript project, the code above works.

Yes, you’re right. (++) is plus for measured values what (+) is for semirings. Same goes for (//), (**) and (-*) for (-)

#4

Bear my newbieness but I didn’t know it was possible to overload the kind system. The only document I’ve read about foreign imports is the PureScript book and this part is outdated. I was wrongly expecting a javascript export.

You mean it doesn’t, do you?

too bad for (–) :wink:

#5

Don’t worry about that. I had not known about that, before I started this project either. I found out about that feature from some slides from Justin Woo https://speakerdeck.com/justinwoo/rowlist-fun-with-purescript?slide=3
Foreign imports of values requires a corresponding definition in a javascript file; imports of types and kinds do not.

No, I mean it does work. Here is what I did:

$ git clone https://gitlab.com/csicar/purescript-typelevel-measures-test-proj test
$ cd test
$ bower install
$ pulp psci
> import Type.Data.Units
> import Type.Data.Units.SI
> liftV 1 ** meter ++ liftV 1 ** meter
2·m²

It would be nice if -- would work but… oh well. I also though about just using (+), (-), but using the same name as a operator from Prelude could be more annoying than (++) and (-*)

1 Like
#6

Thanks for the link :pray:!

What I wanted to say refers to the logical result of adding 1 meter to 1 meter. The result should be a measure of length, not a measure of area.
I also can see

whereas I expect to see

#7

Yes, you’re right. The type of add and sub was incorrect. I’ve now changed that in the newest Version.

> meter ++ meter :: Int : _
2·m¹

EDIT: Add Type annotation to help PS infer the type

Thank you for the feedback!

2 Likes