Exposing newtype coercions to Haskell

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
25 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Simon Peyton Jones
(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 at haskell.org [mailto:glasgow-haskell-
| users-bounces at haskell.org] On Behalf Of Joachim Breitner
| Sent: 04 July 2013 14:30
| To: glasgow-haskell-users at 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 at joachim-breitner.de ? http://www.joachim-breitner.de/
|   Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
|   Debian Developer: nomeata at debian.org

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Joachim Breitner-2
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.

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

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.

Simon



Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Joachim Breitner-2
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.


Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Joachim Breitner-2
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 at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130711/3c548efa/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Simon Peyton Jones
POPLing today.  Let's discuss on Monday

| -----Original Message-----
| From: ghc-devs-bounces at haskell.org [mailto:ghc-devs-bounces at haskell.org]
| On Behalf Of Joachim Breitner
| Sent: 11 July 2013 15:25
| To: ghc-devs at 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 at joachim-breitner.de ? http://www.joachim-breitner.de/
|   Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
|   Debian Developer: nomeata at debian.org

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Simon Peyton Jones
In reply to this post by Joachim Breitner-2
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 at haskell.org [mailto:ghc-devs-bounces at haskell.org] On

|  Behalf Of Joachim Breitner

|  Sent: 11 July 2013 09:41

|  To: ghc-devs at 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 at joachim-breitner.de ? http://www.joachim-breitner.de/

|    Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C

|    Debian Developer: nomeata at debian.org
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130715/40f9d0df/attachment.htm>

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Joachim Breitner-2
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 at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130716/ea03f732/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Simon Peyton Jones
| 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

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Joachim Breitner-2
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 at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130716/44126c5a/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Nicolas Frisby
In reply to this post by Joachim Breitner-2
It's available here (for now).

  http://ittc.ku.edu/~nfrisby/tcrn-plugin.tar.gz

Sorry for the whack build/test infrastructure: I wasn't planning sharing
this write-once experimental code.

The 'MyTcRnDriver.initTcFromModGuts` function and the
'TcRnPlugin.append_guts` are the key functions.

The rest of 'MyTcRnDriver` is only necessary because 'tcRnModule` is a big
function that bakes in its own invocation of 'initTc`. Most other functions
in the tcrn don't do this. I hope to patch GHC to factor 'tcRnModule` a bit
and export the pieces so that it can be re-used with 'initTcFromModGuts`
instead

Note the TODOs; mostly they focus on stuff like hpc and Safe Haskell. Basic
functionality seems fine.

HTH.


On Tue, Jul 16, 2013 at 8:31 AM, Joachim Breitner
<mail at joachim-breitner.de>wrote:

> Hi,
>
> Am Dienstag, den 16.07.2013, 07:44 -0500 schrieb Nicolas Frisby:
> > It allows you to execute TcRn computations (without manually
> > reinitializing its monadic inputs), which is a prerequisite for
> > invoking most functions from the type checker or renamer. I anticipate
> > that such invocations will be helpful in your task.
>
> I see; in that case: Thanks!
>
> Greetings,
> Joachim
>
> --
> Joachim Breitner
>   e-Mail: mail at joachim-breitner.de
>   Homepage: http://www.joachim-breitner.de
>   ICQ#: 74513189
>   Jabber-ID: nomeata at joachim-breitner.de
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130716/9d9c9ed5/attachment.htm>

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Joachim Breitner-2
In reply to this post by Simon Peyton Jones
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 at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130722/beea952b/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Richard Eisenberg-2
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 at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs



Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Simon Peyton Jones
|  - 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 at haskell.org
|  > http://www.haskell.org/mailman/listinfo/ghc-devs
|  
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs at haskell.org
|  http://www.haskell.org/mailman/listinfo/ghc-devs

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Joachim Breitner-2
In reply to this post by Richard Eisenberg-2
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 at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130723/d91726e4/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Richard Eisenberg-2
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 at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs



Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Joachim Breitner-2
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 at joachim-breitner.de ? http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  ? GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130723/d2d3a17b/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Richard Eisenberg-2
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 at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs



Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Joachim Breitner-2
In reply to this post by Richard Eisenberg-2
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 at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130723/795d6de2/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Simon Peyton Jones
In reply to this post by Richard Eisenberg-2
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 at haskell.org] On Behalf Of Richard
|  Eisenberg
|  Sent: 23 July 2013 09:51
|  To: Joachim Breitner
|  Cc: ghc-devs at 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 at haskell.org
|  > http://www.haskell.org/mailman/listinfo/ghc-devs
|  
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs at haskell.org
|  http://www.haskell.org/mailman/listinfo/ghc-devs

12