Hi, Am Dienstag, den 20.08.2013, 07:43 +0000 schrieb Simon Peyton-Jones:
| Questions: | * Will this annotation have other, possibly unwanted effects?
The role annotation will have exactly the *right* effect;
great.
| * Should we also simplify constraints like (NT Age a) to (NT Int a) | automatically and built-in, or do we still want the user to first tell | us that we should do so?
I think we should automatically simplify it.
ok, so in summary the user will never see instance declarations referring to NT in any way, but just one function castNT :: NT a b => a -> b which will just do the right thing (or nothing at all).
| * What about the “only do it if constructors are in scope” idea – if | the typechecker creates these instances on the fly, it might do so for | modules where the constructors are not in scope (either because they are | private, or simply because they have not been imported).
It'll simplify (NT Age a) to (NT Int a) when, and only when, MkAge is in scope. So visibility of the data constructor says just when you want that instance to work. I think that seems fine to me.
I’m a bit uneasy about this; it means that one cannot export the ability to do these casts without exposing everything. Also it leads to a surprising behavior with regard to import lists: Consider a module M which wants to use "castNT :: T -> [Int]" where newtype T = T [Age]" is defined elsewhere. For this to work, I not only have to "import ... (T(T))", but also "import ... (Age(MkAge))", even though I don’t see anything about Age in my code. Also, the typechecker will have to register a use of all these constructors during typechecking – is there precedence for that? I guess we can start with this more restricted, but definitely safe variant and see how much it hinders practical use. Greetings, Joachim -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org