Simplify Data.Type.Equality.==

Authored by dfeuer on Aug 9 2017, 8:50 PM.



Contrary to previous comments, we can calculate == for types
in an extremely general fashion. The approach used here is actually
the one mistakenly rejected as impossible. There will be some cases
when the previous version was able to reduce and this one is not,
particularly for types in * that are unknown, but known equal.
However, the new behavior is much more uniform. Within the
established framework of equality testing by pattern matching,
it does a better job than the previous version.

dfeuer created this revision.Aug 9 2017, 8:50 PM
dfeuer updated this revision to Diff 13469.Aug 9 2017, 9:07 PM

Fix import loop and commit message.

dfeuer edited the summary of this revision. (Show Details)Aug 9 2017, 9:08 PM
dfeuer updated this revision to Diff 13470.Aug 9 2017, 9:26 PM

Remove redundant imports and UndecidableInstances

There may be some places DataKinds can be removed too; I'm
not sure and I doubt it matters.

dfeuer updated this revision to Diff 13471.Aug 9 2017, 9:39 PM

Yet more silly redundant imports.

One more difference: the old way declares

type instance (a :: ()) (b :: ()) = 'True

The new way does not, and the only way to recover it is with a special case. I don't think it's worth it.

Argh. I guess another problem is that people could actually be relying on == not being structural. This could be solved by offering a structural equality default, mutually recursive with the open user-specified equality. The profusion of instances would return, but they'd almost all be tiny. I guess I'll email the libraries list.

bgamari edited edge metadata.Sep 2 2017, 5:49 PM

Was there ever a conclusion on this?

dfeuer added a comment.Sep 2 2017, 6:46 PM

Richard likes it, but I don't think there's been a formal decision as yet.

goldfire edited edge metadata.Sep 3 2017, 5:03 AM

On the related mailing list discussion, I said that this is possible without TypeInType. Here is how:

type family Equal (a :: k) (b :: k) :: Bool where
  Equal ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) =
    Equal f g && Equal a b
  Equal a a = 'True
  Equal a b = 'False

Note that my Equal does not take the kind k as a visible parameter. The problem you might have run into when trying this is that you need to annotate the return kind as Bool in order to get a CUSK, and therefore, have access to polymorphic recursion.

Note that my version here isn't any better in any meaningful way than what's in this diff -- I just wanted to back up my claim that the introduction of TypeInType is incidental.

dfeuer updated this revision to Diff 13757.Sep 5 2017, 5:23 PM

Simplify based on Richard's suggestion

Add to changelog

dfeuer retitled this revision from Use TypeInType to simplify type == to Simplify Data.Type.Equality.==.Sep 5 2017, 6:39 PM
dfeuer edited the summary of this revision. (Show Details)
dfeuer added inline comments.Sep 5 2017, 6:42 PM
23 ↗(On Diff #13757)

I used the same text in each changelog. Should one be a shorter summary?

dfeuer updated this revision to Diff 13758.Sep 5 2017, 6:53 PM

Restore useful comments I deleted, and update them.

Although a library change isn't mine to approve formally, I agree with this change and with the new big comment.

RyanGlScott accepted this revision.Sep 7 2017, 7:08 PM
RyanGlScott added a subscriber: RyanGlScott.

LGTM, save for one very minor thing inline.


Importing only one constructor from Bool feels a bit silly. Let's just import Bool(..).

23 ↗(On Diff #13757)

I think it's fine the way it is.

This revision is now accepted and ready to land.Sep 7 2017, 7:08 PM
This revision was automatically updated to reflect the committed changes.