On Friday, December 11, 2015 at 1:21:04 AM UTC+1, Matthias Felleisen wrote: > On Dec 10, 2015, at 3:04 PM, 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. > > > > 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
What is the problem there? We've discussed singleton types, but arguably they don't really impede abstraction *in the large* — you just need to upcast your implementation to the intended interface. Ignoring performance problems, TR supports even abstract types — so what's left? I'm not sure that *letting your interface be type-infererred* is safe in any language, though it might work in practice to some extent in some (Haskell?). For Scala, we know from experience it's unsafe even in practice. I agree that upcasting to fix the original example would look silly, but the major point of abstraction is for use in the large anyway, isn't it? -- 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.
