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.

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:

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.

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 (-*)

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