On Dec 11, 2015, at 6:36 AM, Paolo Giarrusso <p.giarru...@gmail.com> wrote:
> 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? What you want are opaque types and representation independence for existing types. But, in a gradual type system, types are imposed on untyped data representations that (more or less) signal "it's okay if my clients know how I represent my 'stacks' as long as they don't/can't mess them up." In Racket the closest thing to such a protected representation is our generative struct i.e. instances of two distinct evaluations cannot interfere with each other. In Typed Racket we exclude this (so far). If you look at ML, you'll find that datatype is generative, too, at the type phase level. Once the type checker proves that two distinct "evaluations" of a datatype spec type check (in context), their values can't ever co-mingle at run-time and so it is safe to represent them with the *same* bits. In the original ML this is a significant hole in the type system; ML '98 or whatever it was called fixed this problem. -- Matthias -- 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.
