[racket] Typed Racket reactions on developing polymorphic typed array library, and questions

From: Vincent St-Amour (stamourv at ccs.neu.edu)
Date: Tue Aug 24 19:40:53 EDT 2010

At Mon, 23 Aug 2010 17:58:41 -0700,
Neil Toronto wrote:
> It's fun to open the macro stepper and see "unsafe" scattered 
> everywhere, in all the places I expect it. Pretty much every time it's 
> not there is when I expect TR to be able to prove something it can't prove.

Do you have examples besides fixnum operations?

>   - Change (add1 i) into (unsafe-fx+ 1 i), prove it's safe

We're looking into adding a OneLessThanMaxFixnum type that, when used
as argument to add1 gives a return type of Fixnum. That would solve
this problem.

>   - Replace match-define with multiple defines
> 
> For the last, IIRC, on my version of Racket, match-define calls a 
> predicate to ensure the right struct type, but it's redundant in TR. 

Removing predicates made redundant by typechecking in the general case
is on my todo list.

> I had to do the following in my tests and test app:
> 
>   - Use flsqrt, flfloor, flceiling instead of non-fl* versions

sqrt can indeed return a complex number, but if you pass it a
Nonnegative-Float, the result should be a Nonnegative-Float. As for
floor and ceiling, they should already preserve flonum-ness, and as
such should be optimized. Can you send me an example where these could
not be optimized?

>   - Use (* x x) instead of (sqr x)

sqr should give you the right types. However, its type does not
currently express its full behavior wrt the sign of the result. I'll
fix that.

> You'll want to rename it to with-asserts*, I suppose. I think if I were 
> to spend more time on it, I'd make the type-name part optional, and in 
> those cases use pred?'s syntax as a string as the second argument to 
> raise-type-error.

Thanks, I'll add that. We're also thinking of having assert (and thus
with-asserts*) take types as arguments, instead of just predicates.

Vincent
 


Posted on the users mailing list.