Re: instantiating visible parameters in when deriving instances
Simon, did you meant P2? (Since you can't write instance (k ~ *) => Functor (P1 (a :: k)), as that's ill-kinded). Something like this? data P2 k (a :: k) = MkP2 instance (k ~ *) => Functor (P2 k) That's an interesting idea. Be aware that you actually can't compile that code at the moment, since GHC complains: * Expected kind ‘* -> *’, but ‘P2 k’ has kind ‘k -> *’ * In the first argument of ‘Functor’, namely ‘P2 k’ In the instance declaration for ‘Functor (P2 k)’ I hope this is a bug and not a fundamental limitation. There's another wrinkle in the design we must consider. Not only can datatypes have dependent type parameters, but so can typeclasses themselves. Consider: {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeInType #-} module Cat where import Data.Kind class Cat k (cat :: k -> k -> *) where catId :: cat a a catComp :: cat b c -> cat a b -> cat a c instance Cat * (->) where catId = id catComp = (.) newtype Fun a b = Fun (a -> b) deriving (Cat k) I was surprised to find out that this code currently compiles without issue on GHC 8.0, even though we're deriving (Cat k) instead of (Cat *). This is an effect of the way GHC currently handles deriving clauses, since it unifies the kind of the datatype and typeclass beforehand (therefore, it silently gets unified to Cat * before generating the instance). [1] Is this correct? It definitely feels a bit off. We currently allow this (see Trac #8865 [2]): newtype T a b = MkT (Either a b) deriving ( Category ) Even though Category :: k -> k -> * (i.e., we silently unify k with *). The difference here, as is the difference between P1 and P2 in Simon's email, is that k is not visible, so it's out-of-sight and out-of-mind. When k is visible, as in Cat, when now must be conscious of how it's used in a deriving clause. The Cat code is lying in the sense that we aren't deriving an instance that begins with (Cat k), but rather: instance Cat * Fun where ... Using Simon's advice, we could just as well generate: instance (k ~ *) => Cat k Fun where ... (Again, this doesn't currently compile on 8.0. I really hope that's just a bug.) So I'm starting to lean towards Simon's proposal. That is, we freely unify non-visible type parameters when deriving, but if a type parameter is visible, then we generate equality constraints instead of unifying it. Ryan S. ----- [1] http://git.haskell.org/ghc.git/blob/b0ab8db61568305f50947058fc5573e2382c84eb... [2] https://ghc.haskell.org/trac/ghc/ticket/8865
| So I'm starting to lean towards Simon's proposal. That is, we freely | unify non-visible type parameters when deriving, but if a type | parameter is visible, then we generate equality constraints instead of | unifying it. Why should it make a difference whether it's visible or not. Can't we behave the same for both? Simon | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Ryan | Scott | Sent: 29 March 2016 14:58 | To: ghc-devs@haskell.org | Subject: Re: instantiating visible parameters in when deriving | instances | | Simon, did you meant P2? (Since you can't write instance (k ~ *) => | Functor (P1 (a :: k)), as that's ill-kinded). Something like this? | | data P2 k (a :: k) = MkP2 | instance (k ~ *) => Functor (P2 k) | | That's an interesting idea. Be aware that you actually can't compile | that code at the moment, since GHC complains: | | * Expected kind ‘* -> *’, but ‘P2 k’ has kind ‘k -> *’ | * In the first argument of ‘Functor’, namely ‘P2 k’ | In the instance declaration for ‘Functor (P2 k)’ | | I hope this is a bug and not a fundamental limitation. | | There's another wrinkle in the design we must consider. Not only can | datatypes have dependent type parameters, but so can typeclasses | themselves. Consider: | | {-# LANGUAGE FlexibleInstances #-} | {-# LANGUAGE GeneralizedNewtypeDeriving #-} | {-# LANGUAGE MultiParamTypeClasses #-} | {-# LANGUAGE TypeInType #-} | module Cat where | | import Data.Kind | | class Cat k (cat :: k -> k -> *) where | catId :: cat a a | catComp :: cat b c -> cat a b -> cat a c | | instance Cat * (->) where | catId = id | catComp = (.) | | newtype Fun a b = Fun (a -> b) deriving (Cat k) | | I was surprised to find out that this code currently compiles without | issue on GHC 8.0, even though we're deriving (Cat k) instead of (Cat | *). This is an effect of the way GHC currently handles deriving | clauses, since it unifies the kind of the datatype and typeclass | beforehand (therefore, it silently gets unified to Cat * before | generating the instance). [1] | | Is this correct? It definitely feels a bit off. We currently allow this | (see Trac #8865 [2]): | | newtype T a b = MkT (Either a b) deriving ( Category ) | | Even though Category :: k -> k -> * (i.e., we silently unify k with *). | The difference here, as is the difference between P1 and P2 in Simon's | email, is that k is not visible, so it's out-of-sight and out-of-mind. | When k is visible, as in Cat, when now must be conscious of how it's | used in a deriving clause. | | The Cat code is lying in the sense that we aren't deriving an instance | that begins with (Cat k), but rather: | | instance Cat * Fun where ... | | Using Simon's advice, we could just as well generate: | | instance (k ~ *) => Cat k Fun where ... | | (Again, this doesn't currently compile on 8.0. I really hope that's | just a bug.) | | So I'm starting to lean towards Simon's proposal. That is, we freely | unify non-visible type parameters when deriving, but if a type | parameter is visible, then we generate equality constraints instead of | unifying it. | | Ryan S. | ----- | [1] | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fgit.has | kell.org%2fghc.git%2fblob%2fb0ab8db61568305f50947058fc5573e2382c84eb%3a | %2fcompiler%2ftypecheck%2fTcDeriv.hs%23l653&data=01%7c01%7csimonpj%4006 | 4d.mgd.microsoft.com%7cdd343f6279d74b40a30b08d357da348e%7c72f988bf86f14 | 1af91ab2d7cd011db47%7c1&sdata=I2YgFKCYkZtpSJlN7UzOyawgK2LncTQIlE2PpOAwP | 2c%3d | [2] https://ghc.haskell.org/trac/ghc/ticket/8865 | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.ha | skell.org%2fcgi-bin%2fmailman%2flistinfo%2fghc- | devs%0a&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7cdd343f6279d74 | b40a30b08d357da348e%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=19EhLy | AsemDkPIdmK08C0XBbLufiKEsEwYuLqWhCH3s%3d
Why should it make a difference whether it's visible or not. Can't we behave the same for both?
Oops, I made the wrong distinction. I should have said: we freely
unify eta-reduced type parameters when deriving, but if a type
parameter isn't eta-reduced, then we generate equality constraints
instead of unifying it.
That is, the distinction between
instance Functor P1
-- with -fprint-explicit-kinds, this would be instance Functor * P1
and
instance (k ~ *) => Functor (P2 k)
We can't generate equality constraints for eta-reduced type variables
since there's literally no way to refer to them in an instance.
Ryan S.
On Tue, Mar 29, 2016 at 10:47 AM, Simon Peyton Jones
| So I'm starting to lean towards Simon's proposal. That is, we freely | unify non-visible type parameters when deriving, but if a type | parameter is visible, then we generate equality constraints instead of | unifying it.
Why should it make a difference whether it's visible or not. Can't we behave the same for both?
Simon
| -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Ryan | Scott | Sent: 29 March 2016 14:58 | To: ghc-devs@haskell.org | Subject: Re: instantiating visible parameters in when deriving | instances | | Simon, did you meant P2? (Since you can't write instance (k ~ *) => | Functor (P1 (a :: k)), as that's ill-kinded). Something like this? | | data P2 k (a :: k) = MkP2 | instance (k ~ *) => Functor (P2 k) | | That's an interesting idea. Be aware that you actually can't compile | that code at the moment, since GHC complains: | | * Expected kind ‘* -> *’, but ‘P2 k’ has kind ‘k -> *’ | * In the first argument of ‘Functor’, namely ‘P2 k’ | In the instance declaration for ‘Functor (P2 k)’ | | I hope this is a bug and not a fundamental limitation. | | There's another wrinkle in the design we must consider. Not only can | datatypes have dependent type parameters, but so can typeclasses | themselves. Consider: | | {-# LANGUAGE FlexibleInstances #-} | {-# LANGUAGE GeneralizedNewtypeDeriving #-} | {-# LANGUAGE MultiParamTypeClasses #-} | {-# LANGUAGE TypeInType #-} | module Cat where | | import Data.Kind | | class Cat k (cat :: k -> k -> *) where | catId :: cat a a | catComp :: cat b c -> cat a b -> cat a c | | instance Cat * (->) where | catId = id | catComp = (.) | | newtype Fun a b = Fun (a -> b) deriving (Cat k) | | I was surprised to find out that this code currently compiles without | issue on GHC 8.0, even though we're deriving (Cat k) instead of (Cat | *). This is an effect of the way GHC currently handles deriving | clauses, since it unifies the kind of the datatype and typeclass | beforehand (therefore, it silently gets unified to Cat * before | generating the instance). [1] | | Is this correct? It definitely feels a bit off. We currently allow this | (see Trac #8865 [2]): | | newtype T a b = MkT (Either a b) deriving ( Category ) | | Even though Category :: k -> k -> * (i.e., we silently unify k with *). | The difference here, as is the difference between P1 and P2 in Simon's | email, is that k is not visible, so it's out-of-sight and out-of-mind. | When k is visible, as in Cat, when now must be conscious of how it's | used in a deriving clause. | | The Cat code is lying in the sense that we aren't deriving an instance | that begins with (Cat k), but rather: | | instance Cat * Fun where ... | | Using Simon's advice, we could just as well generate: | | instance (k ~ *) => Cat k Fun where ... | | (Again, this doesn't currently compile on 8.0. I really hope that's | just a bug.) | | So I'm starting to lean towards Simon's proposal. That is, we freely | unify non-visible type parameters when deriving, but if a type | parameter is visible, then we generate equality constraints instead of | unifying it. | | Ryan S. | ----- | [1] | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fgit.has | kell.org%2fghc.git%2fblob%2fb0ab8db61568305f50947058fc5573e2382c84eb%3a | %2fcompiler%2ftypecheck%2fTcDeriv.hs%23l653&data=01%7c01%7csimonpj%4006 | 4d.mgd.microsoft.com%7cdd343f6279d74b40a30b08d357da348e%7c72f988bf86f14 | 1af91ab2d7cd011db47%7c1&sdata=I2YgFKCYkZtpSJlN7UzOyawgK2LncTQIlE2PpOAwP | 2c%3d | [2] https://ghc.haskell.org/trac/ghc/ticket/8865 | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.ha | skell.org%2fcgi-bin%2fmailman%2flistinfo%2fghc- | devs%0a&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7cdd343f6279d74 | b40a30b08d357da348e%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=19EhLy | AsemDkPIdmK08C0XBbLufiKEsEwYuLqWhCH3s%3d
On Mar 29, 2016, at 3:58 PM, Ryan Scott
I hope this is a bug and not a fundamental limitation.
As I posted in the ticket, this is a somewhat fundamental limitation. I qualify by "somewhat" because it's a consequence of a design choice, but reversing the design choice would be rather difficult and lead to several more tough design choices. It's my hope and belief that this restriction will one day be lifted. That day will not be soon. The wiki (https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Liftedvs.Unl...) has some thoughts on the issue, but those notes may be out of date and/or wrong. YMMV. As for Simon's question about the difference between visible and invisible: when the user says `deriving (Cat k)`, the user has written k and presumably means k to be universally quantified. When the user days `deriving Category`, then no `k` has been written and unification seems appropriate. Of course, if we consider that in the `deriving (Cat k)` case, we're just inferring a `k ~ *` constraint, perhaps this is OK. But it's certainly a bit odd. Richard
participants (3)
-
Richard Eisenberg -
Ryan Scott -
Simon Peyton Jones