Specification of newtype deriving

[Ross Paterson]

On Thu, Mar 30, 2006 at 09:48:14PM +0200, Twan van Laarhoven wrote:
> The Trac page for 'Generalised deriving for newtype' remarks that it is 
> 'difficult to specify without saying "the same representation"'.
> 
> I assume that no one has tried yet, so I'll take a shot at it.

Thank you for taking up that challenge.  It is important to know whether
newtype deriving is sugar or not, even though the translation will never
be used by a compiler.

By the way, the description in the GHC User's Guide 7.4.12.2:

	newtype T v1...vn = T' (S t1...tk vk+1...vn) deriving (c1...cm)

is too restrictive in requiring that S must be a type constructor of
the same arity as T, forbidding things like

	newtype Wrap m a = Wrap (m a) deriving (Monad, Eq)

It should be

	newtype T v1...vn = T' (t vk+1...vn) deriving (c1...cm)

with vk+1...vn not free in the type expression t.  It should also
mention that T may not be recursive, unless all the classes are
those derivable by the existing mechanism.  (There is some
awkwardness in the overlap between the two mechanisms.)

Your translation looks good, but I think you missed a bit:

> 4. If T is an algebraic data type:
>    > data T a = C1 (T1 a) ..
>    >          | ..
>    then define:
>    > wrap_T   x = case x of
>    >              (C1 x1 ..) -> C1 (wrap_T1 x1) ..
>    >              ..
>    > unwrap_T x = case x of
>    >              (C1 x1 ..) -> C1 (unwrap_T1 x1) ..
>    >              ..
>    With an alternative for each constructor of T.

The T you were talking about before would be an application of an
algebraic data type constructor to types T_i.  If you just substitute
those for the a's, the expansion could go on forever.  I think it's
necessary to assign each type constructor a higher-rank version of
wrap/unwrap along the lines of Ralf Hinze's "Polytypic values possess
polykinded types".  It looks doable, but it's disturbing that something
with trivial operational semantics is so hard to describe.