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

Add checks for Enum #23

Merged
merged 18 commits into from
Nov 10, 2021
Merged

Conversation

jacereda
Copy link
Contributor

Again, names are intentionally ugly to ensure someone suggests better ones ;)

ltordering a = succ a == Nothing || pred a < succ a

predsuccpredLaw :: a -> Boolean
predsuccpredLaw a = succ a == Nothing || (pred a >>= succ >>= pred) == pred a
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

At first I thought this might be a typo and we should be checking pred a == Nothing instead of succ a == Nothing, but actually I think we can remove that check altogether:

If pred a is Nothing, then (pred a >>= succ >>= pred) == pred a will always be true, regardless of whether you have a law-abiding Enum instance. If pred a is Just something, then whether (pred a >>= succ >>= pred) == pred a holds depends on whether you have a law-abiding Enum instance.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right, the last two can get rid of the test.

gtordering a = succ a == Nothing || succ a > pred a

ltordering ∷ a → Boolean
ltordering a = succ a == Nothing || pred a < succ a
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is redundant; if gtordering holds, and we have a law-abiding Ord instance, then this will certainly hold. I think we should remove this law from the Enum class, really.

@hdgarrood
Copy link
Contributor

Sorry to be a bother but this has made me realise there are some issues with the Enum laws. I'll open an issue in purescript-enums.

@hdgarrood
Copy link
Contributor

Oops, didn't realise you were already discussing this over in enums!

@jacereda
Copy link
Contributor Author

@hdgarrood Can you suggest good names for the Bounded laws?

I also used crappy names there: https://github.com/garyb/purescript-quickcheck-laws/blob/master/src/Test/QuickCheck/Laws/Data/BoundedEnum.purs

@hdgarrood
Copy link
Contributor

The enumpred and enumsucc laws feel a bit like a homomorphism in that the enum structure is preserved when going between a and Int, which might be a bit more obvious if you wrote it like this:

fromEnum <$> pred a == pred (fromEnum a)

I'm not sure if that's necessarily an improvement, though. Also I'm not sure if 'homomorphism' is quite the right word here, because I've only really come across that word in group theory, where it refers to the interaction of a binary operation with a function like fromEnum, but in this case, pred is not binary ("unary"?). So I'm not sure.

@jacereda
Copy link
Contributor Author

I'm doubting now the enumpred/enumsucc laws make sense. Isn't it possible to have, say, an enum mapping only to even values?

@garyb
Copy link
Member

garyb commented Nov 13, 2016

Hmm, I don't think so, that's what the laws are there to prevent. You could have an Even newtype that would only admit even values, and have the appropriate enum for that though.

@jacereda
Copy link
Contributor Author

I found this:

https://hackage.haskell.org/package/proto-lens-0.1.0.2/src/src/Data/ProtoLens/Message/Enum.hs

Shouldn't those be relaxed to:

  • fromEnum (pred a) < fromEnum a
  • fromEnum a < fromEnum (succ a)

@jacereda
Copy link
Contributor Author

Let's say you wanted to wrap libavcodec:
https://github.com/FFmpeg/FFmpeg/blob/master/libavcodec/avcodec.h#L488

If we want to represent that with an enum I think we should relax the rules.

@garyb
Copy link
Member

garyb commented Nov 13, 2016

We don't - or at least, not like that. The way to do it would be to create an ADT for that enum, and then convert it back into a numeric value when using it with the FFI.

@hdgarrood
Copy link
Contributor

Yeah, I agree with @garyb, that's not what an enumeration is in my mind. In my mind an enumeration of a set X is a bijection from the natural numbers to X (or perhaps, instead of the whole set of natural numbers, you might have a finite subset of the natural numbers of the form {1,2,3,...n} for some fixed number n). In that sense, toEnum and fromEnum are this bijection and its inverse. So imo toEnum shouldn't skip over any numbers, either. (In fact, should we have toEnum bottom == 1 as a law?)

You can certainly create an ADT for codecs like that, and so of course you'll need functions to attempt conversions to and from the numeric representation that libavcodec uses, but I don't think these functions should live inside the BoundedEnum typeclass.

@hdgarrood
Copy link
Contributor

hdgarrood commented Nov 13, 2016

Actually looking at the source, I think we should probably have fromEnum bottom == 0 as a law. AFAICT this is a law-abiding instance:

data DayOfWeek = Monday | Tuesday | ...

instance BoundedEnum DayOfWeek where
  fromEnum Monday = 46
  fromEnum Tuesday = 47
  fromEnum Wednesday = 48
  ...

but the code seems to assume that we will have fromEnum bottom == 0. For example: https://github.com/purescript/purescript-enums/blob/3b6c0847f0263369184e4027a76845acde5c17bc/src/Data/Enum.purs#L234-L243

@hdgarrood
Copy link
Contributor

