On Dec 10, 2015, at 3:04 PM, Klaus Ostermann <[email protected]> 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 [email protected]. For more options, visit https://groups.google.com/d/optout.
