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.

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))
Interesting solution but I'm not smart enough to see how the solution can be generalized to any data type that's an instance of Data. Do I have to repeat the "if then else" for every instance of the Data type class (which I can't) or is there some other way? Oscar

It is quite straightforward to extend the SYB generic programming framework to existential data types, including existential data types with type class constraints. After all, an existential is essentially a variant data type with the infinite, in general, number of variants. The only, non-fatal, problem is _not_ with writing the instance of gunfold. Defining gunfold is easy. The problem is that the existing SYB -- or, the module Data/Data.hs to be precise -- has non-extensible constructor and datatype descriptions (Constr and DataType). The problem is not fatal and can be worked around in various inelegant ways. Alternatively, one can fix the problem once and for all by making DataType and Constr extensible -- along the lines of the new Exceptions. The following file http://okmij.org/ftp/Haskell/DataEx.hs demonstrates one such fix. The file DataEx.hs also tries to avoid the overlap with Data.Typeable. (One doesn't need to carry the name of the datatype's type constructor in DataType. That name can be obtained from the result of typeOf). The file DataEx can be used alongside the original Data.hs. The code below uses DataEx in that way, to complement Data.hs. The hope is that the maintainers of SYB might choose to extend Data.hs -- perhaps using some bits or ideas from DataEx.hs. The following is a complete literal Haskell code illustrating gfold/gunfold for existentials.
{-# LANGUAGE ExistentialQuantification, Rank2Types, ScopedTypeVariables #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE DeriveDataTypeable #-}
module SybExistential where
We import the old Data.Data and complement it with DataEx. We assume that DataEx.hs present in the -i path.
import Data.Generics (gnodecount) import Data.Data as Old import DataEx
-- The following is the sample existential data type suggested by -- Oscar Finnsson. We use that data type as our running example.
data DataBox = forall d. (Show d, Eq d, DataEx d) => DataBox d
We make the DataBox itself to be a member of Typeable, Eq and Show.
instance Typeable DataBox where typeOf _ = mkTyConApp (mkTyCon "DataBox") []
instance Show DataBox where show (DataBox x) = "DataBox[" ++ show x ++ "]"
-- Two databoxes are the same if the types of their enclosed values -- are the same, and their values are the same too instance Eq DataBox where DataBox x == DataBox y | Just y' <- cast y = x == y' DataBox _ == DataBox _ = False
The file DataEx makes constructor representation extensible. We hereby add a new variant to constructor representation, so to represent _any_ existential data type.
data ExConstr = forall a. Typeable a => ExConstr a
instance Show ExConstr where show (ExConstr a) = "ExConstr" ++ show (typeOf a)
instance Typeable ExConstr where typeOf _ = mkTyConApp (mkTyCon "ExConstr") []
instance Eq ExConstr where ExConstr x == ExConstr y = typeOf x == typeOf y
We are now ready to implement gfold/gunfold for DataBox. First is gfold; gfold is not affected by our extensions of Constr and is not re-defined in DataEx.
instance Old.Data DataBox where gfoldl k z (DataBox d) = z DataBox `k` d
As the instance of DataType for DataBox we use a DataBox object itself. DataBox is already a member of all needed classes (Eq, Show, Typeable), except for the following. The file DataEx.hs defines a Read-like type class to de-serialize constructor representations. We don't need this feature here.
instance ReadCtor DataBox where readConstr _ str = error "not yet defined"
We come to the main instance, of DataEx:
instance DataEx DataBox where
As the `description' of DataBox's datatype we take a sample DataBox value. We only care about typeOf of that value.
dataTypeOf _ = DataType (DataBox (undefined::Int))
Since an existential data type is a ``variant data type with, generally, infinite number of data constructors'', we can use the very value of the existential as the description of that particular ``constructor.''
toConstr = Constr . ExConstr
And finally, the definition of gunfold
gunfold k z (Constr c) | Just (ExConstr ec) <- cast c, Just (DataBox (_::a)) <- cast ec = k (z (DataBox::a -> DataBox))
That is it. Here are a few tests.
-- sample DataBoxes tdb1 = DataBox (42::Int) tdb2 = DataBox ("string", tdb1)
tdb2_show = show tdb2 -- "DataBox[(\"string\",DataBox[42])]"
The following tests use gfold
tdb1_gcount = gnodecount tdb1 -- 2
tdb2_gcount = gnodecount tdb2 -- 17
whereas the following tests use gunfold.
-- generic ``minimum'' -- (I took a liberty to define 0 as the min Int value, since -- it prints better)
genMin :: DataEx a => a genMin = r where r = case DataEx.dataTypeOf r of DataType x -> build . min_ctor $ x min_ctor x | Just (AlgDataType (c:_)) <- cast x = Constr c min_ctor x | Just IntDataType <- cast x = Constr . DataEx.IntConstr $ 0 min_ctor x | Just CharDataType <- cast x = Constr . DataEx.CharConstr $ " " min_ctor x | Just (DataBox _) <- cast x = Constr . ExConstr $ DataBox False build = DataEx.fromConstrB genMin
min_box = genMin :: DataBox -- DataBox[False]
-- rot a term leaving only its skeleton rot :: DataEx a => a -> a rot = DataEx.fromConstrB genMin . DataEx.toConstr
tdb1_skel = rot tdb1 -- DataBox[0]
tdb2_skel = rot tdb2 -- DataBox[("",DataBox[False])]

OK. That was probably the most complete answer ever.
Under what license are you releasing DataEx.hs? I'm wondering if I may
use it in my package (under BSD3 license) until something like it is
included in SYB.
Pedro: How are extensions to SYB handled? code.google only seems to
handle issues - not tickets.
-- Oscar
On Wed, May 26, 2010 at 8:31 AM,
The only, non-fatal, problem is _not_ with writing the instance of gunfold. Defining gunfold is easy. The problem is that the existing SYB -- or, the module Data/Data.hs to be precise -- has non-extensible constructor and datatype descriptions (Constr and DataType). The problem is not fatal and can be worked around in various inelegant ways. Alternatively, one can fix the problem once and for all by making DataType and Constr extensible -- along the lines of the new Exceptions. The following file
http://okmij.org/ftp/Haskell/DataEx.hs
demonstrates one such fix. The file DataEx.hs also tries to avoid the overlap with Data.Typeable. (One doesn't need to carry the name of the datatype's type constructor in DataType. That name can be obtained from the result of typeOf). The file DataEx can be used alongside the original Data.hs. The code below uses DataEx in that way, to complement Data.hs. The hope is that the maintainers of SYB might choose to extend Data.hs -- perhaps using some bits or ideas from DataEx.hs.

Under what license are you releasing DataEx.hs? I'm wondering if I may use it in my package (under BSD3 license) until something like it is included in SYB.
DataEx.hs as other such code of mine has been written in the hope it might be useful, or at least instructive. I usually place such code in the public domain, and I wish DataEx.hs and the related code in the Haskell-Cafe message to be in the public domain as well. Please use the code as you wish. If a specific formal statement from me is required, please let me know.
participants (2)
-
oleg@okmij.org
-
Oscar Finnsson