Lysxia / first-class-families

First-class type families
https://hackage.haskell.org/package/first-class-families
MIT License
86 stars 12 forks source link

Adds equality class #53

Closed Skyfold closed 8 months ago

Skyfold commented 1 year ago

I have been working on Fcf.Data.MapC to implement MapC using the same type as Data.Map.Strict.Internal.Map. While I was writing the implementation I ran into an issue where TyEq won't work, see pull request.

This adds an equality type class to handle types that are semantically equal, but their types are not equivalent. I added a DefaultCompare_ to Fcf.Class.Ord that implements Compare in terms of Fcf.Class.Eq.== and a < lambda. This would let you have Compare by only defining < or <= for your type that already has equality.

I also removed the export of TyEq from Fcf.Class.Ord. This is to keep users from mistaking TyEq and == as the same thing. Let me know what you think of this change.

The equality type class is split over three files:

  1. Fcf.Class.Eq exports the non-Exp version of functions
  2. Fcf.Class.Eq.Exp exports the Exp version of functions
  3. Fcf.Class.Eq.Internal contains the implementation

I've noticed I don't always need partial function application and this split is something I am experimenting with in Fcf.Data.MapC. Let me know what you think of having a separate Exp version of modules.

Todo:

Skyfold commented 1 year ago

There is one other important question I have: would you consider using doctest, but only for the latest version of GHC supported?

I know we have had issues in fcf-containers with doctest since different versions of ghci report the type differently (the type is the same, just qualified differently). However, being able to test out the docs without having to manually copy over to ghci would be nice to have, plus it would help prevent the docs from drifting from the implementation.

Lysxia commented 1 year ago

Thanks for the PR! That's a very good idea.

I would prefer to just have one module for simplicity, exporting both the Exp and non-Exp variants with different names (and (==) would be non-Exp). Instead of DefaultCompare_ I would suggest the opposite, deriving (==) and (<=) from Compare. I agree with taking TyEq out from Fcf.Class.Ord, and I should maybe even think of a better name for it.

For the doctest issue, can you try using CPP instead? One benefit is that if you build the docs locally you will only get the doctests that are compatible with your local version of GHC.

Skyfold commented 1 year ago

I would prefer to just have one module for simplicity, exporting both the Exp and non-Exp variants with different names (and (==) would be non-Exp).

I merged the Eq modules into Fcf.Class.Eq and named the Exp versions EqExp (to not clash with Eq class) and NotEq. I really like the idea of making the Exp versions names and the non-Exp variants symbols. That way you write Filter (EqExp 5) '[1,5] instead of Filter ((==) 5) '[1,5]. This also means things like 5 == 6 look just like normal Haskell. Ideally, I would like to propagate this convention (Exp versions are names and non-Exp variants use symbols) to the rest of the codebase.

To illustrate what this naming convention would look like I modified Fcf.Class.Ord and Fcf.Data.Bool. Both now export Exp and non-Exp versions where the symbols (e.g.(<=)) are non-Exp and the type families/type synonym have their kind signatures added to their documentation to workaround this haddock issue. Together with Fcf.Class.Eq, these modules should give you a good idea of what this convention would look like in practice and if you want to expand this to other modules. The only downside is that these are all breaking changes (e.g. (<=) :: Bool -> Bool -> Exp Bool becomes (<=) :: Bool -> Bool -> Bool).

Let me know what you think.

Instead of DefaultCompare_ I would suggest the opposite, deriving (==) and (<=) from Compare.

I removed DefaultCompare_ and created EqualityDefault_ (I think I should rename it to DefaultEq_). I agree, it is much less confusing to define one Compare then to write both (==) and (<).

I agree with taking TyEq out from Fcf.Class.Ord, and I should maybe even think of a better name for it.

I think TyEq is a reasonable name. In my head I read it as "type equality". We could make the name TypeEq.

For the doctest issue, can you try using CPP instead? One benefit is that if you build the docs locally you will only get the doctests that are compatible with your local version of GHC.

I have not added the doctest test suite yet. I'll work on this in the next commit.

Lysxia commented 8 months ago

Sorry for the late response. In the end I would like to avoid breaking changes. A better solution then would be to use different modules for the two kinds of names, using an Exp. qualifier (by importing the older modules qualified) instead of an Exp suffix to disambiguate.

Also, for the new Bool definitions, you can reexport those of Data.Type.Bool.

Tell me if you still have time to work on this, otherwise I can make the changes myself.

Skyfold commented 8 months ago

Its been awhile, so my memory is a bit rusty. I think the reason I created new Bool definitions was because Data.Type.Bool accepts any kind, while the ones in Fcf.Data.Bool are actual copies of their value level equivalents.

This is && in Data.Type.Bool

type family a && b where
  'False && a      = 'False
  'True  && a      = a
  a      && 'False = 'False
  a      && 'True  = a
  a      && a      = a

while this is && in my branch

type (&&) :: Bool -> Bool -> Bool
type family (&&) a b where
  'True && b = b
  'False && _ = 'False

Unfortunately, it won't be possible to make non-Exp variants symbols without breaking changes. Looking back at my comments, I was asking for too much reorganization to mold first-class-families into the interface I wanted to use. I want a type level library that is a mirror of its value level counterparts with Exp only used when absolutely necessary. It might make more sense for me to make a fork with my changes so it does not impact current users.

What do you think?

Lysxia commented 8 months ago

The families in Data.Type.Bool do have the right kinds inferred according to haddock (and ghci) https://hackage.haskell.org/package/base-4.19.0.0/docs/Data-Type-Bool.html#t:-38--38-

A fork does seem like the easiest solution to experiment with a new style of encoding type families into something like Fcf.

Skyfold commented 8 months ago

I'll eat my words, Data.Type.Bool does mirror their value level equivalents. I should have checked with ghci.

Interestingly, my local hoogle displays the type family without the type annotations. I bet I mistook the lack of kind to mean it would accept any kind.

I'll close this pull request and keep this re-write as a fork.