[racket] I love TR

If these people were serious, they would add a row with industrial impact measured in $100Ms, but that would make their proof assistants look bad because ACL2's value is more than an order of magnitude the addition of all others. 

;; --- 

If these people were serious, Xanadu would get a lot more play. From what I can tell, it is a dependently typed language that worked. (But yes, it has been abandoned.) 



On Sep 20, 2012, at 6:35 PM, Carl Eastlund wrote:

> [possibly off-topic]
> 
> Is it weird to anyone else that the dependent type comparison table, as well as the proof assistant comparison table linked right above it, seem to assume that proof assistants and dependently typed languages are synonymous?  This assumption, for instance, makes ACL2 look absolutely terrible on the proof assistant comparison chart.  Even after I fixed it up to acknowledge that yes, ACL2 does have proof automation, thank you very much.
> 
> Carl Eastlund
> 
> On Thu, Sep 20, 2012 at 5:57 PM, John Clements <clements at brinckerhoff.org> wrote:
> 
> 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
> >>>
> >>
> >
> 
> 
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
> 
>