You may want to read our papers on Units, Harper/Lillibridge and Leroy both from POPL ’94 and chase the citations forward. But perhaps Reynolds’s old saying “type structure is a syntactic discipline for enforcing levels of abstraction” suffices — Matthias (yes, I have studied all of this too and mostly by talking to the people themselves)
> On Dec 10, 2015, at 5:52 PM, Hendrik Boom <[email protected]> wrote: > > 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.
