Laws for GHC.Generics

[Edward Kmett]

When implementing Data instances for abstract data types to avoid the
horrible mess we used to get with opaque map types and the like, I've found
it useful to use a "model" type internally, like modeling a Map as some
kind of quotient of a list with a fake "constructor" for the function that
wraps it.

https://github.com/haskell/containers/blob/master/Data/Map/Internal.hs#L483

In such cases we were able to avoid introducing any new undefined cases.
I'd really personally prefer if such abstract generic instances could
likewise avoid throwing around bottoms into the surrounding code. Letting
folks generically change out keys in a map is actually quite useful, having
the structure you rebuild randomly bottom out becaue you did so is a lot
less so.

This would imply limiting yourself to just the `to . from = id` law for
such abstract Generic instances (mutatis mutandis for Generic1).

This has the unfortunate property that you can now sometimes detect when
you do choose to break a transformation into two passes, and from . to in
the middle you get detectable differences from if you do it in one pass,
but would allow you to define such things as pretending a map is a list of
pairs, letting you walk in to the keys and the values.

If we thought a tiny bit harder about how to represent such
pseudo-constructors we might be able to make it even safe for users to
reason about when this is the only guarantee they get as opposed to normal.
e.g. perhaps by representing it as a different M1 argument than C1 does
(MetaCons) or extending MetaCons with an extra type level Bool indicating
such 'abstract' use? This could *almost* just be done by the user detecting
the lowercase first letter in the constructor name by introspecting on the
symbol carried in the "virtual" MetaCons, but unfortunately Symbols are
completely opaque as types right now, so guarding against such instances
has to be done at the term rather than type level.

-Edward

On Mon, Mar 20, 2017 at 4:52 PM, Gershom B <gershomb at gmail.com> wrote:

> I had a bit of discussion today on how to handle generic instances for
> abstract types.
>
> It resolved to the following question, in a sense -- what are the laws
> for the Generic typeclass?
>
> Should require that `from` and `to` be an isomorphism of data types
> (i.e. that `from . to` and `to . from` both be the identity) or should
> we require only the weaker one-sided retract condition (i.e. that
> `from . to` be the identity.). If the latter, is it better that `from`
> be partial (which i  prefer) or that it quotient together "equivalent"
> representations (i.e. representing a map as a `fromList` as
> syb-generics do).
>
> The documentation doesn't seem to provide clear guidance here, and it
> might be worth discussing if some should be added.
>
> Cheers,
> Gershom
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170320/0955af81/attachment-0001.html>