Existentials and SYB [Was: GADTs and Scrap your Boilerplate]

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Existentials and SYB [Was: GADTs and Scrap your Boilerplate]

oleg-30

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.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Existentials and SYB [Was: GADTs and Scrap your Boilerplate]

Oscar Finnsson
>> 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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

SYB with Existentials

oleg-30

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])]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: SYB with Existentials

Oscar Finnsson
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,  <[hidden email]> wrote:

>
> 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.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: SYB with Existentials

oleg-30

> 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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe