On Thu, Dec 10, 2015 at 12:04:45PM -0800, Klaus Ostermann 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.
As you go further in setting up more and more powerful type systems, you can eventually get to a system that can be used to rigorously prove program correctness. However, when you go this far, type equivalence becomes an unsolvable problem. To be practical, Racket had to walk the line between infeasiblity and expressiveness. Different people can have very different ideas about where to draw this line. > > Aren't types supposed to be a device for abstraction and for > supporting information hiding? Types and abstraction are orthogonal concepts, which have too often been conflated. Granted, being orthogonal, they work well together. Abstraction is the mechanism for information hiding. -- hendrik -- 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.
