search

fantasyland / fantasy-land

Specification for interoperability of common algebraic structures in JavaScript
MIT License
10.08k stars 373 forks source link

Remove no part checked. Fixes #303. #311

Closed CrossEye closed 5 years ago

CrossEye commented 5 years ago

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?

davidchambers commented 5 years ago

This is nice!

joneshf commented 5 years ago

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 commented 5 years ago

@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 commented 5 years ago

@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 commented 5 years ago

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

CrossEye commented 5 years ago

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

puffnfresh commented 5 years ago

Add forall to everything

xgbuils commented 5 years ago

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:

  1. Does it mean parametric polymorphism?
  2. Does it mean inspection?
  3. Does it mean inspection with observable effect?