@garyb
Copy link
Member

garyb commented Nov 13, 2016

Yeah, I don't think fromEnum bottom needs to be 0 necessarily, it should just map to a contiguous range between fromEnum bottom and fromEnum top?

@jacereda
Copy link
Contributor Author

It's true that trying to model C enums via PS enums might not be a good idea, given that several names in a C enum can refer to the same value. But I also want to understand what does having contiguous values bring to the table.

@hdgarrood
Copy link
Contributor

I think, for me, it's mainly that that is what the word 'enumeration' implies, i.e. that it means the name is appropriate. Also, I don't think requiring contiguousness will rule out many useful instances either. If you can define an Enum instance for some type which satisfies all the laws apart from enumpred and enumsucc, it's always possible to define a different instance that satisfies all the laws (just by changing to/fromEnum).

I guess it also means you can do things like, if you know you want to find the nth successor of something, you can do fromEnum >>> (_ + n) >>> toEnum which I guess might be a lot cheaper than actually doing succ n times, especially if n is quite large. Also it gives you a way of asking how many things are in between two elements: fromEnum x - fromEnum y.

Base automatically changed from master to main February 27, 2021 02:04
@JordanMartinez
Copy link
Contributor

Should this PR be closed?

@hdgarrood
Copy link
Contributor

Possibly, but it would be helpful if you could include some reasoning as to why you think we might want to consider closing this. Are we deciding we don't want to implement checks for Enum in this library at all, or is there a problem with this implementation in particular, or what?

@JordanMartinez
Copy link
Contributor

I was proposing we close this mainly due to inactivity. I think checks for Enum should still be done, but if no one is going to continue working on this, it removes a PR to keep track of. We already have too many open PRs, so I'm trying to reduce that number.

@hdgarrood
Copy link
Contributor

I think we should only close PRs for inactivity if the original submitter is not responsive to questions. That isn't what has happened here - a number of commits have been pushed since the last review. I personally think that we should leave it open until we either:

  • review it and merge it,
  • review it and spot a problem that prevents it from being merged, or
  • we decide we don't want to add Enum law checks to this library after all (in which case the issue can be closed too).

Copy link
Contributor

@JordanMartinez JordanMartinez left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The code here looks good to me. I think the EuclideanRing test changes are due to #30, which should be fixed in #58.

But that being said, aren't there cases where an enumeration could lead to integer overflow if one's starting int is very high? Should the docs be updated to mention the possibility of integer overflow?

src/Test/QuickCheck/Laws/Data/EuclideanRing.purs Outdated Show resolved Hide resolved
@JordanMartinez
Copy link
Contributor

Current CI failures: no BoundedEnum instance for Maybe, Either, or Tuple.

[1/3 NoInstanceFound] test/Test/Data/Either.purs:18:3

  18    Data.checkBoundedEnum prxEither
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  
  No type class instance was found for
  
    Data.Enum.BoundedEnum (Either A B)
  
  while applying a function checkBoundedEnum
    of type Arbitrary t2 => BoundedEnum t2 => Ord t2 => Proxy @Type t2 -> Effect Unit
    to argument prxEither
  while checking that expression checkBoundedEnum prxEither
    has type t0 t1
  in value declaration checkEither
  
  where t1 is an unknown type
        t0 is an unknown type
        t2 is an unknown type

[2/3 NoInstanceFound] test/Test/Data/Maybe.purs:18:3

  18    Data.checkBoundedEnum prxMaybe
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  
  No type class instance was found for
  
    Data.Enum.BoundedEnum (Maybe A)
  
  while applying a function checkBoundedEnum
    of type Arbitrary t2 => BoundedEnum t2 => Ord t2 => Proxy @Type t2 -> Effect Unit
    to argument prxMaybe
  while checking that expression checkBoundedEnum prxMaybe
    has type t0 t1
  in value declaration checkMaybe
  
  where t1 is an unknown type
        t0 is an unknown type
        t2 is an unknown type

[3/3 NoInstanceFound] test/Test/Data/Tuple.purs:18:3

  18    Data.checkBoundedEnum prxTuple
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  
  No type class instance was found for
  
    Data.Enum.BoundedEnum (Tuple A B)
  
  while applying a function checkBoundedEnum
    of type Arbitrary t2 => BoundedEnum t2 => Ord t2 => Proxy @Type t2 -> Effect Unit
    to argument prxTuple
  while checking that expression checkBoundedEnum prxTuple
    has type t0 t1
  in value declaration checkTuple
  
  where t1 is an unknown type
        t0 is an unknown type
        t2 is an unknown type

@JordanMartinez
Copy link
Contributor

CI now builds.

@JordanMartinez
Copy link
Contributor

Can this PR get another review?

@JordanMartinez JordanMartinez merged commit 44d0449 into purescript-contrib:main Nov 10, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

5 participants