[racket] typed racket, filters, and polymorphism

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