Home » forums » LtU Forum

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?

By sciomako at 2013-05-19 22:59 | LtU Forum | previous forum topic | next forum topic | other blogs | 4742 reads

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).

By Sean McDirmid at Mon, 2013-05-20 00:00 | login or register to post comments

"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. ;-)

By raould at Mon, 2013-05-20 19:19 | login or register to post comments

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.

By Douglas McClean at Mon, 2013-05-20 20:35 | login or register to post comments

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.

By Sean McDirmid at Mon, 2013-05-20 23:38 | login or register to post comments

Interesting stuff. Thanks.

Interesting stuff. Thanks.

By sciomako at Mon, 2013-05-20 01:22 | login or register to post comments