On Dec 10, 2015, at 3:04 PM, Klaus Ostermann <klaus...@gmail.com> wrote:
> Thanks for the clarification, Sam. What you write makes sense. > > However, since the default case (without explicit annotations) is that I get > these very (too?) precise singleton types, I have the impression that > reasoning about (typed) program equivalence is more difficult in TR than in > standard statically typed languages. > > Aren't types supposed to be a device for abstraction and for supporting > information hiding? Singleton types seem to be against that spirit by > exposing "implementation details" of the terms, such as the difference > between (- 1 1) and (- 2 2). I don't think gradual/incremental type systems play this role. But it is an open question how we can enrich such type systems with types as abstraction barriers. -- Matthias -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
