Hi, Am Montag, den 08.07.2013, 09:39 +0000 schrieb Simon Peyton-Jones:
| > 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"
Quite right! My mistake was to say "if you CAN do that..." and then discard the evidence that you can do it. What I should have said is
* prove a large bunch of NT constraints (one per constructor field) * then `seq` them * before returning the "ordinary coercion lifting" result.
The thing is, that the "ordinary coercion lifting" is sound (roles permitting -- should check that right off the bat). But we are making a stronger check here, namely that the programmer has exported enough evidence, to expose abstractions.
Although it feels a bit weird to force one set of coercion witnesses (based on datacon field types) and then use another (based on typecon parameters), it could have worked, so I did more work in that direction, but I have hit another obstacle: Just to clarify that we talk about the same things, an easy case: data Family a = Family a a (List a) deriving familyNT :: NT a b -> NT (Family a) (Family b) with "listNT :: NT a b -> NT (List a) (List b)" in scope would get this implementation: familyNT nt = nt `seq` nt `seq` listNT nt `seq` case nt of (NT co -> NT (Family co)) This does ensure that, without breaking abstractions, the user is allowed to convert the arguments of the datacon and produces a sound coercion in in the F_C sense. But what about a simple tree type? data Tree a = Tree a (List (Tree a)) deriving treeNT :: NT a b -> NT (Tree a) (Tree b) I need to force witnesses for * (NT a b) (easy, that is the first argument) and for * (NT (List (Tree a)) (NT (List (Tree b)). The only way to obtain such a witness is to use listNT, which would strictly(!) expect a value of type NT (Tree a) (Tree b), which is what I am trying to produce at the moment, so I cannot simply call treeNT. In this case I can work around it by first creating the final NT value and then use it to create and seq the witnesses required, before returning the result: treeNT nt = let resNT = case nt of (NT co -> NT (Tree co)) in nt `seq` listNT resNT `seq` resNT but this is becoming more and more hacky and inelegant. For example, with mutually recursive data types, I’d have to detect that they are mutually recursive and create similar witnesses in advance for all involved types; for nested recursion I’d have to create multiple witnesses, and who knows what else can happen. From a logical point of view, I’d expect the coercion lifting for a recursive data type to have a type like a ~/C b -> (forall ta tb. (ta ~/C tb -> List ta ~/C List tb)) -> Tree a ~/C Tree b (justified by writing the data type as a fixed point and thinking about fixed-point induction), but its soundness breaks down immediately as the function type -> in the second argument is not total. That’s it for now, 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