Moving forall with coerce

[Joachim Breitner]

Hi David,

Am Montag, den 19.10.2015, 18:06 -0400 schrieb Richard Eisenberg:
> Just to be clear, the Codensity bit (which I don't know) is a red
> herring here. What you want is this:
> 
> > newtype A m a = MkA (forall b. m a -> (a -> m b) -> m b)
> > newtype B (m :: * -> *) a = MkB (forall b. (a -> m b) -> m b)
> > 
> > foo :: A m a -> (m a -> B m a)
> > foo = coerce
> 
> On one level, this is perfectly reasonable. These two types do seem
> to have the same runtime representation. But in thinking about how
> the types work out, it's all less clear. In particular, this seems to
> require impredicativity, as we'll be solving a Coercible constraint
> over forall-types. I think we'll have to sort out impredicativity, in
> general, before we can start to tackle something like this.
> 
> But I haven't thought very deeply about it, and perhaps there's a way
> forward I haven't seen.
> 
> Interesting example!

JFTR, note that the solver can handle forall’s in a very limited way,
namely coercing between two forall’ed types works:
    instance (forall a. Coercible t1 t2) => Coercible (forall a. t1) (forall a. t2)
but you need something more powerful.

Also note that once class join the party, things become less coercible.
This might work:
    > newtype A = A (forall x. Int -> [x] -> x)
    > newtype B = B (Int -> forall x. [x] -> x)
    > :t coerce :: A -> B
(although it currently does not), but this will not
    > newtype A = A (forall x. Show x => Int -> [x] -> x)
    > newtype B = B (Int -> forall x. Show x => [x] -> x)
    > coerce :: A -> B
as the order of the Int and the show instance would be different in the
representation. Not sure how much that implementation detail should
pervade the user space.

OTOH, coercible is already quite implementation-specific, and of course
we want to be able to coerce as much as possible.


Greetings,
Joachim
-- 
Joachim “nomeata” Breitner
  mail at joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0xF0FBF51F
  Debian Developer: nomeata at debian.org

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151020/e68cb85a/attachment.sig>