Question about Roles and the AMP work

[Richard Eisenberg]

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 <austin at well-typed.com> wrote:

> 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/