"equivalent" concept

[xgbuils]

Hi!

I would like to comment that I feel very atracted by this project. I read this project several times to little by little understand better the concepts that are written. However the concept of equivalence is confusing for me. The definition is defined by example and, then, is used on definitions of algebras. For example:

### Functor

1. `u.map(a => a)` is equivalent to `u` (identity)
2. `u.map(x => f(g(x)))` is equivalent to `u.map(g).map(f)` (composition)

But maybe, the type that implements Functor is not any of this type examples. Then, is it not better define equivalence in terms of Setoid that defines equals method?

I mean:

### Functor

Functor implements the Setoid specification

1. `u.map(a => a).equals(u)` (identity)
2. `u.map(x => f(g(x))).equals(u.map(g).map(f))` (composition)

Cheers!

[davidchambers]

Using Setoid is a good idea, @xgbuils, but we would encounter a problem with functions:

Two functions are equivalent if they yield equivalent outputs for equivalent inputs.

x => x + x and x => 2 * x are equivalent, but it's impossible to define Function#fantasy-land/equals such that all equivalent functions are considered equal (even Haskell does not permit == to operate on functions).

[xgbuils]

Hi @davidchambers

But you can assume that exists the definition of Function#fantasy-land/equals and implements Setoid. Indeed, Two functions are equivalent if they yield equivalent outputs for equivalent inputs is a good definition for equals that obey the laws of Setoid. Another thing is that this definition is impossible to implement for all of types of functions or has bad performance. But maybe the implementation is not the scope of fantasy land. I don't know.

[davidchambers]

It could be confusing to refer to a Setoid in one context as a type for which we could describe value equality in words, and in other contexts as a type which actually provides fantasy-land/equals.

[xgbuils]

I don't try to mess terms.

Only I think that "equivalent" concept, for me, it does not seem necessary and the types that are using the equivalent concept could be replaced by types that implements Setoid.

Then, you say that is impossible to define fantasy-land/equals for functions.

But I don't understand what is the problem to not be able to define fantasy-land/equals for functions that implies that is not possible to replace equivalent term by a type that implements Setoid in the current laws.

On the other hand. I do think that is possible to define an Function#fantasy-land/equals that implements Setoid. Other thing is that definition is or isn't computable for all types of functions.

[xaviervia]

I think this might relate to the problem of what equality is in general terms. "Equivalent" as used in the laws seems to me to be referring that the fact that the laws expect the equivalence to be "up to isomorphism".

Defining an equality that works for laws (that is, not just for hard comparisons within the JavaScript language, but in general for the underlying mathematical theory that underpins them) is a problem that is probably outside the scope of Fantasy Land. If I understand this correctly, the problem of equivalence and isomorphisms is what drives Homotopy Type Theory and the Univalent Foundations.

So to recap, I think the meaning of "equivalent" when used in the context of the laws is different than the meaning of the "equals" function regarding the Setoid algebra as implemented within Fantasy Land. "equals" is in this case narrowly defined for the context of JavaScript, which might not have the expressivity to describe the concept of "equivalence".

[xgbuils]

Sorry, I'm a little rusty about maths. But I want to understand exactly what means "equivalent" because someone could be interested in creating some library that implements some algebra of fantasy land and be sure that their library obey the laws.

Then:

"Equivalent" as used in the laws seems to me to be referring that the fact that the laws expect the equivalence to be "up to isomorphism".

It worries me reading "seems to me" about something that I would expect it should be clear. Because if "equivalent" concept is not clear, how could we know if some algebra implementation follows the specified laws or not?

About the "up to isomorphism", I've never read this expression. I read about isomorphism to say that some algebras behave equal to/are equivalent. For example ({true, false}, OR) is isomorphic to ({true, false}, AND). Because there are a bijective function h: {true,false} -> {true, false} such that the behaviour is the same:

h(false) = true
h(true) = false

false OR false == false    |    true  AND true  == true
false OR true  == true     |    true  AND false == false
true OR false  == true     |    false AND true  == false
true OR true   == true     |    false AND false == false

