Exposing newtype coercions to Haskell

[Joachim Breitner]

Hi again,

Am Mittwoch, den 03.07.2013, 10:01 +0200 schrieb Joachim Breitner:
> Am Dienstag, den 02.07.2013, 16:28 +0000 schrieb Simon Peyton-Jones:
> > | I also noticed a problem with my logic for creating the NT-lifting
> > | function.  Suppose
> > |   data C a = MkC (Foo a)
> > | Just having the constructors of C in scope is not sufficient
> > | to safely provide
> > |         NT a b -> NT (C a) (C b)
> > | as the parameters of the constructor might wrap a in another type
> > | constructor, eg
> > |         data Foo a = Foo (Set a)
> > | 
> > | then we certainly don’t want the user to be able to write
> > |         deriving fooNT :: NT a b -> NT (Foo a) (Foo b)
> > 
> > Dually, suppose Foo was an *abstract* type, where we can't see the constructors of Foo.  But the programmer as exported fooNT :: NT a b -> NT (Foo a) (Foo b).  Then we *do* want to be able to derive
> > 	cNT :: NT a b -> NT (C a) (C b)
> > Instead maybe we say
> > 	deriving cNT :: NT a b -> NT (C a) (C b) using( fooNT )
> > listing the imported witnesses that we use.  Or maybe we say simply
> > 	deriving cNT :: NT a b -> NT (C a) (C b) 
> > and magically use any NT-typed things that are in scope.
> 
> Is this really the compiler’s job here? After all, the programmer would
> be able to write
> 
>         deriving cNT' :: NT (Foo a) (Foo b) -> NT (C a) (C b)
>         cNT :: NT a b -> NT (C a) (C b)
>         cNT = cNT' . fooNT
> 
> and expose just cNT to his users, so no expressiveness is lost by not
> providing automatic support here.

Hmm, I notice that this is not fully thought through. A problem is that
on the one hand, the operations we have on newtypes (which allow us to
lift coercions between the _type_ constructor parameters) suggest that
we want
        cNT :: NT a b -> NT (C a) (C b)
while the “do it by hand” intuition suggests that
        cNT :: NT (Foo a) (Foo b) -> NT (C a) (C b)
should be provided. But I only now notice that this function will not be
easily implemented. I guess in this case it could be using NthCo to get
a ~ b from Foo a ~ Foo b, but this is probably shaky.

This tension between the type constructor oriented coercions and data
constructor oriented policy needs a bit more thought.

Greetings,
Joachim

-- 
Joachim “nomeata” Breitner
  mail at joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130704/e4b9c02a/attachment.pgp>