Deriving Data for poly-kinded datatypes

Thu Feb 23 22:49:01 UTC 2017

Some thoughts on the topic: admittedly, probably not very useful.

A couple of obvious statements:

1)

gcast1 itself operationally makes sense regardless of the kind of the
argument you're skipping past.

gcast1 :: forall c t t' a. (Typeable t, Typeable t') => c (t a) -> Maybe (c
(t' a))

This is an operation we can define pretty easily, however we want. It works
more or less by definition. It was included in the original paper.

2)

dataCast1 on the other hand is an member of the class, and it needs that
'Data d' constraint or it can't do its job.

dataCast1 :: (Data a, Typeable t) => (forall d. Data d => c (t d)) -> Maybe
(c a)

Attempting to weaken the Data d constraint there doesn't work, because then
dataCast1 wouldn't be able to do its job. Without it you can't write ext1Q
in terms of dataCast1, as noted in the but about 'bogusDataCast' in the
original paper: Scrap More Boilerplate: Reflection, Zips and Generalized
Casts
<https://github.com/aistrate/Articles/blob/master/Haskell/Scrap%20More%20Boilerplate%20-%20Reflection,%20Zips,%20and%20Generalised%20Casts%20(Laemmel,%20Peyton%20Jones).pdf>

Since then we obviously picked up polymorphic kinds, which muddled the
story about when a data instance is for a type that looks like `T d`.

On the other hand, the user will be the one calling this method, and
they'll have to take Data instances for d and use them to generate c (t
d).  Knowledge of if argument is of kind * is purely local, though. If t is
Typeable and d is Data, then (t d), d is kind *, t :: * -> *. So to call
dataCast1, the user has to already know the argument is kind *, and that
the type t that they are trying to use (maybe not the T in the data
instance itself) is of kind * -> *.

There is no contradiction in trying to call this on a data type with the
wrong kind for it to succeed. T is not necessarily t. It is our job to
check if it is.

Supplying the default shouldn't lock our data instance to the form T a. If
for some reason adding this default would break the instance We can make a
more interesting default that does something like look at the kind of the
argument first to determine if it is kind * before proceeding after casting
to ensure the kinds match.

*tl;dr** yes, it would seem it would be worth fixing the instances of Data
produced to supply dataCast1 when the kind of the argument is polymorphic.
Otherwise turning on PolyKinds in a package will simply break dataCast1 for
basically all of its data types.*

-Edward

P.S. Ultimately, in a perfect world we'd be able to unify dataCast1 and
dataCast2 with some tricky base case for kind k1 = * and induction over k
-> k1. Off hand, I don't see how to do it. I played for a while with trying
to write a higher kinded Data to support this, but my scribbles didn't
cohere into usable code. gfoldl pretty much locks you into kind *. I even
tried playing with profunctors and powers here to no real avail. I do have
some old Data1 code in an syb-extras package that I use to write a few
'impossible' Data instances, but that seems to be solving a different, if
related, problem, and doesn't scale up to arbitrary kinds. Ideally there'd
be a plausible Data that makes sense for other kinds k, and everything
could become dataCast1, w/ dataCast2, and the missing higher versions just
an iterated application of it. I just don't see that there is a way to turn
it into code.

On Thu, Feb 23, 2017 at 2:51 PM, Ryan Scott <ryan.gl.scott at gmail.com> wrote:

> Hi Pedro,
>
> I'm quite confused by a peculiarity of deriving Data (more info in
> Trac #13327 [1]). In particular, if you write this:
>
>     data T phantom = T
>       deriving Data
>
> Then the derived Data instance is NOT this:
>
>     instance Typeable phantom => Data (T phantom) where
>       ...
>
> But instead, it's this:
>
>     instance Data phantom => Data (T phantom) where
>       ...
>       dataCast1 f = gcast1 f
>
> The gcast1 part is why it requires the stronger (Data phantom)
> context, as you noted in Trac #4028 [2].
>
> What confuses me, however, is that is apparently does not carry over
> to poly-kinded datatypes. For instance, if you write this:
>
>     data T (phantom :: k) = T
>       deriving Data
>
> Then you do NOT get this instance:
>
>     instance Data (phantom :: *) => Data (T phantom) where
>       ...
>       dataCast1 f = gcast1 f
>
> But instead, you get this instance!
>
>     instance (Typeable k, Typeable (phantom :: k)) => Data (T phantom)
> where
>       ...
>       -- No implementation for dataCast1
>
> This is quite surprising to me. I'm not knowledgeable enough about
> Data to know for sure if this is an oversight, expected behavior, or
> something else, so I was hoping you (or someone else highly
> knowledgeable about SYB-style generic programming) could help me out
> here.
>
> In particular:
>
> 1. Does emitting "dataCast1 f = gcast1 f" for datatypes of kind (k ->
> *) make sense? Or does it only make sense for types of kind (* -> *)?
> 2. Is there an alternate way to define dataCast1 that doesn't require
> the stronger Data context, but instead only requires the more general
> Typeable context?
>
> Ryan S.
> -----
> [1] https://ghc.haskell.org/trac/ghc/ticket/13327
> [2] https://ghc.haskell.org/trac/ghc/ticket/4028#comment:5
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170223/61c75952/attachment-0001.html>