Correctness of `bindS`

[bolt12]

I've been thinking about the correctness of bindS and if there was any way to prove that if for a data type a, (Bounded a, Enum a) are well defined than the following holds:

natVal (Proxy :: Proxy (Count a)) == length [minBound .. maxBound]

(where Count can be a type-family similar to the one I use in my LAoP library, that counts all possible inhabitants of a data type)

Or even better: ensure that all the possible inhabitants of a are present in [minBound .. maxBound] or [minBound ..], we could safely say that under this restrictions a Selective is equivalent to a (less efficient) Monad.

The problem is that we cannot assure that an end user, for some custom type, will implement Bounded and Enum correctly. For example one could have the following instances:

data Const1 = One | Two deriving (Show)

instance Bounded Const1 where
  minBound = One
  maxBound = One

instance Enum Const1 where
  toEnum _ = One

  fromEnum One = 1
  fromEnum Two = 2

For this type instances [minBound..] would give an infinite list of Ones and [minBound .. maxBound] would give the list [One]. We cannot rely on the end user to provide type instances that compel with the semantic we are looking for...

I guess that if the instances are derived by GHC one can assume they're at least correct wrt the semantics we are looking for, right? With this in mind I found generic-deriving and I think it pretty much offers the invariants we are looking for: GEnum a respects | a | == length genum and also genum has all possible inhabitants of a, through generics. This is good because we are not limited to (Enum a, Bounded a) constraints, which GHC can only derive for data types which have one or more nullary constructors. Which means that, unless someone overwrites the type instance, function bindS is correct.

I tried to work on a PR but it boils down to changing casesEnum for casesGEnum :: GEnum a => Cases a and I was not able to get rid of the partial fromRight on bindS, although I am confident that we can assure that it will not fail.

What do you think about this @snowleopard ? This is are all informal claims but can be seen as a step forward :)

[bolt12]

I made something that mimicks in a simpler way what generic-deriving does but without the fairness in the case of the List type:

• AllValues.hs
• AllValuesPolished.hs

[snowleopard]

@bolt12 Many thanks for sharing your thoughts and experiments!

I agree with your conclusion: we can't really prove much without assuming that instances are lawful.

In the next few weeks, I'm planning to introduce some changes to the Selective type class, following the results I got for multi-way selective functors:

https://github.com/snowleopard/selective/blob/4f378fe673a1ec1c42a469b9df5c87a7ae7ecd3c/src/Control/Selective/Multi.hs#L151-L152

After these changes, bindS will no longer be inefficient, and will no longer require partial functions:

https://github.com/snowleopard/selective/blob/4f378fe673a1ec1c42a469b9df5c87a7ae7ecd3c/src/Control/Selective/Multi.hs#L171-L172

So, I suggest not to do any changes to bindS for now. Let's come back to this discussion once the refactoring is complete!

[bolt12]

Very cool! So basically you have generalization of Coproducts (or types with tags/disjunctive unions) and defend that if you have a computation that produces a value with a tag you can match (deconstruct a la either(?)) that tag and do what you are supposed to do, right?

I really liked the parallel you do with the Applicative type class being the same but restrict t to have only One tag!

And I noticed that you still need Enum/Enumerable constraint on the Selective type class. Maybe we could use GEnum constraint as I said above in order to maybe have a more robust solution.

This is interesting and I wonder what type of changes are you going to introduce, are you going to replace Selective entirely for Multi? Are you going to use Multiunderneath Selective and write, for example, an unpartial version of bindS? I also have some questions:

(Regarding Multi.hs)

• I'm having a hard time understanding why do we need Enum a for the Selective version of bindS and then for the Monad class an unconstrained version suffices, why is this?
• Do Multiway Selective functors still benefit from speculative execution? It seems that with this approach they simply offer conditional static analysis capabilities!

[snowleopard]

Thank you, glad you liked it :-)

Maybe we could use GEnum constraint as I said above in order to maybe have a more robust solution.

For now, I'd like to stick to Enum for simplicity, but I might consider something safer at some point.

This is interesting and I wonder what type of changes are you going to introduce, are you going to replace Selective entirely for Multi?

My current plan is to add the method match to Selective, defining something like matchDefault that provides an inefficient implementation based on select for cases where the efficiency doesn't matter.

I'm having a hard time understanding why do we need Enum a for the Selective version of bindS and then for the Monad class an unconstrained version suffices, why is this?

It comes from the Enum a constraint on the Enumerable (Many a) instance. It's indeed a bit hidden and, at first, I was also a bit confused about where it comes from :-)

Do Multiway Selective functors still benefit from speculative execution?

Yes! The only difference is that now if you statically see a match with N branches, you can decide if you really want to speculatively execute all N branches, knowing that only one of them is going to be needed in the end. Perhaps, it makes sense to speculate only for small values of N.

[bolt12]

Awesome, got it! Thank you :smile: