Exposing newtype coercions to Haskell

Joachim Breitner mail at joachim-breitner.de
Thu Jul 4 15:30:03 CEST 2013


small update: I generalized the code at
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

        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

        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

BTW: Is this still on-topic on glasgow-haskell-users or should I move to

Joachim “nomeata” Breitner
  mail at joachim-breitner.dehttp://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>

More information about the Glasgow-haskell-users mailing list