Whoops, sorry: this is the same thing Konrad was talking about! Duh. Well, hopefully the link is useful.
Robby On Mon, Sep 29, 2014 at 9:32 AM, Robby Findler <ro...@eecs.northwestern.edu> wrote: > Just in case, here is one piece of related work from the PL world and > is probably a reasonable starting point for finding others' attempts > at this problem: > > http://research.microsoft.com/en-us/um/people/akenn/units/ > > Robby > > > On Mon, Sep 29, 2014 at 3:44 AM, Konrad Hinsen > <konrad.hin...@fastmail.net> wrote: >> Matthias Felleisen writes: >> >> > Your message points out where gradual typing badly fails. >> >> Not just gradual typing. I am not aware of any good unit >> implementation in any type system, with the exception of F# and Frink >> whose type systems were explicitly modified to add unit checking as a >> special case. Dependent types should permit a good solution, but I >> haven't seen it done yet. >> >> The reason you need dependent types is that the product of two >> measures is another measure with a new unit, so you must be able to >> construct new types (representing units) from values. For example, a >> length divided by a time yields a speed. Once you can do that, scaling >> a unit (e.g. from meters to kilometers) becomes a special case. >> >> > In this specific case, you have two aspects of dimensionality: >> > dimension per se (I am sure there is a word for it) and the chosen >> > unit to represent it. >> >> The two terms used for this distinction are in fact "dimension" and >> "unit". >> >> > If someone writes (area-of-rectangle 1 [mm] 1 [km]), there is >> > nothing wrong with it -- except that the type checker should insert >> > a coercion from mm to m and from km to m (multiplying/dividing by >> > 1,000). >> >> That's a topic of hot debate in the scientific computing community. >> Some argue that the type checker should consider your example as an >> error, and not do any implicit conversion. The motivation is that the >> expression you used is more likely to be a mistake than the meaningful >> use of expressive language, since best practices recommend to use a >> minimal set of units inside any piece of code. >> >> Anyway, that's a minor detail. If your type system can handle >> automatic conversion, then it can also handle its absence. >> >> >> Alexander D. Knauth writes: >> >> > What I had in mind was for the structs to be available at run-time, >> > but that ideally the optimizer could take them out for the >> > intermediate operations and put them back for the final result. >> >> You are actually adding a very Racket-specific requirement to the >> already difficult units-as-types problem: the interplay between a >> typed and an untyped dialect of the same language. I agree this would >> be nice to have. >> >> Konrad. >> ____________________ >> Racket Users list: >> http://lists.racket-lang.org/users ____________________ Racket Users list: http://lists.racket-lang.org/users
