On Thu, Dec 10, 2015 at 08:25:11PM -0500, Matthias Felleisen wrote: > > > > On Dec 10, 2015, at 4:47 PM, Hendrik Boom <[email protected]> wrote: > > > > On Thu, Dec 10, 2015 at 07:22:40PM -0500, Matthias Felleisen wrote: > >> > >> On Dec 10, 2015, at 3:04 PM, Klaus Ostermann <[email protected]> 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 > > > > > Yes sir :-)
;-) Maybe that's obvious to you, but there are a lot of people it's not obvious to. And a lot of them have been designing programming languages. -- 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 [email protected]. For more options, visit https://groups.google.com/d/optout.
