Exposing newtype coercions to Haskell

[Joachim Breitner]

Hi,

Am Freitag, den 05.07.2013, 08:10 +0000 schrieb Simon Peyton-Jones:
> Re passing bottoms, read "Equality proofs and deferred type errors".
> http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/
> The NT type here is playing the role of (~) in that paper. Just as (~)
> wraps (~#), so NT will wrap (NT#), and it'll play out exactly in the
> paper.  So I'm not bothered about bottoms.

I still am. Let’s have a look at your example:

> Suppose we have a data type 
> 	data T a b = T1 (S a b) (R b)
> where we have in scope
> 	ntS :: NT p p' -> NT q q' -> NT (S p q) (S p' q')
> but R is completely abstract.  Now, is it safe to say
> 	deriving ntT :: NT a a' -> NT (T a b) (T a' b)
> 
> Well, our criterion is whether we can write by hand, a function
> 	foo :: NT a a' -> T a b -> T a' b
> 
> Let's try:
> 	foo g (T1 s r) = T1 (cast s g1) (cast r g2)
>           where
>             g1 :: NT (S a b) (S a' b)
>             g1 = ntS g refl
> 
> 	    g2 :: NT (R b) (R b)
> 	    g2 = refl
> 
> So the general plan is, for each constructor argument of type ty, see
> if you can build a suitable NT value (g1, g2 in the above example),
> using either built-in stuff like refl, or arguments like (g :: NT a
> a'), or in-scope NT values like ntS.
> 
> If you CAN do that, then it's ok (internally) to use ordinary coercion
> lifting, roughly
> 	ntT g = T g refl
> The above per-constructor-arg testing is just to make sure that all
> the relevant witnesses are in scope, to preserve abstraction.  It's
> not for soundness.

I understand the approach, but I think it is insufficient. Assume that
the user wants to cheat for some reason and has this definition for ntS,
clearly writable without having access to S’s internals:

ntS :: NT p p' -> NT q q' -> NT (S p q) (S p' q')
ntS _ _ = error "nah nah"

Then the above check succeeds: You can write the function foo, it would
type check and would, at runtime, throw an exception. But the deriving
mechanism can’t predict that, so it would generate the code "ntT g = T g
refl" _which does not use ntS at all_, suddenly allowing a coecion that
breaks the abstraction.

From what I can tell it works in "Equality proofs and deferred type
errors" because the ~ values are actually used (pattern-matched) in the
Core code and bottoms cause the program to fail at the right points.



Hence my gut feeling that there is something fishy about the existing
coercion rule

         a ~/C a'   b ~/C' b'
         –––––––––––––––––––––
         (T a b) ~/C (T a' b')
        
(which is probably fine for ~/T – I’m currently focusing on the “types
have same representation equality ~/C”) instead of the more
construction-guided rule

     S a b ~/C S a' b'   R b ~/C' R b'
     –––––––––––––––––––––––––––––––––
            (T a b) ~/C (T a' b')

which would ensure that I’d have to actually call ntS and pattern match
the resulting ntS call in the deriving code for ntT, avoiding the
problem shown above.


Maybe (without claiming that I understand the problem fully) these
coercion rules would make the role system obsolete? These problems occur
with GADTs and type families, right? An example for the former would be
        
        data G a where ABool :: G Bool

for which "a ~/C b -> G a ~/C G b" is not ok. But this data type
declaration becomes, in Core, simply

        data G a where ABool :: a ~/T Bool -> G a
        
and by the datatype coercion schema hinted at above the rule would
become

        (a ~/T Bool) ~/C (b ~/T Bool) -> G a ~/C G b.
        
Assuming there is no way to do a ~/C coercion between ~/T witnesses the
bad coercion would be prevented. Refl could still be used there if G has
multiple type parameters and others are ok to coerce.

Similar for type families: A type family "F a" in a data constructor
parameter causes a "F a ~/C F b" requirement to appear which would then
prevent the bad coercion, or restrict it to cases where "F a" and "F b"
indeed to have the same representation.



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/ghc-devs/attachments/20130707/8888e968/attachment.pgp>