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
