Exposing newtype coercions to Haskell

[Joachim Breitner]

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
-------------- 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/glasgow-haskell-users/attachments/20130704/f73b2f4b/attachment.pgp>