Dear John,
Although it's not a trivial change for other type systems, I believe
that the natural numbers should be a base type.
Thanks for the example.
-Arthur
==============================================================
Arthur Nunes-Harwitt
Computer Science Department, Rochester Institute of Technology
Room 70-3509
585-475-4916
==============================================================
"I don't know what the language of the future will be
called, but it will look like LISP."
This email is confidential and intended for the named recipient(s). In
the event the email is received by someone other than the recipient,
please notify the sender at a...@cs.rit.edu.
On Thu, 20 Sep 2012, 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
