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@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org