Exposing newtype coercions to Haskell
Richard Eisenberg
eir at cis.upenn.edu
Wed Jul 24 00:12:09 CEST 2013
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 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
>
More information about the ghc-devs
mailing list