[racket] typed racket, filters, and polymorphism

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.hinsen at 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