On Sep 20, 2012, at 2:49 PM, Matthias Felleisen wrote: > > Duplicating the row for Sage looks fine :-)
Hope you weren't joking: http://en.wikipedia.org/wiki/Dependent_type#Comparison On a related note, someone should probably add a more prominent section on TR in the Racket wikipedia page. Right now it gets about half a sentence…. John Clements > > > 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 >>> >> >
smime.p7s
Description: S/MIME cryptographic signature
____________________ Racket Users list: http://lists.racket-lang.org/users
