On Sep 20, 2012, at 2:27 PM, Matthias Felleisen wrote: > > > 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.
There's a key missing word in the second sentence of the second paragraph… I
think I understand what you're saying.
Based on my tiny definition of dependent types ("types that depend on values"),
TR doesn't look like it has dependent types (e.g. forall n . numbers less than
n), but then again, staged compilation and modules may throw the definition of
dependent types into a cocked hat, if I can extend the type system as part of
an earlier phase.
Tell me how confused I am, on a scale of 1-10 :).
John
PS: if TR really is dependently typed, then it should appear in the table on
this page:
http://en.wikipedia.org/wiki/Dependent_type
I'm not quite sure what you'd put for "Program Extraction", though :).
>
>
>
>
> 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
>
smime.p7s
Description: S/MIME cryptographic signature
____________________ Racket Users list: http://lists.racket-lang.org/users
