Dimensional Analysis in real world and Type Systems

I'm not sure I know what I'm talking about...

Isn't dimensional analysis used in natural science a kind of type checking? If so, doesn't it mean Curry–Howard isomorphism is applicable and, therefore, dimensional analysis is simply theorem proofing?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Many languages support

Many languages support extensions for dimensional unit type checking. For example, see Andrew Kennedy's work on F#. I'm not sure about your theoretical question, but I'm sure someone has asked and answered it before (perhaps you can find an answer in Andrew's work).

"many"?!?!?

uh... i can't say i've seen an over-abundance of existing units code for main-stream languages, let alone well-designed, well-implemented ones! whenever i get into a conversation about these things the only 2 i can ever come up with are F# and Frink. it isn't like java, c#, c++ have it. ocaml apparently has, like, 1 that somebody home-grew? (there are probably 10 different incompatible weird-ass such modules for haskell, though. ;-)

Haskell

You are pretty much right on about the situation in Haskell. I only know of 3, at least one of which is pretty good.

The whole Haskell story around this kind of thing will get a lot nicer, in my opinion, once this GHC ticket is completely finished and everyone can stop rolling their own type level naturals.

I meant in research, this is

I meant in research, this is not an uncommon topic. If we are talking about production, then definitely there aren't many systems that have made it that far.

Interesting stuff. Thanks.

Interesting stuff. Thanks.