Let's rework Data.Type.Equality.==

Fri Sep 1 17:54:45 UTC 2017

Wow, that email really got garbled. I was in the process of drafting it
when I sent it accidentally and then went off into the mountains and forgot
about it. Sorry about that! I had a few more things to say.

First, it might be possible to get away from the non-linear pattern using a
version of generics. In particular, if we derive Rep and From type families
for each type, we can define (==) by comparing generic representations. Or
we could derive (==) directly. Moreover, the non-linear pattern approach
won't help us define type-level Ord; for that we need either direct or
generic-mediated derivation. Related: it's a bit annoying that when the
case  ((f :: j -> k) (a :: j)) is rejected, we *know* that the type being
matched must be a constructor, but we can't really do anything directly
with that information.

Second, you write

> If we have a more flexible notion of equality, how can we be sure that
this more inclusive equality is always respected?
> [...]
> Specifically, you would want this: if (ty1 == ty2) and ty1 is substituted
for ty2 in some context, everything still works.

How is this really different from the situation on the term level? User
code must always take care to respect the quotient. You say (==) is only
"useful" if we can produce

reifyEq :: ((a == b) ~ True, Typeable a, Typeable b) => a :~: b.

I'm not convinced that this is the only measure of utility, although it's
an important one. That said, I suspect that the version of (==) in
Data.Type.Equality should be the simple polykinded one; others would
probably fit better elsewhere. Feel free to accept D3835 if you think we
should just do that.

On Aug 11, 2017 6:28 PM, "David Feuer" <david.feuer at gmail.com> wrote:

On Aug 11, 2017 9:39 AM, "Richard Eisenberg" <rae at cs.brynmawr.edu> wrote:

But I wonder if we're better off dxaa aembracing the distinction between a
reflexive (==) and a structurally recursive (==) and provide both, with
different names.

I don't think it would be bad to offer a canonical reflexive equality test.
There are probably situations where having such a thing would be marginally
useful. In particular,

MyEqual a b ~ 'False

isn't quite the same ass Alaska

YourEqual a b ~ 'False

even if the two type families are defined the same.

Or, we could just decide to go with the structurally recursive one, which
seems to be more useful, especially as I have become much more skeptical of
non-linear patterns (necessary Aziz a a add as ad ahs asf as s for the
reflexive (==)).

I'm a bit fuzzy on this. Don't *both* of my versions rely essentially on
nonlinear patterns to compare constructors? I suppose it might c always xd
Hz

In particular, I don't have a good story for how they would work in
Dependent Haskell. Section 5.13.2 of my thesis (
http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf)
contains some technical discussion of the challenges, but that section may
not be digestible on its own.

The point of difference between David's two proposed changes is
extensibility: that is, could someone decide to have a custom equality
operator on a user-defined type? This is indeed a reasonable thing to want
-- for example, you could imagine a record system that stores names of
fields and their types in a type-level list, but that list should really be
regarded as a set. However, worms lurk under this stone. If we have a more
flexible notion of equality, how can we be sure that this more inclusive
equality is always respected? Specifically, you would want this: if (ty1 ==
ty2) and ty1 is substituted for ty2 in some context, everything still
works. Sadly, there is no way to guarantee such a property. If (==) is to
be useful in a type system, we would need such a guarantee. (By "useful", I
mean that this is implementable: reifyEq :: ((a == b) ~ True, Typeable a,
Typeable b) => a :~: b.) This brings us to the doorstep of higher inductive
types -- a door that might be fun to enter, but is a long long way off.

In sum, I argue for David's first, inextensible version.

By the way, nothing about this requires TypeInType. If I had thought of
David's version (that splits apart type applications) in 2013, I probably
would have implemented (==) that way.

Richard

On Aug 10, 2017, at 9:00 PM, David Feuer <david.feuer at gmail.com> wrote:

I tend to agree with you, although I don't think () is a compelling
argument. Rather,  it reuses the name == that Haskellers are accustomed to
defining flexibly. But for that same reason, as well as the convenience, I
do think we should consider using a kind class. That way things at the type
level look pretty much like they do at the term level.

On Aug 10, 2017 10:59 AM, "Ryan Scott" <ryan.gl.scott at gmail.com> wrote:

> Personally, I'd be more inclined towards latter approach (in
> https://phabricator.haskell.org/D3837). After all, one of the key
> properties of (==) (for which the Haddocks even make a special note)
> is that it does not attempt to provide an instance that works for
> every possible kind. Indeed, as you've discovered, there are cases
> when it doesn't make sense to use DefaultEq, such as for ().
>
> I'll tentatively give my support for D3837, although I'd be curious to
> hear what Richard has to say about this (since I'm reasonably
> confident he gave (==) its current implementation).
>
> Ryan S.
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
_______________________________________________
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/20170901/021cdedb/attachment.html>