[Haskell-cafe] Existentials and SYB [Was: GADTs and Scrap your Boilerplate]

Oscar Finnsson wrote:

I got the GADT

data DataBox where DataBox :: (Show d, Eq d, Data d) => d -> DataBox

and I'm trying to get this to compile

instance Data DataBox where gfoldl k z (DataBox d) = z DataBox `k` d gunfold k z c = k (z DataBox) -- not OK

As has been pointed out, DataBox is an ordinary existential data type, only written using the new-style notation. For clarity, let us define our DataBox with the conventional notation:

data DataBox = forall d. (Show d, Eq d, Data d) => DataBox d

So, the question becomes of using existentials with Scrap your Boilerplate. On one hand, it is unnervingly trivial to incorporate existentials into the SYB framework. Let us consider the signature of gunfold, the problematic member of the (Data a) type class. -- | Unfolding constructor applications gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a We have to eventually produce a value of the type (c DataBox). We observe that our work is done if we manage to produce one value of the type DataBox. We then apply the second argument to gunfold (which `lifts' from any type r to the type c r), and we are done. To produce an existential value, we need one witness of the constraints Show, Eq and Data. For example, the type Int is such witness. Thus, we are done indeed. Here is the complete code:

{-# LANGUAGE ExistentialQuantification, Rank2Types #-}

module F where

import Data.Generics

data DataBox = forall d. (Show d, Eq d, Data d) => DataBox d

instance Typeable DataBox where typeOf _ = mkTyConApp (mkTyCon "DataBox") []

instance Data DataBox where gfoldl k z (DataBox d) = z DataBox `k` d gunfold k z c = z (DataBox (42::Int))

One may complain that we have fixed not only the type of the argument to DataBox but also the value. We should let gunfold to `produce' the value. Here is a sketch:

enDataI :: (Int -> DataBox) enDataI = DataBox

enDataB :: (Bool -> DataBox) enDataB = DataBox

instance Data DataBox where gfoldl k z (DataBox d) = z DataBox `k` d gunfold k z c = (if True then k (z enDataI) else k (z enDataB))

Now, the particular Int value to supply to DataBox will be produced by the function k. The above code used the constant True to fix the choice of the type to Int. Generally, one could use the third argument of gunfold to help make the choice. That is, we could incorporate the choice of the type in the value of Constr.