RE: Exposing newtype coercions to Haskell
(Narrowing to ghc-devs.) 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. 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. (There is some "role" stuff to take account of there, which Richard is working on, but to a first approximation that's it I think.) Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell- | users-bounces@haskell.org] On Behalf Of Joachim Breitner | Sent: 04 July 2013 14:30 | To: glasgow-haskell-users@haskell.org | Subject: Re: Exposing newtype coercions to Haskell | | Hi, | | small update: I generalized the code at | https://github.com/nomeata/nt-coerce/blob/9349dd3/GHC/NT/Plugin.hs | a bit, it is now able to handle to create NT-values for unwarpping | arbitrary newtypes and for lifting across type constructors. It does so | unconditionally, i.e. does _not_ yet check whether the constructors are | in scope and whether the user is allowed to cast the types occurring in | the data constructors. | | So what works is this: | | NT values for newtypes without or with type arguments, and possibly | recursive: | | newtype Age = Age Int deriving Show | ageNT :: NT Age Int | ageNT = deriveThisNT -- temporary syntax for deriving | listNT ... | | newtype MyList a = MyList [a] deriving Show | myListNT :: NT (MyList a) [a] | myListNT = deriveThisNT | | newtype R a = R [R a] deriving Show | rNT :: NT (R a) [R a] | rNT = deriveThisNT | | | NT values for type constructors, replacinge all or some of the type | parameters: | | listNT :: NT a b -> NT [a] [b] | listNT = deriveThisNT | | myListNT' :: NT a b -> NT (MyList a) (MyList b) | myListNT' = deriveThisNT | | data F a b c = F a b c deriving Show | fNT :: NT a a' -> NT (F a b c) (F a' b c) | fNT = deriveThisNT | | | What does not work is creating a NT value between a newtype and its | representation if type arguments change on the way, e.g. | | bar :: NT (MyList Age) [Int] | | but the user can construct that himself: | | bar = myListNT' ageNT `trans` myListNT | | | | The next step would be to add the safeguards about the visibility of | constructors and about the types of data constructor parameters. | Especially the latter is still not clear to me: For example with | | data Foo a = Foo (Bar a) | | is it really sufficient to check whether a "barNT:: NT a b -> NT (Bar a) | (Bar b)" exists? After all, I would not need barNT in the generated | implementation of fooNT, so the user could “provide” this value via | undefined and nobody would notice. | | I get the feeling that already the typing rule for TyConAppCo should | expect coercions between the actual types in the data constructors | rather than just between the type constructor parameters, so that the | implementation barNT would actually have to use fooNT. Maybe that would | simplify the two-equalities-approach. But that is just an uneducated gut | feeling. | | | BTW: Is this still on-topic on glasgow-haskell-users or should I move to | ghc-dev? | | | 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
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
| > 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. Simon
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
Hi, despite my issues with recursive data types, I continued with the implementation. I now added the check if the data type arguments can safely be coerced. I do not scan what is in scope for NT values to use, but rather expect the progammer to promise the required witness when he uses "deriving" and the plug the functions together by himself: https://github.com/nomeata/nt-coerce/blob/ec9b5/tests/LiftAbstract.hs I also added a test suite to show what works already: https://github.com/nomeata/nt-coerce/tree/master/tests what does rightfully not work, due to abstraction: https://github.com/nomeata/nt-coerce/tree/master/tests/failing and what does not yet work, although it conceivably should: https://github.com/nomeata/nt-coerce/tree/master/tests/todo The test suite contains expected output in *.out and *.err, so you can check out what happens without having to run it. The error messages are not yet as nice as they should be. How to proceed from here Is this approach and design good enough to to into GHC, despite not being able to handle _all_ cases where it conceivably could, and the slight unwieldiness when coerctions for data types based on abstract data types? BTW, I find it quite nice to be able to develop such a feature without touching GHC’s source. If that is possible for more contributions, the entry barrier to GHC would be noticeably lowered. Thanks, 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
POPLing today. Let's discuss on Monday | -----Original Message----- | From: ghc-devs-bounces@haskell.org [mailto:ghc-devs-bounces@haskell.org] | On Behalf Of Joachim Breitner | Sent: 11 July 2013 15:25 | To: ghc-devs@haskell.org | Subject: Re: Exposing newtype coercions to Haskell | | Hi, | | despite my issues with recursive data types, I continued with the | implementation. | | I now added the check if the data type arguments can safely be coerced. | I do not scan what is in scope for NT values to use, but rather expect | the progammer to promise the required witness when he uses "deriving" | and the plug the functions together by himself: | https://github.com/nomeata/nt-coerce/blob/ec9b5/tests/LiftAbstract.hs | | I also added a test suite to show what works already: | https://github.com/nomeata/nt-coerce/tree/master/tests | what does rightfully not work, due to abstraction: | https://github.com/nomeata/nt-coerce/tree/master/tests/failing | and what does not yet work, although it conceivably should: | https://github.com/nomeata/nt-coerce/tree/master/tests/todo | | The test suite contains expected output in *.out and *.err, so you can | check out what happens without having to run it. The error messages are | not yet as nice as they should be. | | How to proceed from here Is this approach and design good enough to to | into GHC, despite not being able to handle _all_ cases where it | conceivably could, and the slight unwieldiness when coerctions for data | types based on abstract data types? | | BTW, I find it quite nice to be able to develop such a feature without | touching GHC’s source. If that is possible for more contributions, the | entry barrier to GHC would be noticeably lowered. | | Thanks, | 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
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
Hi, Am Montag, den 15.07.2013, 21:57 +0000 schrieb Simon Peyton-Jones:
· note that the “seq” nonsense is because we allow user-defined NT-values
Are you saying that seq is nonsense? Or that are you just telling me why we need seq?
· 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.
Yes, as discussed.
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
We’ve discussed this proposal before. The only problem with it is that it will not allow the author of a type container which should be abstract to cast it in internal code; if that is ok then type classes are definitely the nicer way. I assume that the “real” NT class will be abstract and castNT/uncastNT exposed as normal functions, not class methods, so that the user does not create custom instances, right?
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.
The thing is that I don’t need local Eq instances; I can just call my local private myCustomEq. But I cannot create a local private coercion. I guess one can argue that if someone has such special needs, he will be able to figure out when to use unsafeCoerce, and just let them play in the rough outsides. So the missing feature can at least functionally approximated (just as it can be now).
Does that make sense?
Nothing new here besides the point that the feature „private, unexposed NT coercions“ do not warrant the extra overhead of introducing new syntax and replicating the deriving feature on the function level, and I’ll take that point. I guess it doesn’t change the implementation a lot, although I probably can’t implement that in a plugin any more. Although it would actually be a useful thing if code for deriving new type classes can be added in a plugin :-) So I’ll soon start implementing that. 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
| Are you saying that seq is nonsense? Or that are you just telling me why | we need seq? No, no, just that all those seqs are big nuisance -- and one caused solely by the fact that users could (in effect) write bogus instances. If they can't, the issue doesn't arise. | We’ve discussed this proposal before. The only problem with it is that | it will not allow the author of a type container which should be | abstract to cast it in internal code; if that is ok then type classes | are definitely the nicer way. OK. The whole story is *so* much simpler if we piggy back on type classes that I think that's a much better way to go. OK, so you can't do "deep casting" of internal data types without exposing the ability to "deep cast" to clients. But we have no convincing examples of such a need. Let's do the simple thing. | I guess it doesn’t change the implementation a lot Oh I think it does change it a LOT. No more hunting through all the in-scope identifier for ones whose type finish with ".... -> NT t1 t2". No new syntax. No new type-class-like deduction algorithm. It all just plays out through the existing type class machinery. | Although it would actually be | a useful thing if code for deriving new type classes can be added in a | plugin :-) Indeed. One answer is "generics". Another is to have a mechanism for a front-end plugin. But let's not bend this feature out of shape to serve that goal. Better to design a better plugin mechanism. Simon
Hi, Am Dienstag, den 16.07.2013, 07:54 +0000 schrieb Simon Peyton-Jones:
| I guess it doesn’t change the implementation a lot
Oh I think it does change it a LOT. No more hunting through all the in-scope identifier for ones whose type finish with ".... -> NT t1 t2". No new syntax. No new type-class-like deduction algorithm. It all just plays out through the existing type class machinery.
Ok, I was referring here to what I have done so far, which is mostly the code that traverses the type and assembles the ~/C witness, which will still be required. Greetings, Joachim -- Joachim Breitner e-Mail: mail@joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata@joachim-breitner.de
Hi, as discussed, I started to work basing the newtype coercions on classes instead of types. I poked around the code, especially TcDeriv.lhs, and I have a few questions: For my current design I wanted to have class IsNT a where type Concrete a coercion :: a ~# Concrete a but that does not work, as methods seem to need to have a boxed type. Using "a ~ Concrete a" does not work as well, as that has kind Constraint. So I wrapped ~# myself and created: data NT a b = NT ((~#) a b) class IsNT a where type Concrete a coercion :: NT a (Concrete a) with only IsNT (I’ll think more about the name ;-)) and probably Concrete exposed; not or coercion. The interface would then be functions castNT :: IsNT a => Concrete a -> a uncastNT :: IsNT a => a -> Concrete a Now we want the user to be able to specify deriving instance IsNT Age -- with Concrete Age = Int deriving instance IsNT a => IsNT [a] -- with Concrete [a] = [Concrete a] deriving instance IsNT v => IsNT (Map k v) -- dito and probably also deriving instance IsNT Int -- with Concrete Int = Int for all non-newtypes. After adding the definitions to ghc-prim and extending PrelNames I tried to make the deriving code, starting with the last examle (IsNT Int). There, the generated code should be something like instance IsNT Int where type Concrete Int = Int coercion = NT (refl Int) But here I am stuck: The deriving code mechanism expects me to give the method definitions as HsExpr, but I’d like to generate Core here. How can I achieve that, or what other options do I have? (Of course this will need further adjustments when Richard’s role code is in.) (If there is a reason to go back to the two parameter type class "NT a b", no problem, but the problem of HsExpr vs. CoreExpr would still remain.) 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
Hi Joachim, A few responses to your plan: - I think you *do* want HsExprs not CoreExprs. Though I haven't worked much in TcDeriv myself, I imagine everything uses HsExprs so that they can be type-checked. This allows nice error messages to be reported at the site of a user's "deriving instance IsNT ...". - The type that you've called NT below will soon exist in base, in the module Data.Type.Equality. See http://ghc.haskell.org/trac/ghc/wiki/TypeLevelReasoning That implementation ran into a little bump this morning, but it should be pushed within 24 hours. - But, there's a wrinkle here. The (~#) type, along with (~) and (:=:) (the last is from the soon-to-be Data.Type.Equality), all work over so-called *nominal* coercions. (Nominal coercions correspond to the "C" coercions from this paper: http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf I hope to have an implementation of the ideas in that paper available later this week. There are some user-facing features, about which there will be wiki page some point quite soon.) A nominal coercion should only exist between two types that are nominally equal. Under this definition Age and Int are not nominally equal, because they have different names. The other interesting equality is "representational". This equality considers Age and Int to be representationally equal, because they have the same representation. A key point of newtype coercions is that they work over representational equality, not only nominal equality. Working over representational equality is what makes them interesting and useful. Currently, there is no way to abstract over representational coercions -- that is, there is no way to store one, say in a GADT or other Haskelly data type. Of course, a data structure within GHC can store a representational coercion; you just can't have one be the payload of an Id, say. So, that means that the implementation of newtype coercions may have to be a little more magical than the design you're writing. Or, it's possible that we could add abstraction over representational coercions, but I prefer the magical approach, because I don't see a general need for the ability to abstract. Now that I think of it, you may need to generalize the deriving mechanism a bit. All current "deriving"s generate code that the user could write. (Typeable is something of an exception here.) Here, the generated code is something that a user can not write. Maybe that's why you wanted CoreExprs in the first place! Somewhat separately: - I prefer the two-parameter class over a one-parameter, as it seems more flexible. If the two-parameter version (without any dependencies between the two parameters) hinders type inference, users can define an explicitly-typed wrapper. Why do I want this flexibility? Because, once roles are done, the following should be possible:
data Foo a = MkFoo deriving instance IsNT (Foo a) (Foo b)
Note that `a` is a phantom parameter here, and, yes, I meant `data` there, not newtype. In other news, I would prefer the name not to mention newtypes, because I think the mechanism is somewhat stronger than just newtype coercions. Richard On 2013-07-22 13:06, Joachim Breitner wrote:
Hi,
as discussed, I started to work basing the newtype coercions on classes instead of types. I poked around the code, especially TcDeriv.lhs, and I have a few questions:
For my current design I wanted to have
class IsNT a where type Concrete a coercion :: a ~# Concrete a
but that does not work, as methods seem to need to have a boxed type. Using "a ~ Concrete a" does not work as well, as that has kind Constraint. So I wrapped ~# myself and created:
data NT a b = NT ((~#) a b) class IsNT a where type Concrete a coercion :: NT a (Concrete a)
with only IsNT (I’ll think more about the name ;-)) and probably Concrete exposed; not or coercion. The interface would then be functions
castNT :: IsNT a => Concrete a -> a uncastNT :: IsNT a => a -> Concrete a
Now we want the user to be able to specify
deriving instance IsNT Age -- with Concrete Age = Int deriving instance IsNT a => IsNT [a] -- with Concrete [a] = [Concrete a] deriving instance IsNT v => IsNT (Map k v) -- dito and probably also deriving instance IsNT Int -- with Concrete Int = Int for all non-newtypes.
After adding the definitions to ghc-prim and extending PrelNames I tried to make the deriving code, starting with the last examle (IsNT Int). There, the generated code should be something like
instance IsNT Int where type Concrete Int = Int coercion = NT (refl Int)
But here I am stuck: The deriving code mechanism expects me to give the method definitions as HsExpr, but I’d like to generate Core here. How can I achieve that, or what other options do I have?
(Of course this will need further adjustments when Richard’s role code is in.)
(If there is a reason to go back to the two parameter type class "NT a b", no problem, but the problem of HsExpr vs. CoreExpr would still remain.)
Greetings, Joachim
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
| - But, there's a wrinkle here. The (~#) type, along with (~) and (:=:) | (the last is from the soon-to-be Data.Type.Equality), all work over | so-called *nominal* coercions. (Nominal coercions correspond to the "C" | coercions from this paper: Excellent point, Richard. Running example deriving instance (NT a b) => NT [a] [b] The whole point of what Joachim is studying is making it possible for the programmer to generate representational equalities, and use them with ntCast. ntCast :: NT a b -> a -> b (I'm ignoring the question about the final names for things.) So we can't use the new (:=:) type because it wraps nominal equality. To work with the approach Joachim sketches we'd need: data REq a b where REq :: (a ~R# b) -> NT a b which wraps a *representational* equality. But as you say, we weren't planning to abstract over representational equalities at all in FC, so that would bring up a range of questions. One possible response is that we *should* allow abstraction over ~R; there's nothing wrong with it in principle, it's just that we didn't think it was necessary. The main cost is that we'd need an unboxed type constructor ~R# (to match the existing ~# which is really nominal equalty ~N#), and a boxed one (called NT above) to match (:=:). So the above instance declaration would somehow generate ntList :: REq a b -> REq [a] [b] ntList (REq (c :: a ~R# b)) = REq ([c] :: [a] ~R# [b]) You mention a "magical" approach, but I'm not sure what that is. The question of how to represent all this in HsSyn, to communicate between TcDeriv and TcInstDcls, is a somewhat separate matter. We can solve that in several ways. But first we need be sure what the FC story is. My instinct is for a 2-param type class. For 'newtype Age = MkAge Int', it seems odd to have both the newtype axiom axiom ax4 : Age ~ Int and a type family axiom axiom ax5 Concrete Age ~ Int Simon A nominal coercion should only | exist between two types that are nominally equal. Under this definition | Age and Int are not nominally equal, because they have different names. | The other interesting equality is "representational". This equality | considers Age and Int to be representationally equal, because they have | the same representation. A key point of newtype coercions is that they | work over representational equality, not only nominal equality. Working | over representational equality is what makes them interesting and | useful. Currently, there is no way to abstract over representational | coercions -- that is, there | is no way to store one, say in a GADT or other Haskelly data type. Of | course, a data structure within GHC can store a representational | coercion; you just can't have one be the payload of an Id, say. So, that | means that the implementation of newtype coercions may have to be a | little more magical than the design you're writing. Or, it's possible | that we could add abstraction over representational coercions, but I | prefer the magical approach, because I don't see a general need for the | ability to abstract. | | Now that I think of it, you may need to generalize the deriving | mechanism a bit. All current "deriving"s generate code that the user | could write. (Typeable is something of an exception here.) Here, the | generated code is something that a user can not write. Maybe that's why | you wanted CoreExprs in the first place! | | Somewhat separately: | | - I prefer the two-parameter class over a one-parameter, as it seems | more flexible. If the two-parameter version (without any dependencies | between the two parameters) hinders type inference, users can define an | explicitly-typed wrapper. Why do I want this flexibility? Because, once | roles are done, the following should be possible: | | > data Foo a = MkFoo | > deriving instance IsNT (Foo a) (Foo b) | | Note that `a` is a phantom parameter here, and, yes, I meant `data` | there, not newtype. In other news, I would prefer the name not to | mention newtypes, because I think the mechanism is somewhat stronger | than just newtype coercions. | | Richard | | On 2013-07-22 13:06, Joachim Breitner wrote: | > Hi, | > | > as discussed, I started to work basing the newtype coercions on classes | > instead of types. I poked around the code, especially TcDeriv.lhs, and | > I | > have a few questions: | > | > For my current design I wanted to have | > | > class IsNT a where | > type Concrete a | > coercion :: a ~# Concrete a | > | > but that does not work, as methods seem to need to have a boxed type. | > Using "a ~ Concrete a" does not work as well, as that has kind | > Constraint. So I wrapped ~# myself and created: | > | > data NT a b = NT ((~#) a b) | > class IsNT a where | > type Concrete a | > coercion :: NT a (Concrete a) | > | > with only IsNT (I’ll think more about the name ;-)) and probably | > Concrete exposed; not or coercion. The interface would then be | > functions | > | > castNT :: IsNT a => Concrete a -> a | > uncastNT :: IsNT a => a -> Concrete a | > | > Now we want the user to be able to specify | > | > deriving instance IsNT Age -- with Concrete Age = Int | > deriving instance IsNT a => IsNT [a] -- with Concrete [a] = | > [Concrete a] | > deriving instance IsNT v => IsNT (Map k v) -- dito | > and probably also | > deriving instance IsNT Int -- with Concrete Int = Int | > for all non-newtypes. | > | > After adding the definitions to ghc-prim and extending PrelNames I | > tried | > to make the deriving code, starting with the last examle (IsNT Int). | > There, the generated code should be something like | > | > instance IsNT Int where | > type Concrete Int = Int | > coercion = NT (refl Int) | > | > But here I am stuck: The deriving code mechanism expects me to give the | > method definitions as HsExpr, but I’d like to generate Core here. How | > can I achieve that, or what other options do I have? | > | > (Of course this will need further adjustments when Richard’s role code | > is in.) | > | > (If there is a reason to go back to the two parameter type class "NT a | > b", no problem, but the problem of HsExpr vs. CoreExpr would still | > remain.) | > | > Greetings, | > Joachim | > | > _______________________________________________ | > ghc-devs mailing list | > ghc-devs@haskell.org | > http://www.haskell.org/mailman/listinfo/ghc-devs | | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://www.haskell.org/mailman/listinfo/ghc-devs
Hi Richard and Simon, thanks for your detailed notes. Am Montag, den 22.07.2013, 17:01 +0100 schrieb Richard Eisenberg:
- I think you *do* want HsExprs not CoreExprs. Though I haven't worked much in TcDeriv myself, I imagine everything uses HsExprs so that they can be type-checked. This allows nice error messages to be reported at the site of a user's "deriving instance IsNT ...".
My plan was to make all checks (constructors in scope; IsNT classes for all data constructor arguments present) in TcDeriv, so you get nice error messages. If it turns out that the actual coercion can only be generated in a later pass, then it the checks just need to be strong enough to make that pass always succeed.
- But, there's a wrinkle here. The (~#) type, along with (~) and (:=:) (the last is from the soon-to-be Data.Type.Equality), all work over so-called *nominal* coercions.
I know; I was just using them until representational equality is in and plan to switch then.
(Nominal coercions correspond to the "C" coercions from this paper)
I got confused by C and T in my previous mails. In any case, I am only concerned with representational equality (T, it seems) for this project.
Or, it's possible that we could add abstraction over representational coercions, but I prefer the magical approach, because I don't see a general need for the ability to abstract.
Hmm, I must admit I was assuming that once the roles implementation is in there will be ~# and ~#/T (or ~R#, which is a less-easy-to-confuse moniker) available in Core.
Now that I think of it, you may need to generalize the deriving mechanism a bit. All current "deriving"s generate code that the user could write. (Typeable is something of an exception here.) Here, the generated code is something that a user can not write. Maybe that's why you wanted CoreExprs in the first place!
Exactly. But it is also the reason why we are aiming for deriving classes (and not NT values), because it is already an established way of having the compiler generate code for you.
- I prefer the two-parameter class over a one-parameter, as it seems more flexible.
Thanks for spotting the phantom type replacing example, which is a features I’d also like to have. The type family was just a quick idea (and it would be neat to be able to ask GHCi via ":kind! (Concrete t)" what t looks like with all newtypes unfolded), but it’s not worth the loss of flexibility. In some cases, the type family might require less type annotations. Consider newtype Age = Age Int newtype NT1 = NT1 Int newtype NT2 = NT2 Int myCast :: Either NT1 Age -> Either NT2 Age myCast = castNT . uncastNT With two parameters, GHC will not know whether it should cast via "Either Int Age" or "Either Int Int", while with a type family there will be only one choice, "Concrete (Either NT1 Age) = Either Int Int". In general, castNT . uncastNT would have the nice type castNT . uncastNT :: Concrete a ~ Concrete b => a -> b which plainly expresses „Cast between any to values who have the same concrete representation.“. Just as a side remark in case this comes up later again. BTW, what should the base-case be? I believe most user-friendly is a least-specific class instance IsNT a a so that the cast "Either Age a -> Either Int a" is possible. Or are overlapping instances too bad and the user should derive instances for all non-container non-newtype types himself: instance IsNT Int Int .... Am Dienstag, den 23.07.2013, 05:23 +0000 schrieb Simon Peyton-Jones:
The question of how to represent all this in HsSyn, to communicate between TcDeriv and TcInstDcls, is a somewhat separate matter. We can solve that in several ways. But first we need be sure what the FC story is.
For now what I am doing is that in TcDeriv, I am implementing the method with a value "unfinishedNTInstance :: a" which I am then replacing in a always-run simplCore pass with the real implementation in Core. It is a work-around that lets me explore the design-space and implementation issues without having to rewire GHC. 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
A few responses: - As Simon said, there is no great reason we don't have ~R# in Core. It's just that we looked through GHC and, without newtype coercions, there is no need for ~R#, so we opted not to include it. I'm still not convinced we need it for newtype coercions, though. What if we have this in Core?
class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a } NTCo:Age :: Age ~R# Int -- see [1] NTAgeInst :: NT Age Int NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT = \(x :: Int). x |> sym NTCo:Age }
[1]: We still do have representational coercions, even though it would be bogus to extract their type, as the type constructor ~R# does not exist. But, coercionKind, which returns the two coerced types, and the new coercionRole (which would return Representational in this case) work just fine. Here, we don't need to abstract over ~R#, by just referring to the global axiom directly. Does this compose well? I think so; you'll just have to inline all of the coercions. But, the coercions won't ever get too big, as they will always mirror exactly the structure of the types being coerced. Simon, this is the sort of "magic" I was thinking of, magical because I can't imagine a way this could be produced from an HsExpr. Also, nice example of how the one-parameter design might aid the programmer. I think that thinking about the base case is also productive, but I don't have a clear enough opinion to express on that front. Richard On 2013-07-23 08:21, Joachim Breitner wrote:
Hi Richard and Simon,
thanks for your detailed notes.
Am Montag, den 22.07.2013, 17:01 +0100 schrieb Richard Eisenberg:
- I think you *do* want HsExprs not CoreExprs. Though I haven't worked much in TcDeriv myself, I imagine everything uses HsExprs so that they can be type-checked. This allows nice error messages to be reported at the site of a user's "deriving instance IsNT ...".
My plan was to make all checks (constructors in scope; IsNT classes for all data constructor arguments present) in TcDeriv, so you get nice error messages. If it turns out that the actual coercion can only be generated in a later pass, then it the checks just need to be strong enough to make that pass always succeed.
- But, there's a wrinkle here. The (~#) type, along with (~) and (:=:) (the last is from the soon-to-be Data.Type.Equality), all work over so-called *nominal* coercions.
I know; I was just using them until representational equality is in and plan to switch then.
(Nominal coercions correspond to the "C" coercions from this paper)
I got confused by C and T in my previous mails. In any case, I am only concerned with representational equality (T, it seems) for this project.
Or, it's possible that we could add abstraction over representational coercions, but I prefer the magical approach, because I don't see a general need for the ability to abstract.
Hmm, I must admit I was assuming that once the roles implementation is in there will be ~# and ~#/T (or ~R#, which is a less-easy-to-confuse moniker) available in Core.
Now that I think of it, you may need to generalize the deriving mechanism a bit. All current "deriving"s generate code that the user could write. (Typeable is something of an exception here.) Here, the generated code is something that a user can not write. Maybe that's why you wanted CoreExprs in the first place!
Exactly. But it is also the reason why we are aiming for deriving classes (and not NT values), because it is already an established way of having the compiler generate code for you.
- I prefer the two-parameter class over a one-parameter, as it seems more flexible.
Thanks for spotting the phantom type replacing example, which is a features I’d also like to have. The type family was just a quick idea (and it would be neat to be able to ask GHCi via ":kind! (Concrete t)" what t looks like with all newtypes unfolded), but it’s not worth the loss of flexibility.
In some cases, the type family might require less type annotations. Consider newtype Age = Age Int newtype NT1 = NT1 Int newtype NT2 = NT2 Int
myCast :: Either NT1 Age -> Either NT2 Age myCast = castNT . uncastNT
With two parameters, GHC will not know whether it should cast via "Either Int Age" or "Either Int Int", while with a type family there will be only one choice, "Concrete (Either NT1 Age) = Either Int Int". In general, castNT . uncastNT would have the nice type castNT . uncastNT :: Concrete a ~ Concrete b => a -> b which plainly expresses „Cast between any to values who have the same concrete representation.“. Just as a side remark in case this comes up later again.
BTW, what should the base-case be? I believe most user-friendly is a least-specific class instance IsNT a a so that the cast "Either Age a -> Either Int a" is possible. Or are overlapping instances too bad and the user should derive instances for all non-container non-newtype types himself: instance IsNT Int Int ....
Am Dienstag, den 23.07.2013, 05:23 +0000 schrieb Simon Peyton-Jones:
The question of how to represent all this in HsSyn, to communicate between TcDeriv and TcInstDcls, is a somewhat separate matter. We can solve that in several ways. But first we need be sure what the FC story is.
For now what I am doing is that in TcDeriv, I am implementing the method with a value "unfinishedNTInstance :: a" which I am then replacing in a always-run simplCore pass with the real implementation in Core. It is a work-around that lets me explore the design-space and implementation issues without having to rewire GHC.
Greetings, Joachim
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Hi, Am Dienstag, den 23.07.2013, 09:51 +0100 schrieb Richard Eisenberg:
A few responses:
- As Simon said, there is no great reason we don't have ~R# in Core. It's just that we looked through GHC and, without newtype coercions, there is no need for ~R#, so we opted not to include it. I'm still not convinced we need it for newtype coercions, though. What if we have this in Core?
class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a } NTCo:Age :: Age ~R# Int -- see [1] NTAgeInst :: NT Age Int NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT = \(x :: Int). x |> sym NTCo:Age }
I thought about this class definition, and it is has the nice property that we can actually implement the methods by hand (without the zero-cost of course), which would be a good lint-like check that we do not generate illegal instances. The problem is that It it would not allow deriving instance NT a b => NT [a] [b] as there is no way to extract the coercion that was used in the implementation of NT a b. Hence the need to expose (to Core, not to tue user) the coercion in the class: The cast operations do not compose well. 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
You're right, of course. I'm now thinking we really do need ~R# to make this work. That's annoying, but not technically difficult. I'll continue to think about this. Richard On 2013-07-23 10:00, Joachim Breitner wrote:
Hi,
Am Dienstag, den 23.07.2013, 09:51 +0100 schrieb Richard Eisenberg:
A few responses:
- As Simon said, there is no great reason we don't have ~R# in Core. It's just that we looked through GHC and, without newtype coercions, there is no need for ~R#, so we opted not to include it. I'm still not convinced we need it for newtype coercions, though. What if we have this in Core?
class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a } NTCo:Age :: Age ~R# Int -- see [1] NTAgeInst :: NT Age Int NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT = \(x :: Int). x |> sym NTCo:Age }
I thought about this class definition, and it is has the nice property that we can actually implement the methods by hand (without the zero-cost of course), which would be a good lint-like check that we do not generate illegal instances. The problem is that It it would not allow deriving instance NT a b => NT [a] [b] as there is no way to extract the coercion that was used in the implementation of NT a b. Hence the need to expose (to Core, not to tue user) the coercion in the class: The cast operations do not compose well.
Greetings, Joachim
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
Hi, Am Dienstag, den 23.07.2013, 09:51 +0100 schrieb Richard Eisenberg:
I think that thinking about the base case is also productive, but I don't have a clear enough opinion to express on that front.
and it seems to tricky; Here we are hitting problems that we did not have with the non-class-approach. tl;dr: "IsNT a a" only works with IncoherentInstances, which are in principle fine for this class (it is univalent in a sense), but requiring this extension would be quite unfortunate. Consider this ghci session (this already works here): Prelude GHC.NT> newtype Age = Age Int deriving Show Prelude GHC.NT> deriving instance IsNT Int Age Prelude GHC.NT> castNT (1::Int) :: Age -- good, works Age 1 Prelude GHC.NT> deriving instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b') Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Age -- also works Left (Age 1) Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Int -- does not work yet <interactive>:12:1: No instance for (IsNT Int Int) arising from a use of ‛castNT’ In the expression: castNT (Left 1 :: Either Int Int) :: Either Age Int In an equation for ‛it’: it = castNT (Left 1 :: Either Int Int) :: Either Age Int Prelude GHC.NT> deriving instance IsNT Int Int Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Int -- works now Left (Age 1) Prelude GHC.NT> :t castNT :: (Either Int Int) -> (Either Age Int) castNT :: (Either Int Int) -> (Either Age Int) :: Either Int Int -> Either Age Int But we are not able to cast such that one type parameter changes while leaving another type _variable_ untouched: Prelude GHC.NT> :t castNT :: (Either Int a) -> (Either Age a) <interactive>:1:1: No instance for (IsNT a1 a1) arising from a use of ‛castNT’ Possible fix: add (IsNT a1 a1) to the context of an expression type signature: Either Int a1 -> Either Age a1 or the inferred type of it :: Either Int a -> Either Age a In the expression: castNT :: (Either Int a) -> (Either Age a) and if we add "IsNT a a" as a base case: Prelude GHC.NT> instance IsNT a a <interactive>:34:10: Warning: No explicit method or default declaration for ‛coercion’ In the instance declaration for ‛IsNT a a’ we get Prelude GHC.NT> :t castNT :: (Either Int a) -> (Either Age a) <interactive>:1:1: Overlapping instances for IsNT a1 a1 arising from a use of ‛castNT’ Matching instances: instance [overlap ok] IsNT a a -- Defined at <interactive>:34:10 instance IsNT Int Int -- Defined at <interactive>:13:1 instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b') -- Defined at <interactive>:10:1 (The choice depends on the instantiation of ‛a1’ To pick the first instance above, use -XIncoherentInstances when compiling the other instance declarations) In the expression: castNT :: (Either Int a) -> (Either Age a) Re-doing the session with -XIncoherentInstances set helps, but requiring that for every module that wants to derive a IsNT class is probably not nice. The one-parameter-variant does not help either. One way to avoid the issue is to have two instances for Either: Prelude GHC.NT> deriving instance (IsNT a a') => IsNT (Either a b) (Either a' b) Prelude GHC.NT> deriving instance (IsNT b b') => IsNT (Either a b) (Either a b') This still requires OverlappingInstances, but I can get the desired cast without IncoherentInstances: Prelude GHC.NT> :t castNT :: Either Int a -> Either Age a castNT :: Either Int a -> Either Age a :: Either Int a -> Either Age a Other casts that should be “normal” are more complicated now: Prelude GHC.NT> let c = (castNT :: Either Age Int -> Either Age Age) . (castNT :: Either Int Int -> Either Age Int) Prelude GHC.NT> :t c c :: Either Int Int -> Either Age Age Prelude GHC.NT> c (Left 1) Left (Age 1) In any case, the whole thing needs a bit more massaging until it becomes sufficiently elegant. Greetings, Joachim -- Joachim Breitner e-Mail: mail@joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata@joachim-breitner.de
If you add -XIncoherentInstances *just to the module that has instance IsNT a a*, then it'll work fine I think. This says "pick this instance even though an instantiation of the constraint might match a more specific instance". You don't need the flag in importing modules. I think that's fine. For the IsNT class, where users cannot define their own instances, it really is not incoherent to pick the IsNT a a instance. The operational effect is always a no-op. In short, I think this'll work fine. Simon | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Joachim | Breitner | Sent: 23 July 2013 12:45 | To: ghc-devs@haskell.org | Subject: Re: Exposing newtype coercions to Haskell | | Hi, | | Am Dienstag, den 23.07.2013, 09:51 +0100 schrieb Richard Eisenberg: | > I think that thinking about the base case is also | > productive, but I don't have a clear enough opinion to express on that | > front. | | and it seems to tricky; Here we are hitting problems that we did not | have with the non-class-approach. | | tl;dr: "IsNT a a" only works with IncoherentInstances, which are in | principle fine for this class (it is univalent in a sense), but | requiring this extension would be quite unfortunate. | | | Consider this ghci session (this already works here): | | Prelude GHC.NT> newtype Age = Age Int deriving Show | Prelude GHC.NT> deriving instance IsNT Int Age | Prelude GHC.NT> castNT (1::Int) :: Age -- good, works | Age 1 | Prelude GHC.NT> deriving instance (IsNT a a', IsNT b b') => IsNT (Either a b) | (Either a' b') | Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Age -- also works | Left (Age 1) | Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Int -- does not work | yet | | <interactive>:12:1: | No instance for (IsNT Int Int) arising from a use of ‛castNT’ | In the expression: | castNT (Left 1 :: Either Int Int) :: Either Age Int | In an equation for ‛it’: | it = castNT (Left 1 :: Either Int Int) :: Either Age Int | Prelude GHC.NT> deriving instance IsNT Int Int | Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Int -- works now | Left (Age 1) | Prelude GHC.NT> :t castNT :: (Either Int Int) -> (Either Age Int) | castNT :: (Either Int Int) -> (Either Age Int) :: Either Int Int -> Either Age Int | | But we are not able to cast such that one type parameter changes while | leaving another type _variable_ untouched: | | Prelude GHC.NT> :t castNT :: (Either Int a) -> (Either Age a) | | <interactive>:1:1: | No instance for (IsNT a1 a1) arising from a use of ‛castNT’ | Possible fix: | add (IsNT a1 a1) to the context of | an expression type signature: Either Int a1 -> Either Age a1 | or the inferred type of it :: Either Int a -> Either Age a | In the expression: castNT :: (Either Int a) -> (Either Age a) | | and if we add "IsNT a a" as a base case: | | Prelude GHC.NT> instance IsNT a a | | <interactive>:34:10: Warning: | No explicit method or default declaration for ‛coercion’ | In the instance declaration for ‛IsNT a a’ | | we get | | Prelude GHC.NT> :t castNT :: (Either Int a) -> (Either Age a) | | <interactive>:1:1: | Overlapping instances for IsNT a1 a1 arising from a use of ‛castNT’ | Matching instances: | instance [overlap ok] IsNT a a -- Defined at <interactive>:34:10 | instance IsNT Int Int -- Defined at <interactive>:13:1 | instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b') | -- Defined at <interactive>:10:1 | (The choice depends on the instantiation of ‛a1’ | To pick the first instance above, use -XIncoherentInstances | when compiling the other instance declarations) | In the expression: castNT :: (Either Int a) -> (Either Age a) | | | Re-doing the session with -XIncoherentInstances set helps, but requiring | that for every module that wants to derive a IsNT class is probably not | nice. | | | The one-parameter-variant does not help either. | | | One way to avoid the issue is to have two instances for Either: | | Prelude GHC.NT> deriving instance (IsNT a a') => IsNT (Either a b) (Either a' b) | Prelude GHC.NT> deriving instance (IsNT b b') => IsNT (Either a b) (Either a b') | | This still requires OverlappingInstances, but I can get the desired cast | without IncoherentInstances: | | Prelude GHC.NT> :t castNT :: Either Int a -> Either Age a | castNT :: Either Int a -> Either Age a | :: Either Int a -> Either Age a | | Other casts that should be “normal” are more complicated now: | | Prelude GHC.NT> let c = (castNT :: Either Age Int -> Either Age Age) . (castNT :: | Either Int Int -> Either Age Int) | Prelude GHC.NT> :t c | c :: Either Int Int -> Either Age Age | Prelude GHC.NT> c (Left 1) | Left (Age 1) | | | | In any case, the whole thing needs a bit more massaging until it becomes | sufficiently elegant. | | Greetings, | Joachim | | -- | Joachim Breitner | e-Mail: mail@joachim-breitner.de | Homepage: http://www.joachim-breitner.de | ICQ#: 74513189 | Jabber-ID: nomeata@joachim-breitner.de
Hi, Am Dienstag, den 23.07.2013, 18:58 +0000 schrieb Simon Peyton-Jones:
If you add -XIncoherentInstances *just to the module that has instance IsNT a a*, then it'll work fine I think. This says "pick this instance even though an instantiation of the constraint might match a more specific instance". You don't need the flag in importing modules.
That does not seem to be the case: Enabling the flag just for the special "IsNT a a" instance does not work: Prelude GHC.NT> :t castNT :: (Either Int a) -> (Either Age a) <interactive>:1:1: Overlapping instances for IsNT a1 a1 arising from a use of ‛castNT’ Matching instances: instance [incoherent] IsNT a a -- Defined at <interactive>:12:10 instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b') -- Defined at <interactive>:7:1 (The choice depends on the instantiation of ‛a1’ To pick the first instance above, use -XIncoherentInstances when compiling the other instance declarations) In the expression: castNT :: (Either Int a) -> (Either Age a) (as correctly specified by the error message.) But now the solution is easy to see: When deriving IsNT, simply set the incoherent flag for every instance, independent of any active pragmas. 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
Hi Joachim, As discussed previously, I do think we need a way to store representational coercions. In my roles branch (which is getting close to pushing, I believe), I have created eqReprPrimTyCon, which is like eqPrimTyCon, but it is the type of coercions witnessing representational equality. The Id stored in a CoVarCo can usefully have a type headed by eqReprPrimTyCon. If you're really eager to take a look, I use github to coordinate among computers; you can see the roles branch at github.com/goldfirere/ghc. Richard On Jul 24, 2013, at 8:31 AM, Joachim Breitner wrote:
Hi,
Am Dienstag, den 23.07.2013, 18:58 +0000 schrieb Simon Peyton-Jones:
If you add -XIncoherentInstances *just to the module that has instance IsNT a a*, then it'll work fine I think. This says "pick this instance even though an instantiation of the constraint might match a more specific instance". You don't need the flag in importing modules.
That does not seem to be the case: Enabling the flag just for the special "IsNT a a" instance does not work:
Prelude GHC.NT> :t castNT :: (Either Int a) -> (Either Age a)
<interactive>:1:1: Overlapping instances for IsNT a1 a1 arising from a use of ‛castNT’ Matching instances: instance [incoherent] IsNT a a -- Defined at <interactive>:12:10 instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b') -- Defined at <interactive>:7:1 (The choice depends on the instantiation of ‛a1’ To pick the first instance above, use -XIncoherentInstances when compiling the other instance declarations) In the expression: castNT :: (Either Int a) -> (Either Age a)
(as correctly specified by the error message.)
But now the solution is easy to see: When deriving IsNT, simply set the incoherent flag for every instance, independent of any active pragmas.
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
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
I thought about the design you suggest below, but rejected it because I don't see how to do lifting -- which is really the whole point! In particular, what are you going to write for ntList :: NT a b -> NT [a] [b] ntList (MkNT castNT uncastNT) = MkNT ??? ??? For lists you could write (fmap castNT), but the whole point of this exercise is not to write that -- and the type might not be an instance of Functor. I'm thinking we need (~R#) as a type constructor. Simon | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Richard | Eisenberg | Sent: 23 July 2013 09:51 | To: Joachim Breitner | Cc: ghc-devs@haskell.org | Subject: Re: Exposing newtype coercions to Haskell | | A few responses: | | - As Simon said, there is no great reason we don't have ~R# in Core. | It's just that we looked through GHC and, without newtype coercions, | there is no need for ~R#, so we opted not to include it. I'm still not | convinced we need it for newtype coercions, though. What if we have this | in Core? | | > class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a } | > NTCo:Age :: Age ~R# Int -- see [1] | > NTAgeInst :: NT Age Int | > NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT = \(x | > :: Int). x |> sym NTCo:Age } | | [1]: We still do have representational coercions, even though it would | be bogus to extract their type, as the type constructor ~R# does not | exist. But, coercionKind, which returns the two coerced types, and the | new coercionRole (which would return Representational in this case) work | just fine. | | Here, we don't need to abstract over ~R#, by just referring to the | global axiom directly. Does this compose well? I think so; you'll just | have to inline all of the coercions. But, the coercions won't ever get | too big, as they will always mirror exactly the structure of the types | being coerced. Simon, this is the sort of "magic" I was thinking of, | magical because I can't imagine a way this could be produced from an | HsExpr. | | Also, nice example of how the one-parameter design might aid the | programmer. I think that thinking about the base case is also | productive, but I don't have a clear enough opinion to express on that | front. | | Richard | | On 2013-07-23 08:21, Joachim Breitner wrote: | > Hi Richard and Simon, | > | > thanks for your detailed notes. | > | > Am Montag, den 22.07.2013, 17:01 +0100 schrieb Richard Eisenberg: | > | >> - I think you *do* want HsExprs not CoreExprs. Though I haven't worked | >> much in TcDeriv myself, I imagine everything uses HsExprs so that they | >> can be type-checked. This allows nice error messages to be reported at | >> the site of a user's "deriving instance IsNT ...". | > | > My plan was to make all checks (constructors in scope; IsNT classes for | > all data constructor arguments present) in TcDeriv, so you get nice | > error messages. If it turns out that the actual coercion can only be | > generated in a later pass, then it the checks just need to be strong | > enough to make that pass always succeed. | > | >> - But, there's a wrinkle here. The (~#) type, along with (~) and (:=:) | >> (the last is from the soon-to-be Data.Type.Equality), all work over | >> so-called *nominal* coercions. | > | > I know; I was just using them until representational equality is in and | > plan to switch then. | > | >> (Nominal coercions correspond to the "C" coercions from this paper) | > | > I got confused by C and T in my previous mails. In any case, I am only | > concerned with representational equality (T, it seems) for this | > project. | > | >> Or, it's possible | >> that we could add abstraction over representational coercions, but I | >> prefer the magical approach, because I don't see a general need for | >> the | >> ability to abstract. | > | > Hmm, I must admit I was assuming that once the roles implementation is | > in there will be ~# and ~#/T (or ~R#, which is a less-easy-to-confuse | > moniker) available in Core. | > | > | >> Now that I think of it, you may need to generalize the deriving | >> mechanism a bit. All current "deriving"s generate code that the user | >> could write. (Typeable is something of an exception here.) Here, the | >> generated code is something that a user can not write. Maybe that's | >> why | >> you wanted CoreExprs in the first place! | > | > Exactly. But it is also the reason why we are aiming for deriving | > classes (and not NT values), because it is already an established way | > of | > having the compiler generate code for you. | > | > | >> - I prefer the two-parameter class over a one-parameter, as it seems | >> more flexible. | > | > Thanks for spotting the phantom type replacing example, which is a | > features I’d also like to have. The type family was just a quick idea | > (and it would be neat to be able to ask GHCi via ":kind! (Concrete t)" | > what t looks like with all newtypes unfolded), but it’s not worth the | > loss of flexibility. | > | > | > In some cases, the type family might require less type annotations. | > Consider | > newtype Age = Age Int | > newtype NT1 = NT1 Int | > newtype NT2 = NT2 Int | > | > myCast :: Either NT1 Age -> Either NT2 Age | > myCast = castNT . uncastNT | > | > With two parameters, GHC will not know whether it should cast via | > "Either Int Age" or "Either Int Int", while with a type family there | > will be only one choice, "Concrete (Either NT1 Age) = Either Int Int". | > In general, castNT . uncastNT would have the nice type | > castNT . uncastNT :: Concrete a ~ Concrete b => a -> b | > which plainly expresses „Cast between any to values who have the same | > concrete representation.“. Just as a side remark in case this comes up | > later again. | > | > | > | > BTW, what should the base-case be? I believe most user-friendly is a | > least-specific class | > instance IsNT a a | > so that the cast "Either Age a -> Either Int a" is possible. Or are | > overlapping instances too bad and the user should derive instances for | > all non-container non-newtype types himself: | > instance IsNT Int Int .... | > | > | > Am Dienstag, den 23.07.2013, 05:23 +0000 schrieb Simon Peyton-Jones: | >> The question of how to represent all this in HsSyn, to communicate | >> between TcDeriv and TcInstDcls, is a somewhat separate matter. We can | >> solve that in several ways. But first we need be sure what the FC | >> story is. | > | > For now what I am doing is that in TcDeriv, I am implementing the | > method | > with a value "unfinishedNTInstance :: a" which I am then replacing in a | > always-run simplCore pass with the real implementation in Core. It is a | > work-around that lets me explore the design-space and implementation | > issues without having to rewire GHC. | > | > Greetings, | > Joachim | > | > | > _______________________________________________ | > ghc-devs mailing list | > ghc-devs@haskell.org | > http://www.haskell.org/mailman/listinfo/ghc-devs | | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://www.haskell.org/mailman/listinfo/ghc-devs
Yes, that's what I got from Joachim's response to my design, also. My only other thought is to have some way to store an _axiom_, instead of an R coercion. But, that seems very fishy and wrong-headed. So, I guess we'll have to have ~R#. I'm tempted to use "~R#" as its name, to make it impossible to write in Haskell code. Would there be any problems with this? I'll go ahead and include the new coercion form when I commit roles. Richard On Jul 23, 2013, at 7:46 PM, Simon Peyton-Jones wrote:
I thought about the design you suggest below, but rejected it because I don't see how to do lifting -- which is really the whole point! In particular, what are you going to write for
ntList :: NT a b -> NT [a] [b] ntList (MkNT castNT uncastNT) = MkNT ??? ???
For lists you could write (fmap castNT), but the whole point of this exercise is not to write that -- and the type might not be an instance of Functor.
I'm thinking we need (~R#) as a type constructor.
Simon
| -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Richard | Eisenberg | Sent: 23 July 2013 09:51 | To: Joachim Breitner | Cc: ghc-devs@haskell.org | Subject: Re: Exposing newtype coercions to Haskell | | A few responses: | | - As Simon said, there is no great reason we don't have ~R# in Core. | It's just that we looked through GHC and, without newtype coercions, | there is no need for ~R#, so we opted not to include it. I'm still not | convinced we need it for newtype coercions, though. What if we have this | in Core? | | > class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a } | > NTCo:Age :: Age ~R# Int -- see [1] | > NTAgeInst :: NT Age Int | > NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT = \(x | > :: Int). x |> sym NTCo:Age } | | [1]: We still do have representational coercions, even though it would | be bogus to extract their type, as the type constructor ~R# does not | exist. But, coercionKind, which returns the two coerced types, and the | new coercionRole (which would return Representational in this case) work | just fine. | | Here, we don't need to abstract over ~R#, by just referring to the | global axiom directly. Does this compose well? I think so; you'll just | have to inline all of the coercions. But, the coercions won't ever get | too big, as they will always mirror exactly the structure of the types | being coerced. Simon, this is the sort of "magic" I was thinking of, | magical because I can't imagine a way this could be produced from an | HsExpr. | | Also, nice example of how the one-parameter design might aid the | programmer. I think that thinking about the base case is also | productive, but I don't have a clear enough opinion to express on that | front. | | Richard | | On 2013-07-23 08:21, Joachim Breitner wrote: | > Hi Richard and Simon, | > | > thanks for your detailed notes. | > | > Am Montag, den 22.07.2013, 17:01 +0100 schrieb Richard Eisenberg: | > | >> - I think you *do* want HsExprs not CoreExprs. Though I haven't worked | >> much in TcDeriv myself, I imagine everything uses HsExprs so that they | >> can be type-checked. This allows nice error messages to be reported at | >> the site of a user's "deriving instance IsNT ...". | > | > My plan was to make all checks (constructors in scope; IsNT classes for | > all data constructor arguments present) in TcDeriv, so you get nice | > error messages. If it turns out that the actual coercion can only be | > generated in a later pass, then it the checks just need to be strong | > enough to make that pass always succeed. | > | >> - But, there's a wrinkle here. The (~#) type, along with (~) and (:=:) | >> (the last is from the soon-to-be Data.Type.Equality), all work over | >> so-called *nominal* coercions. | > | > I know; I was just using them until representational equality is in and | > plan to switch then. | > | >> (Nominal coercions correspond to the "C" coercions from this paper) | > | > I got confused by C and T in my previous mails. In any case, I am only | > concerned with representational equality (T, it seems) for this | > project. | > | >> Or, it's possible | >> that we could add abstraction over representational coercions, but I | >> prefer the magical approach, because I don't see a general need for | >> the | >> ability to abstract. | > | > Hmm, I must admit I was assuming that once the roles implementation is | > in there will be ~# and ~#/T (or ~R#, which is a less-easy-to-confuse | > moniker) available in Core. | > | > | >> Now that I think of it, you may need to generalize the deriving | >> mechanism a bit. All current "deriving"s generate code that the user | >> could write. (Typeable is something of an exception here.) Here, the | >> generated code is something that a user can not write. Maybe that's | >> why | >> you wanted CoreExprs in the first place! | > | > Exactly. But it is also the reason why we are aiming for deriving | > classes (and not NT values), because it is already an established way | > of | > having the compiler generate code for you. | > | > | >> - I prefer the two-parameter class over a one-parameter, as it seems | >> more flexible. | > | > Thanks for spotting the phantom type replacing example, which is a | > features I’d also like to have. The type family was just a quick idea | > (and it would be neat to be able to ask GHCi via ":kind! (Concrete t)" | > what t looks like with all newtypes unfolded), but it’s not worth the | > loss of flexibility. | > | > | > In some cases, the type family might require less type annotations. | > Consider | > newtype Age = Age Int | > newtype NT1 = NT1 Int | > newtype NT2 = NT2 Int | > | > myCast :: Either NT1 Age -> Either NT2 Age | > myCast = castNT . uncastNT | > | > With two parameters, GHC will not know whether it should cast via | > "Either Int Age" or "Either Int Int", while with a type family there | > will be only one choice, "Concrete (Either NT1 Age) = Either Int Int". | > In general, castNT . uncastNT would have the nice type | > castNT . uncastNT :: Concrete a ~ Concrete b => a -> b | > which plainly expresses „Cast between any to values who have the same | > concrete representation.“. Just as a side remark in case this comes up | > later again. | > | > | > | > BTW, what should the base-case be? I believe most user-friendly is a | > least-specific class | > instance IsNT a a | > so that the cast "Either Age a -> Either Int a" is possible. Or are | > overlapping instances too bad and the user should derive instances for | > all non-container non-newtype types himself: | > instance IsNT Int Int .... | > | > | > Am Dienstag, den 23.07.2013, 05:23 +0000 schrieb Simon Peyton-Jones: | >> The question of how to represent all this in HsSyn, to communicate | >> between TcDeriv and TcInstDcls, is a somewhat separate matter. We can | >> solve that in several ways. But first we need be sure what the FC | >> story is. | > | > For now what I am doing is that in TcDeriv, I am implementing the | > method | > with a value "unfinishedNTInstance :: a" which I am then replacing in a | > always-run simplCore pass with the real implementation in Core. It is a | > work-around that lets me explore the design-space and implementation | > issues without having to rewire GHC. | > | > Greetings, | > Joachim | > | > | > _______________________________________________ | > ghc-devs mailing list | > ghc-devs@haskell.org | > http://www.haskell.org/mailman/listinfo/ghc-devs | | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://www.haskell.org/mailman/listinfo/ghc-devs
| that seems very fishy and wrong-headed. So, I guess we'll have to have ~R#. I'm | tempted to use "~R#" as its name, to make it impossible to write in Haskell code. Sounds ok to me. Simon | -----Original Message----- | From: Richard Eisenberg [mailto:eir@cis.upenn.edu] | Sent: 23 July 2013 23:12 | To: Simon Peyton-Jones | Cc: Joachim Breitner; ghc-devs@haskell.org | Subject: Re: Exposing newtype coercions to Haskell | | Yes, that's what I got from Joachim's response to my design, also. My only other | thought is to have some way to store an _axiom_, instead of an R coercion. But, | that seems very fishy and wrong-headed. So, I guess we'll have to have ~R#. I'm | tempted to use "~R#" as its name, to make it impossible to write in Haskell code. | Would there be any problems with this? I'll go ahead and include the new coercion | form when I commit roles. | | Richard | | On Jul 23, 2013, at 7:46 PM, Simon Peyton-Jones wrote: | | > I thought about the design you suggest below, but rejected it because I don't | see how to do lifting -- which is really the whole point! In particular, what are you | going to write for | > | > ntList :: NT a b -> NT [a] [b] | > ntList (MkNT castNT uncastNT) = MkNT ??? ??? | > | > For lists you could write (fmap castNT), but the whole point of this exercise is | not to write that -- and the type might not be an instance of Functor. | > | > I'm thinking we need (~R#) as a type constructor. | > | > Simon | > | > | -----Original Message----- | > | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Richard | > | Eisenberg | > | Sent: 23 July 2013 09:51 | > | To: Joachim Breitner | > | Cc: ghc-devs@haskell.org | > | Subject: Re: Exposing newtype coercions to Haskell | > | | > | A few responses: | > | | > | - As Simon said, there is no great reason we don't have ~R# in Core. | > | It's just that we looked through GHC and, without newtype coercions, | > | there is no need for ~R#, so we opted not to include it. I'm still not | > | convinced we need it for newtype coercions, though. What if we have this | > | in Core? | > | | > | > class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a } | > | > NTCo:Age :: Age ~R# Int -- see [1] | > | > NTAgeInst :: NT Age Int | > | > NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT = | \(x | > | > :: Int). x |> sym NTCo:Age } | > | | > | [1]: We still do have representational coercions, even though it would | > | be bogus to extract their type, as the type constructor ~R# does not | > | exist. But, coercionKind, which returns the two coerced types, and the | > | new coercionRole (which would return Representational in this case) work | > | just fine. | > | | > | Here, we don't need to abstract over ~R#, by just referring to the | > | global axiom directly. Does this compose well? I think so; you'll just | > | have to inline all of the coercions. But, the coercions won't ever get | > | too big, as they will always mirror exactly the structure of the types | > | being coerced. Simon, this is the sort of "magic" I was thinking of, | > | magical because I can't imagine a way this could be produced from an | > | HsExpr. | > | | > | Also, nice example of how the one-parameter design might aid the | > | programmer. I think that thinking about the base case is also | > | productive, but I don't have a clear enough opinion to express on that | > | front. | > | | > | Richard | > | | > | On 2013-07-23 08:21, Joachim Breitner wrote: | > | > Hi Richard and Simon, | > | > | > | > thanks for your detailed notes. | > | > | > | > Am Montag, den 22.07.2013, 17:01 +0100 schrieb Richard Eisenberg: | > | > | > | >> - I think you *do* want HsExprs not CoreExprs. Though I haven't worked | > | >> much in TcDeriv myself, I imagine everything uses HsExprs so that they | > | >> can be type-checked. This allows nice error messages to be reported at | > | >> the site of a user's "deriving instance IsNT ...". | > | > | > | > My plan was to make all checks (constructors in scope; IsNT classes for | > | > all data constructor arguments present) in TcDeriv, so you get nice | > | > error messages. If it turns out that the actual coercion can only be | > | > generated in a later pass, then it the checks just need to be strong | > | > enough to make that pass always succeed. | > | > | > | >> - But, there's a wrinkle here. The (~#) type, along with (~) and (:=:) | > | >> (the last is from the soon-to-be Data.Type.Equality), all work over | > | >> so-called *nominal* coercions. | > | > | > | > I know; I was just using them until representational equality is in and | > | > plan to switch then. | > | > | > | >> (Nominal coercions correspond to the "C" coercions from this paper) | > | > | > | > I got confused by C and T in my previous mails. In any case, I am only | > | > concerned with representational equality (T, it seems) for this | > | > project. | > | > | > | >> Or, it's possible | > | >> that we could add abstraction over representational coercions, but I | > | >> prefer the magical approach, because I don't see a general need for | > | >> the | > | >> ability to abstract. | > | > | > | > Hmm, I must admit I was assuming that once the roles implementation is | > | > in there will be ~# and ~#/T (or ~R#, which is a less-easy-to-confuse | > | > moniker) available in Core. | > | > | > | > | > | >> Now that I think of it, you may need to generalize the deriving | > | >> mechanism a bit. All current "deriving"s generate code that the user | > | >> could write. (Typeable is something of an exception here.) Here, the | > | >> generated code is something that a user can not write. Maybe that's | > | >> why | > | >> you wanted CoreExprs in the first place! | > | > | > | > Exactly. But it is also the reason why we are aiming for deriving | > | > classes (and not NT values), because it is already an established way | > | > of | > | > having the compiler generate code for you. | > | > | > | > | > | >> - I prefer the two-parameter class over a one-parameter, as it seems | > | >> more flexible. | > | > | > | > Thanks for spotting the phantom type replacing example, which is a | > | > features I'd also like to have. The type family was just a quick idea | > | > (and it would be neat to be able to ask GHCi via ":kind! (Concrete t)" | > | > what t looks like with all newtypes unfolded), but it's not worth the | > | > loss of flexibility. | > | > | > | > | > | > In some cases, the type family might require less type annotations. | > | > Consider | > | > newtype Age = Age Int | > | > newtype NT1 = NT1 Int | > | > newtype NT2 = NT2 Int | > | > | > | > myCast :: Either NT1 Age -> Either NT2 Age | > | > myCast = castNT . uncastNT | > | > | > | > With two parameters, GHC will not know whether it should cast via | > | > "Either Int Age" or "Either Int Int", while with a type family there | > | > will be only one choice, "Concrete (Either NT1 Age) = Either Int Int". | > | > In general, castNT . uncastNT would have the nice type | > | > castNT . uncastNT :: Concrete a ~ Concrete b => a -> b | > | > which plainly expresses "Cast between any to values who have the same | > | > concrete representation.". Just as a side remark in case this comes up | > | > later again. | > | > | > | > | > | > | > | > BTW, what should the base-case be? I believe most user-friendly is a | > | > least-specific class | > | > instance IsNT a a | > | > so that the cast "Either Age a -> Either Int a" is possible. Or are | > | > overlapping instances too bad and the user should derive instances for | > | > all non-container non-newtype types himself: | > | > instance IsNT Int Int .... | > | > | > | > | > | > Am Dienstag, den 23.07.2013, 05:23 +0000 schrieb Simon Peyton-Jones: | > | >> The question of how to represent all this in HsSyn, to communicate | > | >> between TcDeriv and TcInstDcls, is a somewhat separate matter. We can | > | >> solve that in several ways. But first we need be sure what the FC | > | >> story is. | > | > | > | > For now what I am doing is that in TcDeriv, I am implementing the | > | > method | > | > with a value "unfinishedNTInstance :: a" which I am then replacing in a | > | > always-run simplCore pass with the real implementation in Core. It is a | > | > work-around that lets me explore the design-space and implementation | > | > issues without having to rewire GHC. | > | > | > | > Greetings, | > | > Joachim | > | > | > | > | > | > _______________________________________________ | > | > ghc-devs mailing list | > | > ghc-devs@haskell.org | > | > http://www.haskell.org/mailman/listinfo/ghc-devs | > | | > | _______________________________________________ | > | ghc-devs mailing list | > | ghc-devs@haskell.org | > | http://www.haskell.org/mailman/listinfo/ghc-devs | > |
participants (3)
-
Joachim Breitner -
Richard Eisenberg -
Simon Peyton-Jones