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

[oleg at okmij.org]

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.