Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Traversable laws? #24

Open
glebec opened this issue Sep 22, 2018 · 2 comments
Open

Traversable laws? #24

glebec opened this issue Sep 22, 2018 · 2 comments

Comments

@glebec
Copy link

glebec commented Sep 22, 2018

It doesn't appear as if checkers actually enforces all the Traversable laws, which include (as per http://haskellbook.com):

  • Naturality: t . traverse f = traverse (t . f). Transforming the final outer layer is the same as transforming the produced structure on the inside before swapping the types.
  • Identity: traverse Identity = Identity. Traversable doesn't add or inject any structure / context.
  • Composition: traverse (Compose . fmap g . f) = Compose . fmap (traverse g) . traverse f. "…we can collapse sequential traversals into a single traversal, by taking advantage of the Compose datatype, which combines structure."

These laws can be expressed via sequenceA but it's just another formulation, neither prettier nor uglier IMHO.

The current check just runs:

traversable :: forall f a b m.
               ( Traversable f, Monoid m, Show (f a)
               , Arbitrary (f a), Arbitrary b, Arbitrary a, Arbitrary m
               , CoArbitrary a
               , EqProp (f b), EqProp m) =>
               f (a, b, m) -> TestBatch
traversable = const ( "traversable"
                    , [ ("fmap", property fmapP)
                      , ("foldMap", property foldMapP)
                      ]
                    )
 where
   fmapP :: (a -> b) -> f a -> Property
   foldMapP :: (a -> m) -> f a -> Property

   fmapP f x = f `fmap` x =-= f `fmapDefault` x
   foldMapP f x = f `foldMap` x =-= f `foldMapDefault` x

Perhaps I am misreading this or not reasoning through it all the way, but it doesn't seem to me that this is enforcing all the laws, explicitly or implicitly.


Follow up: does this link imply that if fmap and foldMap can be recovered, then the laws must hold? It seems the other way around to me, that if the laws hold, fmap and foldMap can be recovered. I don't know enough to state this definitively, but the implication arrow doesn't seem to be symmetric here, i.e. I don't know if this is an "if and only if" relationship.

@glebec glebec changed the title traversable laws? Traversable laws? Sep 22, 2018
@sjakobi
Copy link
Member

sjakobi commented Mar 19, 2019

I agree that the Traversable laws should be covered completely.

For reference, both quickcheck-classes and hedgehog-classes offer properties for Traversable, but their implementations are among the trickier ones.

@sjakobi
Copy link
Member

sjakobi commented Feb 23, 2022

Good progress in #61. Tests for the naturality law(s) seem to be a bit tricky to implement and are left to do.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants