Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft: Redefines the EqF type class to be heterogeneous. #132

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

benjaminselfridge
Copy link
Contributor

@benjaminselfridge benjaminselfridge commented Apr 19, 2022

This is just a draft -- not ready for merge.

This implements a change discussed in #129. Basically, it redefines EqF to be same-kinded with TestEquality, since the homogeneous variant wasn't being used. The idea is that EqF asks "are the types AND values of these two things equal?" so it makes sense to define on non-singletons.

I tried to be relatively conservative here, keeping TestEquality instances in most cases.

Another note -- I didn't do the analogous thing for TestEqualityF and TestEqualityFC; if this PR is to be merged, it probably makes sense to do those too, and make the change all in one go.

@benjaminselfridge benjaminselfridge marked this pull request as draft April 20, 2022 00:17
Comment on lines +93 to +96
-- | @EqF@ allows you to test for type- and value-level equality over a
-- parameterized type. It is like @TestEquality@, but unlike that class, @EqF@
-- returns `Nothing` when the type indices are equal but the values are not.
-- This makes it appropriate to implement on non-singleton types.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be helpful to provide an example of code that is not a legal TestEquality instance but is a legal EqF instance.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good call.

Comment on lines -270 to -273
instance TestEquality (Index l) where
testEquality IndexHere IndexHere = Just Refl
testEquality (IndexThere x) (IndexThere y) = testEquality x y
testEquality _ _ = Nothing
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I presume that this instance was removed because it does not obey the TestEquality laws? If so, should we remove the instances for other Index data types in parameterized-utils (e.g., Data.Parameterized.Context.{Safe,Unsafe}.Index)? Or would it be better to keep this TestEquality instance for a while to give users a chance to migrate to EqF?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, and I actually meant to put this back in to allow just such a gradual change.

Initially I had actually removed the instances in Context, but realized that it might screw people up in the short term if I did that.

Do you know if there is a way to deprecate a type class instance and have GHC give a warning that they should use eqF instead of testEquality?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not aware of a way to attach DEPRECATED pragmas to instances, unfortunately.

I am curious exactly how much churn this PR would entail. Even if we keep around all of the existing TestEquality instances, we're still changing TestEquality constraints to EqF, including OrdF's superclass—it seems likely that this will uncover missing EqF instances downstream. But if the changes required can be minimized to "copy-paste your TestEquality instances and change TestEquality to EqF", that might be manageable.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yep, this would entail a lot of churn -- not only will we uncover missing EqF instances downstream, this will invalidate all existing EqF instances (although I'm not sure if there are too many of those).

But yeah, the solution should just be to copy-paste instances.

I made this PR in discussion with RobD, as a way to start the conversation about whether this change is worth it. I think it is worth it, personally -- insofar as parameterized-utils is Galois' offering of a "standard library for dependent types in Haskell", we want to be in compliance with all the basic laws.

@robdockins
Copy link
Contributor

I'm generally in favor of this change. However, I think we need to break it into pieces to help manage the churn. First, let's change the Kind of EqF, implement new instances here and give downstream packages some time to implement their own instances. Next, we can change things that currently require TestEquality to require EqF instead, and finally we can remove TestEquality instances that don't follow the laws.

@benjaminselfridge
Copy link
Contributor Author

Makes sense to me.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants