New Constrained Type Variable for `(==)`

I want a new Constrained Type Variable, equalable. It can be filled in by types that (==) can compare soundly.

Type annotation of the (==) operator is a -> a -> Bool. However (==) can do expected behavior on only a part of types. For instance, Bytes in the elm/bytes package makes an unsound behavior that the operation always returns True.(elm/bytes issue)

It is because a value of Bytes is constructed by DataView on the Javascript code. (==) compare values using enumerable properties. The operator returns False when any enumerable properties aren’t the same between these arguments. A DataView value doesn’t have any enumerable properties, so the operator never returns False.

Types using Javascript code are easy to make this behavior, so such package maintainers have to make an effort to avoid it. I think the type system should do it alternatively on compiling time.

By equalable type variable, we can get several advantages. Of course, the Elm compiler will be able to detect the potential of unsound behavior by the (==) operator. On the other example, Dict comparable v will be able to replace with Dict equalable v as a more general type because comparable is a subset of equalable.

What do you think about this proposal?


In a document Basics in elm/core,

In a future release, the compiler will detect when (==) is used with problematic types and provide a helpful error message.

If it relates to my proposal or there is a plan, please tell me!

The biggest use case for static checking of == is function types. Function equality is undecidable (theoretically impossible). But the problem is that functions or other non-equatable types “infect” data structures that they are placed in. A record that contains a list of records with a custom type with one tag that has a function field is not equatable.

The existing CTVs all have a fixed number of members: only Int and Float are numbers. But an equatable CTV contains an unbounded number of types.

The benefits of a “proper” solution to equality wouldn’t just be eliminating undesirable behavior (always True for Bytes; a crash for functions). It would also be a way for custom types to define equality. The built-in Dict comparable v type is implemented as a red-black tree in Elm and has equality special-cased so that dictionaries with equal elements are equal, even if the tree representation differs. There is currently no way for a third-party library to do something similar.

@mgold

Thank you for replying! I have several questions.

In ideal, if the value equality was undecidable, it should detect on compiling time. If the function equality was undecidable theoretically, it can be detected by excluding from equalable CTV.

But an equatable CTV contains an unbounded number of types.

Did you say about the difficulty of the implementation? comparable CTV also contains an unbounded number types I think. comparable contains List comparable, and also contains List (List comparable). It can nest more (List (List (List (List comparable))) is comparable). Like this, equalable can be defined by a fixed number of types nest. Also, non-comparable types can infect data structures. Is it a disadvantage for the implementation of equalable?

The benefits of a “proper” solution to equality wouldn’t just be eliminating undesirable behavior.

What’re the benefits of it? Won’t the special case implemented for eliminating undesirable behavior?

The biggest problem with adding equatable as a CTV is that Elm’s syntax doesn’t allow you to constrain a variable in more than one way. For example, you can’t ask for a type that is both equatable and appendable. With the existing CTVs this isn’t much of a problem because they have very predictable overlaps: number and appendable have no common types (so specifying both would be useless), number implies comparable (so you can just use number) and comparable and appendable have precisely one type in common, String (so you can just use that).

With equatable, things would be more complicated because a function that requires both equatable and appendable is conceivable, but there are types that are both (List Int), types that are just equatable (Int) and types that are just appendable (List (Int -> Int)).

4 Likes

Reading this, I am wondering what benefit would equalable give us that we are not already getting from comparable? Perhaps it was explained in the OP, but I didn’t quite get it. :thinking:

I am wondering what benefit would equalable give us that we are not already getting from comparable ?

It is because equalable is more general than comparable. For example, equalable contains the user-defined Custom Types. I proposed equalable as a CTV that (==) do desirable behavior with.
When equalable was defined, (==) can have a type annotation as:

(==) : equalable -> equalable -> Bool

comparable contains too few types, so equalable cannot replace it.

The benefits of equalable are:

  • The compiler will be able to detect the potential of undesirable behavior by (==).
  • Some functions using comparable can be replaced with equalable as more general functions.

But if you include user defined custom types in equalable, can’t you just go the whole way and include them in comparable?

type SomeType = 
    Blah Int -- treat as 0, the Int will sort beneath this using lexicographical ordering.
  | Foo -- treat as 1
  | Bar NestedCustomType -- treat as 2, the nested type will sort beneath lexicographically.

equalable will still have the same restrictions as comparable in being undecidable over functions, so can’t you get just as far with mapping custom types onto comparable as you can with equaliable?

1 Like

This should not be possible as

type Maybe a =
    Just a -- treat as 0
    | Nothing -- treat as 1

and

type Maybe a =
    Nothing -- treat as 0
    | Just a -- treat as 1

should be the same.

This could be done by defining an order on the Constructors(Just,Nothing). I believe there were plans for something like that to come in the future, but from what I understand it would require a rewriting of the underlying type system.

For equalable this problem does not occur.

Just sort the constructor names.

I suppose records are more problematic.

type alias SomeRec =
 { a : Int
 , b : Int
 }

Do you take a or b as coming first in the lexicographical sort?

Is { a = 1, b = 2 } < { a = 2, b = 1 } because you compare the as first, or the other way because you compare the bs first.

Yes, it would absolutely be possible to make custom types and records comparable. However, there are (at least) three things you need to think about:

  1. The order for these types should be well-defined and predictable. That would probably mean sorting record fields alphabetically and custom constructors either alphabetically or in source order.

  2. If you make custom types comparable, built-in types such as List a (for comparable a) should also be comparable. But then you get back to the problems I mentioned in my last post that Elm doesn’t allow you to specify that a type variable should be both comparable and appendable.

  3. The order defined in this way carries basically no semantic information. It is just a convenience to allow you to use more types in Dicts and such.

The difference between equalable and comparable is generality. equalable does not need ordering.
So, it is difficult to define a record as comparable. However, to define as equalable is possible.

But I need to think about custom types because They can contain functions without type annotation (however, variants are defined before compiling).
I do not know inside the Elm compiler, so I do not know also how much effort is needed to implement it.

@rtfeldman
What do you think about it?
I want to decide the conclusion about whether it should be implemented or not.

If you had some unclear things due to my cheep English, please ask me.