> 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.
I don't agree. See, for instance, the "abstraction theorem" from Reynolds. What you say describes the situation in systems with ML-like module systems. In ML, modules are not types because, for various good and bad reasons, there is no such thing as an "instance" of a module. But countless papers on "first class modules" turn modules into types. The simplest example are maybe existential types in System F, which are often used as a form of first-class module (see, e.g., Pierce's TAPL). If I have a value of type T, then T is certainly an abstraction barrier, because all I can do with the value is dictated by T. If T=String, for instance, I cannot multiply the value by 7, even though I could in principle multiply the bit pattern of string. If T=a for some abstract type a, then I can do nothing with the value except to pass it elsewhere (which is one facet of relational parametricity). -- 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.
