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:
data T a = C1 (T1 a) .. | ..
4. If T is an algebraic data type: 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.