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:
distance :: Int : Meter' ()
distance = liftV 10 ** meter
> distance -- prints:
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:
energyInBarOfChocolate :: Int : Joule ()
energyInBarOfChocolate = liftV 2_300_000 ** joule
> energyInBarOfChocolate -- prints:
forceOver5Meter :: Int : Newton ()
forceOver5Meter = energyInBarOfChocolate // (liftV 5 ** meter)
> forceOver5Meter -- prints:
> :t forceOver5Meter ** liftV 5 ** meter // sec -- what type does it have?
Int : Kg P1 * Meter P2 * Sec N3 * () -- without Type aliases:
( 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:
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: