Open xgbuils opened 5 years ago
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:
In my view, both of these cases should be allowed.
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.
The point here is that seems that these kind of laws are too much restrictive:
Sanctuary breaks this law in multiple ways:
- Input type checking
- 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).
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:
Input type checking
Regarding Sanctuary breaking this law, i don't think it quite counts:
@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?:
class Just extends Maybe {
...
map(f) {
const r = f(this.val)
return r === null ? Maybe.of(r) : Maybe.of(r);
}
}```
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 ofvar
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.
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 thenull
orundefined
value than for other values is unlikely to comply with the rule.
... and then simply use <forall ...>
where needed.
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.
See #311.
@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.
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
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:
This implementation breaks
No parts of f's return value should be checked
. However, it is also breaking the composition law: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:and
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!