> I think interesting conversations could be had about why this problem is harder to model using type systems than other problems are. We can summarize this in

> I think interesting conversations could be had about why this problem is harder to model using type systems than other problems are. We can summarize this in ten seconds: More equations hold between combinations of units than combinations of types constructed using type constructors. For example, m kg m^-1 = kg, but no such relationship exists between (A, (B, A -> R)) and B. Proving these sorts of equivalences adds complexity to type systems.