Joachim Discussing with Richard Eisenberg, we wondered the following. · note that the “seq” nonsense is because we allow user-defined NT-values · also note that to determine which NT values we can derive from in-scope NT values, we have to do something very similar to type-class solving. Eg. need NT [T] [S], have available ntList :: forall ab. NT a b -> NT [a] [b], so use ntList to simplify NT [T] [S] to NT T S. Hence the following suggestion: revert from NT as a data value to NT as a class. Thus class NT a b where castNT :: a -> b uncastNT :: b -> a Now when you have a data type you can say “deriving( NT )”, or things like deriving NT a b => NT [a] [b] and expect the usual type-class deriving mechanism to do the job. As usual, you can only do this if you can see the data constructor of the relevant type. Now, you can say things like newtype Age = MkAge Int f :: [Age] -> Int f xs = sum (uncastNT xs) and it’ll work fine. If you omitted the type annotation on f you’d get something like f :: (Num a, NT [a] b) => b -> a which is probably OK. You might worry that instances are not scopeable. Quite right. If you make an NT instance, *everyone* can see it. So don’t make a type an instance of NT unless that’s want. This is not terrible; it just means that you can’t make *local* NT instances, just as you can’t make local Eq instances. This seems to involve a lot less special pleading than before, while still allowing the control you need. For example, for Map you might say deriving instance NT a b => NT (Map k a) (Map k b) The *derived* NT instances would be implemented, just as now, with lifted coercions. You cannot write your own NT instance, just as you can’t write your own Typable instance. That means we don’t need to worry about those bogus instances. Does that make sense? Simon | -----Original Message----- | From: ghc-devs-bounces@haskell.org [mailto:ghc-devs-bounces@haskell.org] On | Behalf Of Joachim Breitner | Sent: 11 July 2013 09:41 | To: ghc-devs@haskell.org | Subject: Re: Exposing newtype coercions to Haskell | | 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