Remove no part checked. Fixes #303. #311

CrossEye · 2019-02-18T19:23:31Z

This avoids the "No parts of should be checked" from the individual rules and adds a forAll intro section to explain what that means.

It is done using forall annotations on signatures. Could someone with deeper knowledge of H-M types double-check that I added it correctly?

Fixed strange type Removes 'No part of the value should be checked'. Adds intro section. Fixing strange typo Fixed strange type

davidchambers · 2019-02-18T20:40:15Z

This is nice!

davidchambers · 2019-02-18T20:40:42Z

README.md

+
+## `forAll`
+
+[Parametric polymorphism][pp] is essential to these algebras.  When the rules for any type are specified as applied to all values (`forall a b`) of the given generic types (here `a` and `b`), 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.


Could you wrap this paragraph at 79 characters?

Please change “Javascript” to “JavaScript” for consistency with the rest of the document.

Done and done.

davidchambers · 2019-02-18T20:41:50Z

README.md

@@ -363,7 +371,7 @@ method takes one argument:
 #### `map` method

 ```hs
-map :: Functor f => f a ~> (a -> b) -> f b
+map :: forall a b . Functor f => f a ~> (a -> b) -> f b


PureScript appears not to include a space before the .. I suggest we follow suit.

(Space is allowed in PS before the dot btw)

Yes, allowed in Haskell as well, at least in some example code, but it's much more rare, it seems.

davidchambers · 2019-02-18T20:44:33Z

README.md

@@ -159,6 +159,14 @@ Identity type, for example, could provide `Id` as its type representative:
 If a type provides a type representative, each member of the type must have
 a `constructor` property which is a reference to the type representative.

+
+## `forAll`


Might “Parametricity” be a better heading?

I don't think so. If someone doesn't understand this signature because of the forall clause:

map :: forall a b. Functor f => f a ~> (a -> b) -> f b

and tries to figure out what it is, a header that matches the confusing keyword is better than a term that -- given this confusion -- is likely unknown to them also.

Good point. Shall we use forall rather than forAll, though?

Absolutely. I'll fix that tonight.

safareli · 2019-02-19T06:46:22Z

README.md

+
+[Parametric polymorphism][pp] is essential to these algebras.  When the rules
+for any type are specified as applied to all values (`forall a b`) of the 
+given generic types (here `a` and `b`), the rule must hold for any JavaScript


I'm wondering how can we make restrictions polymorphism implies more clear here.
What you think on something like this:(bold is for highlighting the addition):

Parametric polymorphism is essential to these algebras. When the rules
for any type are specified as applied to all values (forall a b) of the
given generic types (here a and b), the rule must hold for any possible
JavaScript value ~~unless otherwise specified~~.
Since a parametrically polymorphic value does not "know" anything about the
type variables, it must behave the same regardless of its type. This is a somewhat
limiting but extremely useful property known as parametricity.
This implies, that a function should behave in same way for all values,
i.e. inspection of value is not allowed. for instance, that code that
behaves differently for the null or undefined value than for other
values ~~is unlikely to comply~~ complying with the rule.

we can steal some ideas from https://wiki.haskell.org/Polymorphism or/and link to it too (has better explanation then wikipedia)

I would like to expand this section. These are good ideas. The "unless otherwise specified" has to do with things like f must be a binary function or b must be same Apply as a. In such cases, not every value is allowable.

"is unlikely to comply" was about examples such as return r === null ? Maybe.of(r) : Maybe.of(r). The only way these examples could work is if their differences are not observable, so perhaps we can skip it. But it was part of the motivation for this change.

safareli · 2019-02-19T06:50:17Z

README.md

@@ -552,11 +559,7 @@ method takes two arguments:
    1. if `f` is not a function, the behaviour of `reduce` is unspecified.
    2. The first argument to `f` must be the same type as `x`.
    3. `f` must return a value of the same type as `x`.
-    4. No parts of `f`'s return value should be checked.
-
-1. `x` is the initial accumulator value for the reduction


why remove this line?

I have no problem putting it back. I just didn't see it adding anything. Is there something that makes it clear that an "empty" foldable will return this value? Do you think that this text captures that?

davidchambers

Several type signatures are missing forall. Let's use forall everywhere it applies, not just for the methods whose descriptions currently include “no parts of […] should be checked”.

joneshf · 2019-02-19T14:18:24Z

Since we were writing Haskell-esque type signatures, we were also inheriting Haskell's implicit forall for all type variables. I.e. it was already implied that things were parametrically polymorphic. The bit about no values being checked was still added in even though the signature explained that part. And we still get implementations that are not law abiding. The fact that we've moved to explicit forall doesn't seem like enough of a justification to me to also remove the bit about no values being checked. Adding an explicit forall is good because it is acting like a springboard to explain parametric polymorphism!

I'm not going to veto this PR, I think people making changes is good and I support it. But, I don't think this solves the underlying problem of people writing unlawful implementations.

Also, if we're now writing PureScript-esque type signatures (or Haskell-esque with GHC's ScopedTypeVariables extension), then we need to be consistent. All of the type variables should be introduced in the forall. E.g. map should be:

map :: forall a b f. Functor f => f a ~> (a -> b) -> f b

not

map :: forall a b. Functor f => f a ~> (a -> b) -> f b

Being inconsistent will lead to further explanations needed about how GHC's ScopedTypeVariables extension actually works and that's far off the beaten path of this spec.

CrossEye · 2019-02-19T20:46:57Z

@joneshf:

The goal was not to add forall. It was explicitly to remove "no values should be checked". (See #303 for details.) Adding forall seemed to be a compromise for those cases. I have no problem removing forall everywhere and just depending upon an expanded section on parametricity. I actually think that would be better.

CrossEye · 2019-02-19T20:59:50Z

@davidchambers: Rather than adding forall to the other signatures, let's look at removing all of them, and simply depending upon a parametricity section. I'll try to create a separate PR tonight or tomorrow.

davidchambers · 2019-03-02T20:01:34Z

@CrossEye, if you don't intend to update this pull request, shall we close it?

CrossEye · 2019-03-02T20:43:59Z

I intend to create a replacement, but life has gotten in the way. Hopefully soon.

puffnfresh · 2019-03-04T09:44:29Z

Add forall to everything

xgbuils · 2019-03-06T20:53:44Z

After @joneshf said that:

Since we were writing Haskell-esque type signatures, we were also inheriting Haskell's implicit forall for all type variables.

What 's the reason to add forall to everything? In my opinion, it generates noise in the law definitions. A section which explains that all laws are parametrically polymorphic is enough for me.

I think we have to get an agreement in #303 before doing the PR. Because it seems that no part to be checked is too much opened to interpretations:

Does it mean parametric polymorphism?
Does it mean inspection?
Does it mean inspection with observable effect?

CrossEye added 5 commits February 18, 2019 13:58

Removes 'No part of the value should be checked'. Adds intro section.

14fd346

Fixed strange type

3d72dbf

Fixing strange typo

2648ba7

Fixed strange typo

33bfd66

Removes 'No part of the value should be checked'. Adds intro section.

406b53f

Fixed strange type Removes 'No part of the value should be checked'. Adds intro section. Fixing strange typo Fixed strange type

CrossEye mentioned this pull request Feb 18, 2019

Is really necessary specify "No parts of <...> value should be checked"? #303

Open

davidchambers reviewed Feb 18, 2019

View reviewed changes

CrossEye added 3 commits February 18, 2019 18:31

Wrapping at 79 columns. 'Javascript' -> 'JavaScript'

61408a1

Wrapping at 79 columns. 'Javascript' -> 'JavaScript'

72a881f

Removing spaces: 'forall a b . <...>' -> 'forall a b. <...>'

89a0bd1

safareli reviewed Feb 19, 2019

View reviewed changes

davidchambers requested changes Feb 19, 2019

View reviewed changes

CrossEye closed this Mar 2, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Remove no part checked. Fixes #303. #311

Remove no part checked. Fixes #303. #311

CrossEye commented Feb 18, 2019

davidchambers commented Feb 18, 2019

davidchambers Feb 18, 2019

davidchambers Feb 18, 2019

CrossEye Feb 18, 2019

davidchambers Feb 18, 2019

CrossEye Feb 18, 2019

safareli Feb 19, 2019

CrossEye Feb 19, 2019

davidchambers Feb 18, 2019

CrossEye Feb 18, 2019

davidchambers Feb 19, 2019

CrossEye Feb 19, 2019

safareli Feb 19, 2019

CrossEye Feb 19, 2019

safareli Feb 19, 2019

CrossEye Feb 19, 2019

davidchambers left a comment

joneshf commented Feb 19, 2019

CrossEye commented Feb 19, 2019

CrossEye commented Feb 19, 2019

davidchambers commented Mar 2, 2019

CrossEye commented Mar 2, 2019

puffnfresh commented Mar 4, 2019

xgbuils commented Mar 6, 2019


		## `forAll`

		[Parametric polymorphism][pp] is essential to these algebras. When the rules for any type are specified as applied to all values (`forall a b`) of the given generic types (here `a` and `b`), 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.

Remove no part checked. Fixes #303. #311

Remove no part checked. Fixes #303. #311

Conversation

CrossEye commented Feb 18, 2019

davidchambers commented Feb 18, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

davidchambers left a comment

Choose a reason for hiding this comment

joneshf commented Feb 19, 2019

CrossEye commented Feb 19, 2019

CrossEye commented Feb 19, 2019

davidchambers commented Mar 2, 2019

CrossEye commented Mar 2, 2019

puffnfresh commented Mar 4, 2019

xgbuils commented Mar 6, 2019