nick8325 / quickspec

Equational laws for free
BSD 3-Clause "New" or "Revised" License
250 stars 24 forks source link

Can I add constrained polymorphic methods to a signature? #48

Closed isovector closed 4 years ago

isovector commented 4 years ago

I'd like QuickSpec to find monoid homomorphisms of the form foo (x <> y) = foo x <> foo y, but it's not clear how to give the (<>) :: Monoid m => m -> m -> m method to the signature, as it complains there is no Monoid instance for A.

nick8325 commented 4 years ago

QuickSpec does (experimentally) support typeclass polymorphism; see https://github.com/nick8325/quickspec/blob/master/examples/tests/TypeClass.hs for an example. Internally this uses Dict from the constraints package; you can add a typeclass-polymorphic function by converting it to take an explicit Dict parameter instead, and QuickSpec will recognise the use of Dict as typeclass polymorphism and handle it specially (e.g. hiding the Dict arguments when printing out laws).

However, there is a catch: QuickSpec assumes that all polymorphic terms can be tested by defaulting them to a single type (by default Int). In this case, since there's no Monoid Int instance, you won't be able to test any term that has a Monoid m constraint. You can use defaultTo to change the type used for defaulting (e.g. [Int] would work in this case), but if you have several different typeclasses this only works if you can find one instance that fits them all.

isovector commented 4 years ago

To clarify what I think you mean, if I have (assume I've correctly fiddled the dicts):

signature
  [ con "<>" $ (<>) @A
  , con "mempty" $ mempty @A
  , con "Nothing" $ Nothing @Int
  ]

QS will not find the monoid laws due to the Int defaulting, but it will find the mempty = Nothing law?

nick8325 commented 4 years ago

Yes, that's right!

isovector commented 4 years ago

Amazing! Thanks for the explanation. I'll see about finding somewhere to document this :)