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). -- 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.

