On Thu, Dec 10, 2015 at 07:22:40PM -0500, Matthias Felleisen wrote: > > On Dec 10, 2015, at 3:04 PM, Klaus Ostermann <klaus...@gmail.com> 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 don't use types as abstraction barriers. You use modules aas abstraction barriers. And in your module system you specify explicitly how much type information is exported to be used to type-check the module user. Modules are not types. But they can contain type definitions. You an export the type definition, or just the type's presence. -- 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.
