Duplicating the row for Sage looks fine :-)
On Sep 20, 2012, at 5:38 PM, John Clements wrote:
>
> 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
>>
>
____________________
Racket Users list:
http://lists.racket-lang.org/users
