search

mikeizbicki / subhask

Type safe interface for working in subcategories of Hask
BSD 3-Clause "New" or "Revised" License
418 stars 43 forks source link

Question: Any plans/considerations about working with physical units and the numeric heirarchy #11

Open mvcisback opened 9 years ago

mvcisback commented 9 years ago

Hello,

I've done a decent amount of data analysis/physics calculations in Haskell, and one of the things that has continually frustrated me is trying to get type level units (like in dimensional-tf) to play nicely with libraries that weren't designed for them (automatic differentiations and integrations for example). While I can often rephrase the core calculation in a dimensionless way, sometimes it seems unavoidable.

From what I understand the primary issue is that multiplication of units does not form a monoid w.r.t a type A (m*m : m^2 not m).

Would there be anyway to build in the distinction or mechanism for dealing with this at the type class hierarchy level?

mikeizbicki commented 9 years ago

This is an interesting question that's good for me to think about. The short answer is: not yet, but probably in the future.

The long answer:

Currently, multiplication is supported via the Ring type class, which would not allow what you want for the same reason that the Prelude's Num type class doesn't. This restriction seems pretty important to me because type inference becomes much harder once you generalize the (*) operator.

Matrix multiplication runs into this same issue, and the way around that is to treat every Matrix as a linear function. Then, matrix multiplication is composition in the linear category, i.e. the (.) operator. This gives a pretty natural looking syntax and type inference remains nice.

I suspect something similar might work for units of measure. I haven't thought about this at all before, but here's my first thoughts. Let's say we have the two variables:

a = 5 :: Meter
b = 2 :: Kg

Then multiplication should have a type like:

(*) :: Meter -> Kg -> Meter*Kg

So the question is: what general operation has a type that look like this? One that comes to mind right away is the tensor product. The tensor product in the category Hask is (,) :: a -> b -> (a,b), but since multiplication is linear, we would want the tensor product in the category of linear transformations, which is denoted by (><) in SubHask.

Unfortunately, SubHask doesn't currently have a good notion of tensor products. There's a hack type class at: https://github.com/mikeizbicki/subhask/blob/master/src/SubHask/Algebra.hs#L2129 (the (><) operator is an overspecialized version of the type we want: (><)::v1 -> v2 -> v1><v2). There is a more general version of tensor products for any category is at: https://github.com/mikeizbicki/subhask/blob/master/src/SubHask/Category.hs#L255, but I haven't spent any time thinking about how to make this interface syntactically nice.

The real trick to making this easy to use is to come up with an abstraction that adequately captures the notion of ring multiplication, function composition, and tensor products. That sounds like it's probably doable, but it's not immediately obvious to me how.