But I don't understand what means some value is isomorphic to another value.

u.map(a => a) is equivalent to u (identity) u.map(x => f(g(x))) is equivalent to u.map(g).map(f) (composition)

Then definitely, I don't understand what means "equivalent" for you reading the first paragraph. Sorry.

Defining an equality that works for laws (that is, not just for hard comparisons within the JavaScript language, but in general for the underlying mathematical theory that underpins them) is a problem that is probably outside the scope of Fantasy Land. If I understand this correctly, the problem of equivalence and isomorphisms is what drives Homotopy Type Theory and the Univalent Foundations.

Of course, I also think defining an equality is outside the scope of Fantasy Land. In my opinion, Fantasy Land defines algebras based on methods that obey some specified laws. Fantasy Land don't say the implementation of these methods, it just says some rules that must obey. For this reason, defining "equivalent" seems outside of the scope and this concept definition does not make sense for me. My view is, then, using fantasy-land/equals that ensure reflexivity, symmetry and transitivity and is clearer to know if obey the laws or not.

So to recap, I think the meaning of "equivalent" when used in the context of the laws is different than the meaning of the "equals" function regarding the Setoid algebra as implemented within Fantasy Land.

From my point of view, fantasy-land/equals does not have meaning.

"equals" is in this case narrowly defined for the context of JavaScript, which might not have the expressivity to describe the concept of "equivalence".

For me, fantasy-land/equals is not narrow concept of JavaScript. An example for that is === or == don't obey reflexivity. For me fantasy-land/equals is an algebraic method without any meaning or expressivity.

On the other hand, I still don't understand why does being not able to define a computable algorithm for each type of function, imply being not able to use fantasy-land/equals instead of "equivalent" concept on algebra laws.

Cheers and thanks!

[bumbleblym]

You can create a legal setoid that has different behavior for 'equal' values.

Even(2).equals(Even(4)) // true
Even(2).reduce((acc, x) => acc + x, 0) // 2
Even(4).reduce((acc, x) => acc + x, 0) // 4

[xgbuils]

Hi @bumbleblym

I'm trying to understand your example but I don't know what is Even and how are equals and reduce methods implemented.

Thanks!

[bumbleblym]

The Even setoid divides numbers into 2 equivalence classes depending on whether they are even.

As others have tried to point out, equivalence as defined by your setoids, and equivalence as required by the spec... are not equivalent. ( •_•) ( •_•)>⌐■-■ (⌐■_■)

class Even {
  constructor(num) {
    this.num = num;
    this.isEven = num % 2 === 0;
  }
  equals(other) {
    return this.isEven === other.isEven;
  }
  reduce(f, z) {
    return f(z, this.num);
  }
}

Even(2).equals(Even(3)) // false

[xgbuils]

As others have tried to point out, equivalence as defined by your setoids, and equivalence as required by the spec... are not equivalent.

I guess that you are surely right. But I don't understand what means equivalence required by the spec.

First of all, I guess that Even object is not any of the 4 examples of the docs list:

• Two lists are equivalent if they are equivalent at all indices.
• Two plain old JavaScript objects, interpreted as dictionaries, are equivalent when they are equivalent for all keys.
• Two promises are equivalent when they yield equivalent values.
• Two functions are equivalent if they yield equivalent outputs for equivalent inputs.

Then, I will try to understand what is "equivalent" reading that:

2. "equivalent" is an appropriate definition of equivalence for the given value. The definition should ensure that the two values can be safely swapped out in a program that respects abstractions.

Ok, it seems that first sentence does not shed light on the meaning. I need to understand what means "a program that respects abstractions" to understand the second sentence. I don't know it.

Thanks!

[bumbleblym]

The definition should ensure that the two values can be safely swapped out in a program that respects abstractions.

What it means is that values a and b are equivalent if swapping one out for the other in any program does not change that program's behavior.

a and b might not implement Setoid. But we could replace x => x * 2 with y => 2 * y and expect the same behavior. So they are equivalent.

