Fwd: Question about Roles and the AMP work

Mon May 12 17:46:47 UTC 2014

I'm not familar with the internals of GHC, but maybe it would be possible
for GHC to just use the default definition for `join` in the case that
deriving fails because of roles? At least if the class to be derived has a
`MINIMAL` pragma, GHC could check if that is still satisfied even without
the method that failed to derive, and use the default definition if that's
the case.

2014-05-12 17:28 GMT+02:00 Edward Kmett <ekmett at gmail.com>:

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 <
> simonpj at microsoft.com> wrote:
>
>> 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 at haskell.org] On Behalf Of
>> Austin
>> | Seipp
>> | Sent: 12 May 2014 13:53
>> | To: ghc-devs at 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 at haskell.org
>> | http://www.haskell.org/mailman/listinfo/ghc-devs
>>
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140512/b6f98051/attachment.html>