typelevel / general

Repository for general Typelevel information, activity and issues
19 stars 8 forks source link

Submitting coulomb for typelevel incubator membership #78

Closed erikerlandson closed 7 years ago

erikerlandson commented 7 years ago

coulomb is a statically typed unit analysis library for Scala, supporting the following features:

The coulomb project meets the following requirements:

Thank you for your consideration!

erikerlandson commented 7 years ago

@milessabin expressed interest in a comparison between coulomb, libra and squants. A comprehensive comparison is daunting but I'll take a stab at sketching the most fundamental differences here.

Firstly, squants, libra and coulomb are all addressing the same basic use case: augment numeric quantities with statically typed unit information that can be checked for unit-analytic consistency at compile time.

squants is by far the oldest, and most mature. It has a rich feature set, including support for numeric vectors, many predefined units, and support for i/o with unit types. It is less general in the sense of supporting arbitrary unit expressions, as libra and coulomb do. Extending it is a more or less "manual" process of defining new classes and conversions between them.

coulomb and libra evolved fairly recently, and in parallel. We discovered each other in the last couple months, when I happened to stumble on Zainab Ali's libra talk at the typelevel Copenhagen summit schedule. coulomb and libra aim at providing a more generalizable capability, by leveraging modern Scala dependent-typing techniques. A programmer can define new unit expressions that leverage the type system to automatically integrate with existing units. The two packages achieve this in different ways.

coulomb's unit types are built on a system of unit traits paired with binary infix "operator" types %*, %/ and %^, which allow unit expressions (UnitExpr) of arbitrary complexity to be built up, for example:

val bandwidth = 1024.withUnit[(Giga %* Byte) %/ Second]
val acceleration = 32f.withUnit[Foot %/ (Second %^ _2)]
val ohms = (0.01).withUnit[(Kilogram %* (Meter %^ _2)) %/ ((Second %^ _3) %* (Ampere %^ _2))]

These types are recursively traversed at compile time, using an algorithm coded into scala macros, that simultaneously determines when unit type expressions are compatible (i.e. can be converted to each other), and if so what the conversion factor is. The algorithm itself deserves a blog post, but the code is very suggestive of how it works.

A useful property of this unit expression architecture is that it is convenient for defining function signatures

def foo(acceleration: Double WithUnit (Foot %/ (Second %^ _2))) = { ... }

And also for deriving new units

@UnitDecl("furlong", 660)
trait Furlong extends DerivedUnit[Foot]

@UnitDecl("earthgravity", 9.807, "g")
trait EarthGravity extends DerivedUnit[Meter %/ (Second %^ _2)]

The libra library represents static unit types as an HList. @zainab-ali has already written an excellent blog post and given a talk on how she designed her system, so I will not attempt to duplicate a detailed description here. My intuitions about how non-atomic type expressions are built up in this HList representation aren't very good yet; I'd welcome any insights!

Some cool features of libra include rational exponents (coulomb currently supports integer exponents, although it could be enhanced to use the rational system that libra uses), which in turn allows taking roots of unit quantities in addition to exponentiation. Because it is built directly on HList, it is likely to integrate with other typelevel projects with low friction.

There are many other differences, but I believe that these are the most fundamental ones. Hopefully this very brief comparison is a useful baseline!

erikerlandson commented 7 years ago

An addendum to the comparison above, here are examples of creating a value of 9.8 m/s^2 in each of the three packages. Note, I have edited out scala path prefixes of most types, because it improves the clarity of seeing the structure of the types, for comparison.

First, squants:

scala> val (d, t) = (Meters(9.8), Seconds(1.0))
d: squants.space.Length = 9.8 m
t: squants.time.Time = 1.0 s

scala> d / (t * t)
res1: squants.Acceleration = 9.8 m/s²

Note, here it results directly in a type of Acceleration, which is a result from "hard-coded" definition of Meter / (SecondSquared)

Next, is the libra equivalent:

scala> val (d, t) = (9.8.m, 1.0.s)
d: libra.QuantityOf[Double,Length,Metre] = Quantity(9.8)
t: libra.QuantityOf[Double,Time,Second] = Quantity(1.0)

scala> d / (t * t)
res2: Quantity[Double,(MetricUnit[Int(0),Length], Fraction[Int(1),Int(1)]) with KeyTag[Length,(MetricUnit[Int(0),Length], Fraction[Int(1),Int(1)])] :: (MetricUnit[Int(0),Time], Fraction[Int(-2),Int(1)]) with KeyTag[Time,(MetricUnit[Int(0),Time], Fraction[Int(-2),Int(1)])] :: HNil] = Quantity(9.8)

here, you can see the HList structure of the type, and the Fraction exponents. Also note the use of literal types.

Lastly, is the equivalent in coulomb:

scala> val (d, t) = (Meter(9.8), Second(1.0))
d: Quantity[Double,Meter] = Quantity(9.8)
t: Quantity[Double,Second] = Quantity(1.0)

scala> d / (t * t)
res2: Quantity[Double,%/[Meter,%^[Second,IncChurchInt[IncChurchInt[ZeroChurchInt]]]]] = Quantity(9.8)

Note that the exponent _2 for Second is encoded in a Church integer type system. This would be simpler using the new literal types feature like libra does.

larsrh commented 7 years ago

Approved! Welcome & please add yourself to the incubator list.