a and b might not compare equal. We aren't going to get an answer from comparing 2 infinite lists of repeating 0's. But we could swap one out for the other and expect the same behavior. So they are equivalent.

a and b might compare equal.Even(2).equals(Even(4)). But swapping one out for the other has different behavior. So they are not equivalent, in that context.

[bcherny]

a and b might not implement Setoid. But we could replace x => x 2 with y => 2 y and expect the same behavior. So they are equivalent.

That is a convenient example because that specific case is already well defined in alpha equivalency.

If you rephrase your definition "a and b are equivalent if swapping one out for the other in any program does not change that program's behavior", you can think of a program p that takes some value x and produces a value y. Are you saying that x and x' are "equivalent" if the codomain of outputs of y (p(x)) is "equivalent" to the codomain of outputs of y' (p(x'))? Either the definition is circular, or we're relying on an informal "common sense equivalence", or I'm missing something.

[bumbleblym]

I don't know if x => x * 2 and y => 2 * y can be alpha equivalent (note the operand order). Or x => x + x and y => y * 2. Or arr.map(f).reverse() and arr.reverse().map(f). But they should be equivalent.

The equivalence of x and x' depending on the equivalence of y and y' seems circular. I don't know how to address that.

[davidchambers]

arr.reverse().map(f) and arr.map(f).reverse() are not equivalent, @bumbleblym: the former reverses arr in place; the latter does not.

[gabejohnson]

Should https://github.com/fantasyland/fantasy-land#terminology have a line explaining that equivalence for primitives is the same as ===? The definition given is completely circular.

[xgbuils]

Thanks!

I think I've already understood the meaning of "equivalent" concept used by Fantasy Land. One more doubt, if I implement Even setoid that does not implements reduce method like that:

class Even {
    constructor (num) {
        this.num = num
    }
    equals (other) {
        this.num % 2 === other.num % 2
    }
}

Is it Even(2) equivalent to Even(4)? If it is, I think that I know what means "program that respects abstractions". We need to define what methods/properties are public for some type of object to be able to define if is equivalent to another object.

[xgbuils]

Hi @gabejohnson

I think that equivalence for primitives should be Object.is because as defined in the terminlogy section says that two values can be safely swapped out in a program and we have 0 === -0 but x variable with 0 value can't be changed to x variable with -0 value in this program:

if (Object.is(x, 0)) {
    console.log('x is equal to 0')
}

[gabejohnson]

TIL Object.is. Thanks @xgbuils!

[bumbleblym]

@davidchambers: Thanks for the heads up!

@xgbuils: That raises some interesting questions:

console.log(Even(2)); // Even {num: 2}
console.log(Even(4)); // Even {num: 4}

There are a few other JavaScript introspection functions that I'm not familiar with. From what I understand, the use of such functions would not respect abstractions. Since their public behavior are exactly the same, you may consider them to be equivalent.

Perhaps someone else should chime in.

[mrosata]

Should https://github.com/fantasyland/fantasy-land#terminology have a line explaining that equivalence for primitives is the same as ===? The definition given is completely circular.

@gabejohnson Using @xgbuils suggestion of Object.is in place of ===, then that line added to the terminology section would read better.

[xgbuils]

Hi,

Currently, I think I understand the "equivalent" definition and it seems it has more advantages than using Setoid#equals.

About circularity, I don't think that definition is circular. I was able to know that the best definition for primitives is Object.is only understanding this sentence:

The definition should ensure that the two values can be safely swapped out in a program that respects abstractions.`

The same can be deduced of functions reading this sentence. Then, if there are examples is for better understanding. But they don't give more information than the definition does. Then, I think there is not circular definition.

For me it's OK to close this issue. Or maybe someone would like to do a PR to improve the understanding of equivalent definition. My English is not very good and I prefer to let someone else do the PR.

Thanks!

[davidchambers]

For me it's OK to close this issue.

Okay. I will close the issue, but we are of course open to pull requests to improve the wording.