[racket] I love TR

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Thu Sep 20 17:27:28 EDT 2012

Are you sure that you blew your entire budget on this email? 

TR is a dependently typed language. While types don't entire values, they depend on those 'aspects' of values (is it a cons? is it a positive value?) that can be checked with (usually cheap) predicates. 




On Sep 20, 2012, at 5:21 PM, John Clements wrote:

> … and I don't mean Teddy Roosevelt.
> 
> TR just discovered a bug that other type systems totally wouldn't have. As a side-benefit, it appears that TR should be able to generate substantially faster code as a result.
> 
> Short synopsis: 
> 
> I have inner-loop code that's using 'modulo'. As it turns out, modulo is slow, because (among other things) it handles cases where the modulus needs to be added or subtracted more than once.  So, I wrote my own. In fact, I specialized my own to the situation where it wrapped down only, because it was being applied to a counter that only got bumped up by 1.
> 
> I found another use of modulo, and pointed it to the same function.
> 
> OOPS! the program doesn't type-check any more. Why? because TR correctly notes that in my other use of the function, it's entirely possible for the index to be less than zero. 
> 
> In principle, any dependent type system should have been able to figure this out. In practice, though, I don't know of any languages that actually support dependent types in this way… er, agda?
> 
> Anyhow, TR just saved me a bunch of debugging time.
> 
> Of course, I just blew it all, writing this e-mail….
> 
> John
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users



Posted on the users mailing list.