Derive proof of completeness for derived generators

[AlgebraicWolf]

Currently, there is a strong reasons to believe that derived generators are (intensionally) complete - in our case, this means that in the tree representing a derived generator for certain type (for each value of this type) there exists a leaf node that contains this value. However, there is no proof that this completeness holds. For correctness reasons, it might be useful to derive a proof of intensional completeness along with the generator.

[buzden]

It definitely is a necessary thing. And since I have already thought quite something about this problem a while ago, I'll try to summarise those thoughts here (not necessarily all at once).

Raw generators

First of all, it looks like completeness proof of our current generators must assume completeness of raw generators.

Alternatively, we can consider that this proof would be a variant of implication of completeness of some raw generators to a completeness of our generators, but this looks extremely hard since no raw generators are visible outside the type of a generator.

Type of the proof

Honest way

In the simplest form the completeness proof should look like *for this particular generator of type a for any value x of type a there is a way to get it from the generator. I call this the honest form of the completeness property.

Since running of our generators involves a random seed, the realisation of the completeness property could look like this:

0 Complete : Gen a -> Type
Complete g = (x : a) -> (seed ** runGen g seed = x)

if we had a function runGen : Gen a -> Seed -> a.

Or at least the resulting type could be (seed ** runGen g seed = Just x) if the resulting type of runGen was Maybe a, considering that generators can be empty.

Generality problem

The problem is that our generators runner unGen is polymorphic of any MonadRandom, and thus if we could formulate a pure function like runGen above, it would mean that our property is formulated only for a particular pure MonadRandom implementation, like random-pure which means that this completeness is not so complete.

But this is not the hardest problem.

Problems for pure

Even if we would agree that our completeness property involves only particular pure MonadRandom implementation,
the honest form would mean a bit more. It not only means that we theoretically can get any value of an appropriate type from a generator, it means that a series of pseudo-random values definitely can line up to provide any value. This property involves particular pseudo-random algorithm and particular way of using it, say, in unGen function. This variant of property is too intensional for our generators, it looks too deep into the implementation. Anyway, this is no feasible to try to build a reverse function for a realistic pseudo-random algorithm.

Proposed solution (discussible)

So, my idea was to abstract over implementation, assuming some reasonable properties for external stuff. Say, assuming that we can get any Fin n from any point of time in any MonadRandom, we can be sure that OneOf of complete generators is complete.

Having that, we can formulate a type for completeness property which describes each separate constructor of Gen type separately.

Say, if Gen a is defined like

data Gen : Type -> Type where
  Empty : Gen a
  Pure : a -> Gen a
  Raw : (MonadRandom m => m a) -> Gen a
  OneOf : List (Gen a) -> Gen a
  Bind : Gen a -> (a -> Gen b) -> Gen b

we can consider the property in the following form:

data Complete : Gen a -> Type where
  NoElems : Not a -> Complete Empty
  SingleElem : ((x, y : a) -> x = y) -> Complete $ Pure x
  AssumeRaw : Complete $ Raw sf
  Choose : Either (All Complete gs, ?composite_compl) -> Complete $ OneOf gs
  Chain : Complete lhs -> ((x : a) -> Complete $ rhs x) -> Complete $ Bind lhs rhs

(we need to think what to write instead of ?composite_compl to express a situation when OneOf of several non-complete generators produce a complete generator)

Having property in this form, we need several separate properties proving that, say map and <*> preserve completeness.

Further

Like in #57 with emptiness characteristic, we can try to add completeness property to the type of Gen itself. Then, in any combinator there will be a need to think of when completeness is preserved or gained (which, I'm afraid, would blow signatures a lot).

[AlgebraicWolf]

Alternative approach to specifying completeness, assuming for now that we don't have (or care about) Raw generators, would be to do the following:

1. Specify a special type describing descent down the generator tree, of form data GenPath : Gen a -> Type
2. Having this type, we can have a deterministic version of unGenDeterministic : (g : Gen a) -> GenPath g -> Maybe a
3. Then the completeness property for generator g can be specified as a type isomorphic to a function of signature (x : a) -> (p : GenPath g ** unGenDeterministic g p === x)

[spcfox]

Another option is to use something similar to what @buzden described in Honest way, but with a special predictable MonadRandom. There's no need to build an inverse function for it because it doesn't involve actual randomness. Instead, it will act as a model that, depending on the seed, can generate any sequence of choices, like an ideal random generator. The seed can be based on or represented by a GenPath.

0 Complete : Gen a -> Type
Complete g = (x : a) -> (seed ** runGen g seed predictableRandom = x)

[AlgebraicWolf]

Additionally, instead of supplying a predictable implementation of MonadRandom, would be to instead figure out what notion of fairness does one need to impose upon the MonadRandom, and to write the proof in a conditional manner: given the proof of RNG fairness, we can show that our generator is complete. In this case, writing such proof for a special MonadRandom should be fairly easy, and with more complex generators one can find it sufficient to squint really hard at the fairness condition and at the generator, and conclude that it should, hopefully, hold.

Moreover, the fairness condition would also have a connection to GenPath representation: fairness should entail, for any path in a generator tree, existence of a seed that realizes that path.