Back to explicit Coercible instances?
Hi, the recent discussion about roles and abstraction lets me wonder whether we should re-evaluate the question of where the Coercible instances come from. Currently, upon use of "coerce", GHC will create Coercible instances out of thin air, as long as the roles agree, and checking some constructor-in-scope invariants. This is troublesome WRT. abstraction. One alternative that was discussed before is explicit Coercible instances. That is, if I write a datatype datatype MyList a = Cons a (MyList a) | MyNil then I have to explicitly write either deriving Coercible to get instance Coercible a b => Coercible (MyList a) (MyList b) or – especially if I want to control which parameters are coercible – have to use standalone deriving and write deriving instance Coercible a b => Coercible (MyList a) (MyList b) For something like Set, the user would not use “deriving Coercible”, but would use deriving instance Coercible a b => Coercible (Set k a) (Set k b) Manual instances of Coercible would be prohibited. The instances are checked for things like: * do the roles allow the behaviour? * are the constructors in scope (for standalone deriving)? * are the arguments of the constructors coercible? The last check ensures that the user cannot break abstraction by wrapping an abstract datatype in a datatype of its own. But note that these instances (between the datacon argument types) are only checked, never actually used! Therefore we must sure that only sound instances exists, and that the user cannot bogus instances (e.g. one with all fields undefined). This would imply a few differences: * Already for syntactical reasons, there will be no instances for coercing constraints. As we have seen, this is a good thing. * Would be no way to use a coercion within the abstraction boundaries, but not outside, because you either have the instance, or you don’t. And assuming GND would simply implement its classes by passing each method through "coerce", this would hopefully also yield a sensible design for GND. 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
I don’t really agree. Here's why: The exact rules you suggest for when "deriving(Coercible)" would be allowed, are the rules we can use for when we need a "from thin air" instance. Moreover, I'm very keen to give a simple, precise answer to the question if s is coercible to t when is (T s) coercible to (T t) I propose that the answer is given by precisely T's roles. At the moment I don't see why we would want to do anything more complicated. But I'm open to being persuaded otherwise Simon | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of | Joachim Breitner | Sent: 12 October 2013 11:52 | To: ghc-devs@haskell.org | Subject: Back to explicit Coercible instances? | | Hi, | | the recent discussion about roles and abstraction lets me wonder | whether | we should re-evaluate the question of where the Coercible instances | come | from. | | Currently, upon use of "coerce", GHC will create Coercible instances | out | of thin air, as long as the roles agree, and checking some | constructor-in-scope invariants. This is troublesome WRT. abstraction. | | One alternative that was discussed before is explicit Coercible | instances. That is, if I write a datatype | datatype MyList a = Cons a (MyList a) | MyNil | then I have to explicitly write either | deriving Coercible | to get | instance Coercible a b => Coercible (MyList a) (MyList b) | or – especially if I want to control which parameters are coercible – | have to use standalone deriving and write | deriving instance Coercible a b => Coercible (MyList a) (MyList | b) | | For something like Set, the user would not use “deriving Coercible”, | but | would use | deriving instance Coercible a b => Coercible (Set k a) (Set k | b) | | Manual instances of Coercible would be prohibited. The instances are | checked for things like: | * do the roles allow the behaviour? | * are the constructors in scope (for standalone deriving)? | * are the arguments of the constructors coercible? | The last check ensures that the user cannot break abstraction by | wrapping an abstract datatype in a datatype of its own. But note that | these instances (between the datacon argument types) are only checked, | never actually used! Therefore we must sure that only sound instances | exists, and that the user cannot bogus instances (e.g. one with all | fields undefined). | | This would imply a few differences: | * Already for syntactical reasons, there will be no instances for | coercing constraints. As we have seen, this is a good thing. | * Would be no way to use a coercion within the abstraction boundaries, | but not outside, because you either have the instance, or you don’t. | | | And assuming GND would simply implement its classes by passing each | method through "coerce", this would hopefully also yield a sensible | design for GND. | | | 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 Samstag, den 12.10.2013, 12:12 +0000 schrieb Simon Peyton-Jones:
The exact rules you suggest for when "deriving(Coercible)" would be allowed, are the rules we can use for when we need a "from thin air" instance.
right! The important difference is that with deriving, only the the type author can use the features, and can decide whether he wants to allow it for his data type or not.
Moreover, I'm very keen to give a simple, precise answer to the question if s is coercible to t when is (T s) coercible to (T t) I propose that the answer is given by precisely T's roles. At the moment I don't see why we would want to do anything more complicated.
I’m not sure if „... if the roles allow it“ is any simpler than „if there is a Coercible instance for it“, and Haskell programmers might be happier if they can think in terms of type class instances without learning a new concept. But you are right: This thread doesn’t really add any thing new; it would just be an alternative way to specify coercability (explicit instances instead of role annotation), which is a bit more familiar to the programmer, possible more flexible (e.g. some library author could make the instance conditional by adding some fancy type-class-hackery constraints), possibly less flexible (no way to talk about coercing types that involve class class constraints). 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
Hello,
On Sat, Oct 12, 2013 at 5:23 AM, Joachim Breitner
Moreover, I'm very keen to give a simple, precise answer to the question if s is coercible to t when is (T s) coercible to (T t) I propose that the answer is given by precisely T's roles. At the moment I don't see why we would want to do anything more complicated.
I’m not sure if „... if the roles allow it“ is any simpler than „if there is a Coercible instance for it“, and Haskell programmers might be happier if they can think in terms of type class instances without learning a new concept.
I like the `deriving Coercible` idea, it seems to fit quite naturally with the rest of the language and does not require programmers to have to know about roles. We'd have to be careful that we use the instances consistently though, in particular, I don't think we can just fall back to using roles behind the scenes, because the class mechanism is more general (unles we restrict it somehow). Here are some examples: data T a = T deriving instance Coercible (T Int) (T Char) deriving instance Coercible (T Int) (T Bool) This allows very precise control, but I don't think that we can express it with roles. Now consider another declaration like this: data S a = S (T a)deriving Coercible Here we'd need some cleverness to determine what instances to derive. Another question is: are the instances going to be automatically symmetric, or would one have to write two versions of each rule? Using the previous example, would I have to also add: deriving instance Coercible (T Char) (T Int) This seems a bit tedious and not in the spirit of `Coercible`. OTOH, if we were to make `Coercable` automatically symmetric, we'd have to make sure that the derived user instances are invertible. Consider for example: deriving instance Eq a => Coercible (T a) (T b) This allows coercing `T Int` to `T (Int -> Int)` but not the other way. All in all, I like the `deriving Coercible` notation, but I think that we should restrict it to something that essentially matches the `role` mechanism under the hood (and get an error saying that we can't derive the instance otherwise). Here is a stab at the rules: * The head of the instance must be of the form: Coercible (T a1 a2 ...) (T b1 b2 ...), where `T` is a concrete type, and the `as` and `bs` are variables. * The only constraints in the context may be of the form `Coercible a1 b1`, or `Coercible a2 b2`, etc... * There can be only one instance derived per type `T` With these restrictions we essentially have another way to specify the roles. The role of the Nts parameter of `T` can be determined like this: role aN bN | aN == bN = Nominal | otherwise = if context has Coercible aN bN then Representational else Phantom Hope this helps, -Iavor
| > Moreover, I'm very keen to give a simple, precise answer to the | question | > if s is coercible to t | > when is (T s) coercible to (T t) | > I propose that the answer is given by precisely T's roles. At the | > moment I don't see why we would want to do anything more complicated. | | I’m not sure if „... if the roles allow it“ is any simpler than „if | there is a Coercible instance for it“, and Haskell programmers might be | happier if they can think in terms of type class instances without | learning a new concept. But it *is* simpler, because given the question can I say 'deriving instance Coercible A B'? the answer involves roles. So by adding this instance stuff you have *two* things to explain instead of one. It might seem that the presence or absence of a 'deriving Coercible' declaration gives you more control, but the *same* control is given by a role annotation. So I'm still not seeing any added value here, though I am seeing added complexity. Simon
participants (3)
-
Iavor Diatchki -
Joachim Breitner -
Simon Peyton-Jones