Hi, to support deriving NT instances properly, TcDeriv needs to be modified. But there are some structural obstacles: So far, all classes which had to be had the “type of interest” as their only type argument. Therefore, DerivSpec, the data structure in that file, carries information about what instances to derive, in the field dc_tc :: TyCon. But with NT it is different: * It has two parameters, * the type of interest is likely not the last parameter (e.g. NT Age Int) * and it can happen that there is a type variable in the last parameter (e.g. NT Int a => NT Age a). All that is difficult to squeeze into the existing data structure. The data type also has the ds_tys :: [Type] parameter, which contains all type parameters to the class (e.g. [Int, a]). So at first I thought about simply removing dc_tc and use the data from (last ds_tys) whenever needed. But in the case of type families, ds_tc is not just the type constructor of (last ds_tys), but rather what it resolves to. So before I rewrite lots of code there, I’d like to get some advice: Should I extend the DerivSpec to support multi-parameter-typeclasses (and figure out how to support data families here), or rather bypass the whole lot and handle NT instance generation separately? Or is there maybe another, more elegant way? Thanks, 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
The more I think about this, the more I wonder if we shouldn't treat NT in a similar way that we treat (~); that is, with built-in rules. The point is, we use (a) roles, and (b) visibility of the data constructor to control abstraction via existence/visibility of the instance. We don't really need a third mechanism (c) the presence or absence of a 'deriving' clause Instead, it can syntactically be a class, but be treateded rather like the SingI class which has an infinite number of instances -- that is, the type checker has a built-in way of simplifying NT constraints. For example, the typechecker simplifies [s] ~ [t] to s ~ t (This is just unification.) Similarly it can simplify NT [s] [t] to NT s t (in a role-aware way, of course). I think this will end up being a lot simpler than trying to push it through the full 'deriving' mechanism. Does that make sense? Simon | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of | Joachim Breitner | Sent: 19 August 2013 15:19 | To: ghc-devs | Subject: Advice about TcDeriv | | Hi, | | to support deriving NT instances properly, TcDeriv needs to be modified. | But there are some structural obstacles: So far, all classes which had | to be had the “type of interest” as their only type argument. Therefore, | DerivSpec, the data structure in that file, carries information about | what instances to derive, in the field dc_tc :: TyCon. | | But with NT it is different: | * It has two parameters, | * the type of interest is likely not the last parameter (e.g. NT Age | Int) | * and it can happen that there is a type variable in the last parameter | (e.g. NT Int a => NT Age a). | All that is difficult to squeeze into the existing data structure. | | The data type also has the ds_tys :: [Type] parameter, which contains | all type parameters to the class (e.g. [Int, a]). So at first I thought | about simply removing dc_tc and use the data from (last ds_tys) whenever | needed. But in the case of type families, ds_tc is not just the type | constructor of (last ds_tys), but rather what it resolves to. | | So before I rewrite lots of code there, I’d like to get some advice: | Should I extend the DerivSpec to support multi-parameter-typeclasses | (and figure out how to support data families here), or rather bypass the | whole lot and handle NT instance generation separately? Or is there | maybe another, more elegant way? | | Thanks, | 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
Good morning, Am Dienstag, den 20.08.2013, 07:24 +0000 schrieb Simon Peyton-Jones:
The more I think about this, the more I wonder if we shouldn't treat NT in a similar way that we treat (~); that is, with built-in rules. The point is, we use (a) roles, and (b) visibility of the data constructor to control abstraction via existence/visibility of the instance. We don't really need a third mechanism (c) the presence or absence of a 'deriving' clause
Instead, it can syntactically be a class, but be treateded rather like the SingI class which has an infinite number of instances -- that is, the type checker has a built-in way of simplifying NT constraints.
For example, the typechecker simplifies [s] ~ [t] to s ~ t (This is just unification.) Similarly it can simplify NT [s] [t] to NT s t (in a role-aware way, of course).
I think this will end up being a lot simpler than trying to push it through the full 'deriving' mechanism.
Does that make sense?
it is certainly true that there are many obstacles when trying to use the normal class mechanisms here. One of the main reason we wanted to use (standalone) deriving instances (or even the NT type constructor idea earlier) was to give library authors a way to communicate their abstractions, to avoid the coercion between (Set Int) and (Set (Down Int)). But thanks to Richard’s role annotation, this can be prevented by annotating the Set’s type variables with @N. So far so good. Questions: * Will this annotation have other, possibly unwanted effects? * 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? * 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). 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
| Questions: | * Will this annotation have other, possibly unwanted effects? The role annotation will have exactly the *right* effect; in particular, it'll prevent you saying class Foo a where foo :: Set a -> Set a instance Foo Int where ... newtype Age = MkAge Int deriving( Foo ) | * 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. | * 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. Simon | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of | Joachim Breitner | Sent: 20 August 2013 08:37 | To: ghc-devs | Subject: Re: Advice about TcDeriv | | Good morning, | | Am Dienstag, den 20.08.2013, 07:24 +0000 schrieb Simon Peyton-Jones: | > The more I think about this, the more I wonder if we shouldn't treat | > NT in a similar way that we treat (~); that is, with built-in rules. | > The point is, we use | > (a) roles, and | > (b) visibility of the data constructor | > to control abstraction via existence/visibility of the instance. We | > don't really need a third mechanism | > (c) the presence or absence of a 'deriving' clause | > | > Instead, it can syntactically be a class, but be treateded rather like | > the SingI class which has an infinite number of instances -- that is, | > the type checker has a built-in way of simplifying NT constraints. | > | > For example, the typechecker simplifies | > [s] ~ [t] | > to | > s ~ t | > (This is just unification.) Similarly it can simplify | > NT [s] [t] | > to | > NT s t | > (in a role-aware way, of course). | > | > I think this will end up being a lot simpler than trying to push it | > through the full 'deriving' mechanism. | > | > Does that make sense? | | it is certainly true that there are many obstacles when trying to use | the normal class mechanisms here. | | One of the main reason we wanted to use (standalone) deriving instances | (or even the NT type constructor idea earlier) was to give library | authors a way to communicate their abstractions, to avoid the coercion | between (Set Int) and (Set (Down Int)). But thanks to Richard’s role | annotation, this can be prevented by annotating the Set’s type variables | with @N. So far so good. | | Questions: | * Will this annotation have other, possibly unwanted effects? | * 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? | * 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). | | 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
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
participants (2)
-
Joachim Breitner -
Simon Peyton-Jones