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

[Carter Schonwald]

The close family with nonlinear matching does seem simpler.  Like I can
comfortably read it and understand what it does reasonably well and have
uniform expectations of what it means.

That said, I'm open to be swayed otherwise.  The

On Fri, Aug 11, 2017 at 11:44 AM Richard Eisenberg <rae at cs.brynmawr.edu>
wrote:

> tl;dr: I like David's first version, D3835.
>
> There is a fundamental tension in the definition of (==): Should it be
> reflexive or not? By "reflexive" here, I mean that (a == a) reduces to
> True, even if you know nothing further about a. The current definition of
> (==) is reflexive in this way for types of kind Type, but not for any of
> the other concrete instances (except the one for ()).
>
> We can't currently have our cake and it eat, too: as David points out in
> this thread, (==) is either reflexive or structurally recursive. It can't
> do both. Possibly a solution to #4259 (
> https://ghc.haskell.org/trac/ghc/ticket/4259) would allow us to have (==)
> that is both reflexive and structurally recursive, but I have no idea how
> to do it.
>
> I agree that the current choice of implementation for (==) is inconsistent
> in this regard and is perhaps foolish. I have no principled argument for
> why it is the way it is. But I wonder if we're better off embracing the
> distinction between a reflexive (==) and a structurally recursive (==) and
> provide both, with different names. 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 for the
> reflexive (==)). 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
>
>
> _______________________________________________
> 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/20170811/2b1e0d0d/attachment.html>