Fantasy-land: Is really necessary specify "No parts of <...> value should be checked"?

[xgbuils]

Hi!

After reading #210, I still don't understand why these kind of law are needed. The topic starts talking about "No parts of b return value should be checked. But, finally, it concludes that the implementations that perform this kind of checks are breaking other laws.

For example:

class Maybe {
    static of(val) {
      return new Just(val);
    }
}

class Just extends Maybe {
    constructor(val) {
        super()
        this.val = val;
    }
    map(f) {
        const r = f(this.val)
        return r === null ? new Nothing() : Maybe.of(r);
    }
}

class Nothing extends Maybe {
    map(f) {
        return this;
    }
}

This implementation breaks No parts of f's return value should be checked. However, it is also breaking the composition law:

const f = x => x === 2 ? null : x;
const g = x => x === null ? 2 : x;

Maybe.of(2).map(f).map(g) // Nothing {}
Maybe.of(2).map(x => g(f(x))) // Just {val: 2}

Then, I wonder if No parts of f's return value should be checked is a really necessary law. For me it's a weird law because is talking about the implementation. For example these two implementations of Maybe:

class Just extends Maybe {
    ...
    map(f) {
        const r = f(this.val);
        return Maybe.of(r);
    }
}

and

class Just extends Maybe {
    ...
    map(f) {
        const r = f(this.val)
        return r === null ? Maybe.of(r) : Maybe.of(r);
    }
}

behave the same and are identity and composition law compliant. However, the second breaks the No parts of f's return value should be checked and is not functor lawful. It doesn't make sense for me.

Cheers!

[Avaq]

I think the law is there to serve as a more direct deterrent for unlawful implementations. Specifically, Maybe.of = x => x ? Just(x) : Nothing kind of implementations were very common.

I also believe that the law is redundant with regards to preventing these bad implementations, and in fact, overly restrictive otherwise. Sanctuary breaks this law in multiple ways:

1. Input type checking
2. Constrained type instances

In my view, both of these cases should be allowed.

[SimonRichardson]

I think the law is there to serve as a more direct deterrent for unlawful implementations. Specifically, Maybe.of = x => x ? Just(x) : Nothing kind of implementations were very common.

It is indeed to prevent that, also "were" should be "are". If someone comes up with a better phrasing of this, then I don't see why it shouldn't be amended.

[xgbuils]

The point here is that seems that these kind of laws are too much restrictive:

Sanctuary breaks this law in multiple ways:

1. Input type checking
2. Constrained type instances

and redundant (it seems that each algebraic type that is not "No parts of <...> value should be checked" compliant, it's not compliant with other of its laws).

[safareli]

Let's take simplest functions form the spec: of :: Applicative f => a -> f a. it's followed with No parts of "a" should be checked.

In Purescript similar function for Array will have signature like this:
of :: forall a. a -> Array a

if you have function like this you can't do anything to the input (you can't perform any "checking") except passing it to some other function or storing it in some other value. it's because it can be of any type and when you say your function works for all types it must work for all types otherwise compiler will reject you implementation.

In js there is no type system, and this kind of restriction is just specified verbally in fantasy land. for example the "No parts of <...> value should be checked" from the spec rejects this implementation:

Array.prototype.of = function(val) {
  if (val == []) {return []} else return [val]
  // or
  if (val == null) {return []} else return [val]
}

Which will be valid if that restriction is removed from the spec and we don't want such implementations as it would result in unlawful behavior.

We could use forall <...> in signature instead of the "No parts of <...> value should be checked" but it would not change the fact that "No parts of <...> value should be checked.

Sanctuary breaks this law in multiple ways:

1. Input type checking

2. Constrained type instances

Regarding Sanctuary breaking this law, i don't think it quite counts:

1. Input type checking is done during development, it's is basically doing the job of a compiler and if something is off your app crashes. If it's inspecting the value and depending on it's contents returns different result that it would be violation for me.
2. "Constrained type instances" it's also not a violation to me as it's not changing the value itself it's just adding some "instances" (it's just poor mans instance declaration).

[CrossEye]

@safareli:

Which will be valid if that restriction is removed from the spec and we don't want such implementations as it would result in unlawful behavior.

But if there's some other law that the implementation would be breaking, isn't this one then redundant? I think that's the main point.

I know that FantasyLand is written as a specification with little room for exposition, but I would rather see this as a note, or perhaps as forall <...>.

Again, is there any reason that this should be unlawful?:

js class Just extends Maybe { ... map(f) { const r = f(this.val) return r === null ? Maybe.of(r) : Maybe.of(r); } }

[safareli]

The inspection happening in the example you provided has no observable effect, therefore I consider it to be valid implementation.

Having forall <..> to me is same as the "No part ...." and if we start using forall the spec should still describe what a forall means and in that description we would still have something like:

forall <var>. - means that no part of var shouldn't be checked, i.e. implementation should not perform any inspection of a value so it works for all possible values in the same way.

[CrossEye]

I guess I'd simply like to see a section in the prefix similar to the "Terminology", "Type Signatures", etc. ones, something like:

forAll

Parametric polymorphism is essential to these algebras. When the rules for any type are specified as applied to all values (forall a or ∀ a) the rule must hold for any Javascript values unless otherwise specified. This implies, for instance, that code that behaves differently for the null or undefined value than for other values is unlikely to comply with the rule.

... and then simply use <forall ...> where needed.

[safareli]

That sounds good to me! Unless others disagree on this, I think a way forward would be to open a PR with changes discussed here.

[CrossEye]

See #311.

[nadameu]

@CrossEye:

Again, is there any reason that this should be unlawful?:

class Just extends Maybe {
    ...
    map(f) {
        const r = f(this.val)
        return r === null ? Maybe.of(r) : Maybe.of(r);
    }
}

It is not unlawful because both of the branches of the ternary operator return the same value (Maybe.of(r)). As @safareli said, the inspection has no observable effect.

The given implementation is equivalent to:

class Just extends Maybe {
  ...
  map(f) {
    return Maybe.of( f(this.val) );
  }
}

There is no inspection happening, which is exactly what the specification determines.

[xgbuils]

I would like to point that specs talk about inspection (checked), not about inspection with observable effect.

Do specs really need to talk about what means obserbable effect when there are other more clear laws which avoid unlawful specs?

For example, the fantasy-land/map type with the identity and composition functor laws are enough for spec completeness. The rest of definition rules are redundant:

u['fantasy-land/map'](f)
f must be a function

Of course, fantasy-land/map type says that first param of fantasy-land/map method must be a function (a -> b).

If f is not a function, the behaviour of fantasy-land/map is unspecified.

Of course, fantasy-land/map laws are expressed assuming fantasy-land/map type. There is nothing defined out of the scope.

f can return any value.

Of course, b in fantasy-land/map type means value of any type.

No parts of f's return value should be checked.

This is the law I started talking about. In my opinion too much restrictive and composition functor law avoids wrong implementations (see my first post).

fantasy-land/map must return a value of the same Functor

Of course, if it were not like that, the type of fantasy-land/map would have been:
fantasy-land/map :: Functor f, Functor t => f a ~> (a -> b) -> t b