Question about Roles and the AMP work
Hello all, While picking the AMP patch back up, it is almost ready to go, but I got quite a puzzling error when attempting to build 'haskeline' with the AMP changes. I don't seem to remember encountering this error before - but maybe my mind is hazy. The error in question is this: https://gist.github.com/thoughtpolice/6df4c70d8a8fb711b282 The TL;DR is that the move of `join` into base has caused a problem here. The error really speaks for itself: GND tries to derive an instance of `join` for DumbTerm, which would have the type join :: DumbTerm m (DumbTerm m a) -> DumbTerm m a and be equivalent to join for StateT. But this can't hold: DumbTerm should unwrap directly to StateT (by newtype equality) and thus the third parameter to StateT in this case is `DumbTerm m a` if you expand the types - but because this argument is Nominal, it cannot unify with 'PosixT m', which is the actual definition of DumbTerm in the first place! With a little thought, this error actually seems reasonable. But it puzzles me as to what we should do now. One thing we could do is just write the instances manually, of course. But that's a bit annoying. Another alternative (and also unfortunate) change is to leave `join` out of Monad, in which case the GND mechanism is oblivious to it and does not need to worry about deriving these cases. I am not sure how many packages depend on using GND to derive monads like StateT with Nominal arguments, but I imagine it is not totally insignificant and will essentially hurt a lot of people who may use it. Richard, I'm particularly interested to hear what you think. This one sort of snuck up! (NB: despite this, the AMP work is very close to landing in HEAD, at which point we can begin cleaning stuff up faster.) -- Regards, Austin Seipp, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/
This looks a bit awkward to me. Here's a small test case class C m where ret :: a -> m a bind :: m a -> (a -> m b) -> m b join :: m (m a) -> m a newtype T m a = MkT (m a) deriving( C ) This is accepted without the 'join' in the class, but rejected with it. So *all* uses of GND to do 'deriving( Monad )' will break when 'join' is added to Monad. And this is because we don't know that 'm' ranges only over things that have representational arguments; type variables always have nominal arguments. The paper draws attention to this shortcoming, but now it's becoming important. I can't think of an obvious workaround either, except not putting 'join' in Monad. Simon | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Austin | Seipp | Sent: 12 May 2014 13:53 | To: ghc-devs@haskell.org | Subject: Question about Roles and the AMP work | | Hello all, | | While picking the AMP patch back up, it is almost ready to go, but I got | quite a puzzling error when attempting to build 'haskeline' with the AMP | changes. I don't seem to remember encountering this error before - but | maybe my mind is hazy. | | The error in question is this: | | https://gist.github.com/thoughtpolice/6df4c70d8a8fb711b282 | | The TL;DR is that the move of `join` into base has caused a problem | here. The error really speaks for itself: GND tries to derive an | instance of `join` for DumbTerm, which would have the type | | join :: DumbTerm m (DumbTerm m a) -> DumbTerm m a | | and be equivalent to join for StateT. But this can't hold: DumbTerm | should unwrap directly to StateT (by newtype equality) and thus the | third parameter to StateT in this case is `DumbTerm m a` if you expand | the types - but because this argument is Nominal, it cannot unify with | 'PosixT m', which is the actual definition of DumbTerm in the first | place! | | With a little thought, this error actually seems reasonable. But it | puzzles me as to what we should do now. One thing we could do is just | write the instances manually, of course. But that's a bit annoying. | | Another alternative (and also unfortunate) change is to leave `join` out | of Monad, in which case the GND mechanism is oblivious to it and does | not need to worry about deriving these cases. | | I am not sure how many packages depend on using GND to derive monads | like StateT with Nominal arguments, but I imagine it is not totally | insignificant and will essentially hurt a lot of people who may use it. | | Richard, I'm particularly interested to hear what you think. This one | sort of snuck up! | | (NB: despite this, the AMP work is very close to landing in HEAD, at | which point we can begin cleaning stuff up faster.) | | -- | Regards, | | Austin Seipp, Haskell Consultant | Well-Typed LLP, http://www.well-typed.com/ | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://www.haskell.org/mailman/listinfo/ghc-devs
As a straw man, if we went to a typeclass-driven 'next arg is
representational' approach then we could possibly recover 'join' here.
e.g.
class Representational f where
rep :: Coercion f g -> Coercion a b -> Coercion (f a) (g b)
class Representational f => Phantom f where
phantom :: Coercion f g -> Coercion (f a) (g b)
When we look at for the constraint head Coercible (f a) (g b) we'd then
check for Phantom f and if so look for Coercible f g, or fall back to
Representational
f, and look for Coercible f g and Coercible a b.
Then to derive GND for C m it'd need to check Representational m due to the
type of join needing m's next arg to be representational, find it and move
on.
The set of these instances can be left open like any other typeclass and
users could supply their own for tricky conversions if need be.
If you just wrote the existing role annotations, but let them request
currently impossible roles you could use the desired role to infer the
constraints involved.
e.g.
newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }
should be able to derive something like
instance Representational (StateT s)
instance Representational m => Representational (StateT s m)
instance Phantom m => Phantom (StateT s m)
If we put nominal or representational on the m argument
type role StateT nominal nominal nominal
then we could just elide the instances for anything lower in the nominal ->
representational -> phantom lattice than the named role.
The positional argument scheme isn't perfect, as in the above it'd fail to
let you derive `instance Representational StateT` due to the s occurring
under m, an argument later in the argument list, but it does fix most of
the problems with Coercible and monad transfomers.
There might be some fancier form that can cover all of the use cases, but
I'm not seeing it off hand.
-Edward
On Tue, May 13, 2014 at 12:59 AM, Simon Peyton Jones
This looks a bit awkward to me. Here's a small test case
class C m where ret :: a -> m a bind :: m a -> (a -> m b) -> m b join :: m (m a) -> m a
newtype T m a = MkT (m a) deriving( C )
This is accepted without the 'join' in the class, but rejected with it.
So *all* uses of GND to do 'deriving( Monad )' will break when 'join' is added to Monad.
And this is because we don't know that 'm' ranges only over things that have representational arguments; type variables always have nominal arguments. The paper draws attention to this shortcoming, but now it's becoming important.
I can't think of an obvious workaround either, except not putting 'join' in Monad.
Simon
| -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Austin | Seipp | Sent: 12 May 2014 13:53 | To: ghc-devs@haskell.org | Subject: Question about Roles and the AMP work | | Hello all, | | While picking the AMP patch back up, it is almost ready to go, but I got | quite a puzzling error when attempting to build 'haskeline' with the AMP | changes. I don't seem to remember encountering this error before - but | maybe my mind is hazy. | | The error in question is this: | | https://gist.github.com/thoughtpolice/6df4c70d8a8fb711b282 | | The TL;DR is that the move of `join` into base has caused a problem | here. The error really speaks for itself: GND tries to derive an | instance of `join` for DumbTerm, which would have the type | | join :: DumbTerm m (DumbTerm m a) -> DumbTerm m a | | and be equivalent to join for StateT. But this can't hold: DumbTerm | should unwrap directly to StateT (by newtype equality) and thus the | third parameter to StateT in this case is `DumbTerm m a` if you expand | the types - but because this argument is Nominal, it cannot unify with | 'PosixT m', which is the actual definition of DumbTerm in the first | place! | | With a little thought, this error actually seems reasonable. But it | puzzles me as to what we should do now. One thing we could do is just | write the instances manually, of course. But that's a bit annoying. | | Another alternative (and also unfortunate) change is to leave `join` out | of Monad, in which case the GND mechanism is oblivious to it and does | not need to worry about deriving these cases. | | I am not sure how many packages depend on using GND to derive monads | like StateT with Nominal arguments, but I imagine it is not totally | insignificant and will essentially hurt a lot of people who may use it. | | Richard, I'm particularly interested to hear what you think. This one | sort of snuck up! | | (NB: despite this, the AMP work is very close to landing in HEAD, at | which point we can begin cleaning stuff up faster.) | | -- | Regards, | | Austin Seipp, Haskell Consultant | Well-Typed LLP, http://www.well-typed.com/ | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://www.haskell.org/mailman/listinfo/ghc-devs
Yuck yuck yuck -- that's what I think. Austin's analysis below agrees with mine. The error *is* reasonable, because if `coerce` worked in this scenario, a particularly dastardly (and very un-Lawful) Monad instance could break type safety. Furthermore, I think it's absolutely necessary that Monad remain GND'able. It's a common idiom, and I use it myself quite frequently. What to do? Here are some possible ways forward: 1) Implement the second half of roles (as in the original POPL "Generative type abstraction" paper). This would make roles more first-class and allow us to say something like
class Applicative m => Monad (m :: representational -> *) where ...
Under this scenario, all Monad instances would need to be over types with a representational argument, and then `coerce`ing join would be sound. (Actually, we would probably put the representational constraint as a superclass of Functor, but you get the idea.)
There are two downsides to this: a) implementing the much-more complicated role scenario, and b) a GADT could not be a Monad any more. I do actually think (b) would bite some users.
2) Don't put `join` in Monad.
Sorry for asking a perhaps-obvious question, but why put `join` in Monad at all? Are there examples where doing this would increase efficiency?
3) Something along the lines of Edward's suggestion. As he admits, his idea is still incomplete, but I think it would snag a lot of cases. If the current roles machinery works 95% of the time, the current machinery + built-in support for Edward's idea would get 99.5% of real use cases, I would think. It is a little "hackish" and somewhat unprincipled, but I think it would work in practice. I would even have GHC produce the `Representational` instances automatically.
Richard
On May 12, 2014, at 8:53 AM, Austin Seipp
Hello all,
While picking the AMP patch back up, it is almost ready to go, but I got quite a puzzling error when attempting to build 'haskeline' with the AMP changes. I don't seem to remember encountering this error before - but maybe my mind is hazy.
The error in question is this:
https://gist.github.com/thoughtpolice/6df4c70d8a8fb711b282
The TL;DR is that the move of `join` into base has caused a problem here. The error really speaks for itself: GND tries to derive an instance of `join` for DumbTerm, which would have the type
join :: DumbTerm m (DumbTerm m a) -> DumbTerm m a
and be equivalent to join for StateT. But this can't hold: DumbTerm should unwrap directly to StateT (by newtype equality) and thus the third parameter to StateT in this case is `DumbTerm m a` if you expand the types - but because this argument is Nominal, it cannot unify with 'PosixT m', which is the actual definition of DumbTerm in the first place!
With a little thought, this error actually seems reasonable. But it puzzles me as to what we should do now. One thing we could do is just write the instances manually, of course. But that's a bit annoying.
Another alternative (and also unfortunate) change is to leave `join` out of Monad, in which case the GND mechanism is oblivious to it and does not need to worry about deriving these cases.
I am not sure how many packages depend on using GND to derive monads like StateT with Nominal arguments, but I imagine it is not totally insignificant and will essentially hurt a lot of people who may use it.
Richard, I'm particularly interested to hear what you think. This one sort of snuck up!
(NB: despite this, the AMP work is very close to landing in HEAD, at which point we can begin cleaning stuff up faster.)
-- Regards,
Austin Seipp, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/
participants (4)
-
Austin Seipp -
Edward Kmett -
Richard Eisenberg -
Simon Peyton Jones