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 ____________________ Racket Users list: http://lists.racket-lang.org/users
