 Using Physical Dimensions
started 2/14/2001; 12:11:04 AM - last post 2/15/2001; 11:47:20 AM
|
|
andrew cooke - Using Physical Dimensions 
2/14/2001; 12:11:04 AM (reads: 2367, responses: 11)
|
|
| Using Physical Dimensions |
|
If you've done physics or engineering you know that dimensions are a useful way of checking calculations - if the answer to a calculation has units of kg then it can't be a velocity.
This paper discusses how to add support for this to statically typed languages (with implementation in ML) so that programs are automatically checked in the same way.
Posted to theory by andrew cooke on 2/14/01; 12:11:34 AM
|
|
|
|
Ehud Lamm - Re: Using Physical Dimensions
2/14/2001; 7:23:48 AM (reads: 1369, responses: 0)
|
|
|
|
pixel - Re: Using Physical Dimensions
2/14/2001; 8:26:49 AM (reads: 1359, responses: 0)
|
|
|
# explanation why a good solution is impossible
You should say "impossible in Ada"!
As far as i understand the Ada solution, it is far from the one proposed in the paper.
|
|
andrew cooke - Re: Using Physical Dimensions
2/14/2001; 8:37:30 AM (reads: 1347, responses: 0)
|
|
|
Although I had heard of the paper before, I posted it here after it was referenced in the Haskell mailing list. I've just worked out how to see that list online and the post is here (earlier I was searching in the haskell list, not haskell-cafe).
Anyway, I posted a note about the Ada papers and got a quick (and fairly frank! :-) reply - as pixel says above, the approach is very different. I guess it will show up here soon.
Apologies if I seem to be playing different people off each other - I was just trying to pass information backwards and forwards while being in the tricky position of not having spent enough time on the paper to understand it...
|
|
Ehud Lamm - Re: Using Physical Dimensions
2/14/2001; 10:31:44 AM (reads: 1337, responses: 0)
|
|
|
Indeed, I should have emphesized the fact that the discussion I linked was about implementing a solution in Ada. I was mearly giving another data point. I don't have any personal feelings about this issue. I just thought seeing another treatment may be interesting.
Didn't mean to cause confusion.
|
|
Ehud Lamm - Re: Using Physical Dimensions
2/14/2001; 10:57:08 AM (reads: 1338, responses: 0)
|
|
|
To be more specific: The interesting thing is what this teaches us about type systems. Ada's type system is fairly rich compared to most imperative languages (esp. if you take into acount generic units, and tagged types - and their interaction). However, it is fairly primitive to type systems commonly found in functional languages. I didn't really study this issue in any detail, so I can not pinpoint the technical features that are crucial for this application. Can anyone elaborate?
|
|
andrew cooke - Re: Using Physical Dimensions
2/14/2001; 12:45:48 PM (reads: 1353, responses: 0)
|
|
|
There's now a response here that suggests that parametric polymorphism over dimensions is necessary.
|
|
Ehud Lamm - Re: Using Physical Dimensions
2/14/2001; 2:23:41 PM (reads: 1349, responses: 0)
|
|
|
I hope I am not the one bad-mouthed in the message you point to. I just gave some pointers, not having really thought about any of this mysefl in any detail. It is just not really the sort of thing I am interested in, so I don't have any solid views on this.
Saying parametric polym is crucial is not saying much. It solves problems that are not specific to the units problem (if I understand what the poster wants to say.
One thing I agree with: better read the papers...
|
|
pixel - Re: Using Physical Dimensions
2/14/2001; 5:55:15 PM (reads: 1353, responses: 0)
|
|
|
As for me, i find it quite nice. More static analysis is always nice :)
I wonder if a language has exception inference? aka infere the exceptions a function throws and ensure you don't try to catch an exception not thrown and can verify the exceptions a function throws (recursively). That is a soft version of Java exception declarations in methods prototype.
And do you know any other static analysis?
|
|
Chris Rathman - Re: Using Physical Dimensions
2/14/2001; 8:30:26 PM (reads: 1352, responses: 0)
|
|
And do you know any other static analysis? Well, there's always the potential to statically verify that the terms of the contract (in a language that supports DbC). :-)
|
|
andrew cooke - Re: Using Physical Dimensions
2/15/2001; 12:08:52 AM (reads: 1336, responses: 0)
|
|
|
I hope I am not the one bad-mouthed in the message you point to
I think it was the original author, but it wasn't clear. Made me uncomfortable (see earlier post) too.
|
|
pixel - Re: Using Physical Dimensions
2/15/2001; 11:47:20 AM (reads: 1311, responses: 0)
|
|
|
As far as i know, statically verifying the terms of the contract is not decidable :-/
The B formal method's purpose is this
|
|
|
|