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

Doc 'Eq' instance fails Substitutivity #57

Open
BenjaminCosman opened this issue Jul 4, 2020 · 1 comment
Open

Doc 'Eq' instance fails Substitutivity #57

BenjaminCosman opened this issue Jul 4, 2020 · 1 comment

Comments

@BenjaminCosman
Copy link

Consider the following code:

module Main (main) where
import Prelude hiding ((<>))
import Text.PrettyPrint

main :: IO ()
main = do
  let s1 = text "if:" $+$ nest 4 (text "pass")
  let s2 = text "if:\n    pass"
  let f = (text "x" <>)

  --not following Eq's Substitutivity 'law':
  --first is True but second is False
  print $   s1 ==   s2
  print $ f s1 == f s2

  --examine the values visually:
  print $   s1
  print $   s2
  print $ f s1
  print $ f s2
  --outputs the following (note extra space in the 3rd):
  -- if:
  --     pass
  -- if:
  --     pass
  -- xif:
  --      pass
  -- xif:
  --     pass

If this is not the intended behavior of the various functions involved (<>, $+$, nest, ==), then there is a bug that should be fixed. If this is the intended behavior, then the documentation on Eq should alert the reader to the fact that the Substitutivity Law is not followed.

@phadej
Copy link
Contributor

phadej commented Jul 5, 2020

It could be documented that Eq instance witnesses equivalence (==) `on` render, thus for most combinators in the library substitutivity indeed doesn't hold.

pr welcome

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

No branches or pull requests

2 participants