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 racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
