[racket] typed racket, filters, and polymorphism

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.