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.
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.
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)).
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.
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?
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.
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:
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.
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.
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.
