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