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.