I don't think it is a good long term design decision to partially replicate Sampleable functionality in a second type class that lives next to it. To me the two sensible choices seem to be:

• Either we just drop Arbitrary entirely and build a deriving handler for Sampleable that, at least for now, uses the id shrinker function.
• SampleableExt is refactored to be based on both Arbitrary and Shrinkable

can you explain why you went for neither of those?

Thanks -- both are good suggestions!

For context, this PR is part of a broader project to replicate Rocq QuickChick's functionality for deriving generators that produce data satisfying user-defined inductive predicates (this PR is spun off this repo).

Part of this broader project involves defining a ArbitrarySuchThat typeclass:

/-- Generators of type `α` such that `P : α -> Prop` holds for all generated values.
    Note that these generators may fail, which is why they have type `OptionT Gen α`. -/
class ArbitrarySuchThat (α : Type) (P : α → Prop) where
  arbitraryST : OptionT Gen α

For simplicity / ease of comparison with QuickChick, I tried to make the derived generators in ArbitrarySuchThat be as close as possible to the generators produced by QuickChick, which resulted in me adopting the same typeclass definitions as QuickChick. (I also wanted to avoid modifying Plausible internals, which is why I adopted to make Arbitrary its own typeclass instead of re-factoring SampleableExt directly.)

This was useful for rapid prototyping, but I agree with you that it's a bad idea to have Arbitrary replicate some of SampleableExt's functionality.

I think the best solution moving forward might be to refactor SampleableExt to be based on both Arbitrary and Shrinkable -- this makes the design more modular and separates the generation/shrinking logic. What do you think?

What makes this typeclass different from Plausible.Random Id?

Ah sorry, this is an easy question; Arbitrary is a version of Random with a "size" parameter.

Yep, you're correct! Having a dedicated typeclass for generation (Arbitrary) allows us to maintain a similar design to Haskell QuickCheck & Rocq QuickChick and makes it easier to refer to the generators for a particular type in the body of derived generators.

makes it easier to refer to the generators for a particular type in the body of derived generators.

Is Plausible.Random.random really any harder to refer to than Arbitrary.arbitrary? Maybe let's resolve the size argument issue below before continuing.

Ah yes, you're right -- thanks! Random Id is basically the same as Arbitrary.

(The following explanation is purely for my own understanding / for documentation purposes)

Plausible.Random.random has type RandGT g m α. If we set g = StdGen and m = Id, then unfolding definitions gives us:

RandGT StdGen Id α
≡ RandG StdGen α            -- since for any `g`, we have `RandG g := RandGT g Id`
≡ Rand α                             -- by definition of `Rand`

Gen α is defined as ReaderT (ULift Nat) Rand α, so under the hood, Arbitrary.arbitrary, which has type Gen α is using the same Rand α random generator as Plausible.Random.random.

I guess in this case, the main benefit of having an Arbitrary typeclass is that it maintains the same naming convention as Haskell QuickCheck (which one could argue is somewhat tenuous), and that Arbitrary serves as an abbreviation for Random Id, which may make the deriving infrastructure easier to implement (Random Id is a partially-applied typeclass whereas Arbitrary isn't).

If you want to go that route, I'd suggest abbrev Arbitrary α := Random Id α.

Note that the idea in Random m α is that some types such as Expr are much easier to sample in interesting ways in MetaM. It's totally fair to declare the m a distraction and specialize to Id in this Pr, but I think creating a brand new typeclass is a bad idea.

Ah that's fair, thanks for the suggestion! I'll defer to @hargoniX on whether to keep Arbitrary since we were discussing in another thread above whether to keep Arbitrary as a new typeclass or to refactor the existing SampleableExt typeclass.

Doesn't Gen already have this size parameter built in?

Yep, you're correct that Gen already has a size parameter built-in! However, when deriving proofs of soundness + completeness for the derived generators (which we're currently working on in a separate PR), as observed in Generating Good Generators for Inductive Relations (POPL 2018), it is convenient to have a separate typeclass which makes the generator's size parameter explicit (i.e. ArbitrarySized in this PR). Specifically, section 5.1 of the paper discusses how the semantics of Gen (in Rocq QuickChick, but a similar argument can be made for Plausible generators) are defined by the set of values that are generated for a particular size parameter, and how reasoning about monotonicity with respect to generators' size parameter leads to natural specifications for generator combinators.

But to be clear, this is currently defined as arbitrarySized : Nat -> ULift Nat -> Plausible.Rand α (after unfolding), where both Nats are the size. If you genuinely have two different sizes at play, then the docstring should distinguish them.

Are you sure that our Gen corresponds to the one QuickCh(e|i)ck and not to something else? Right now your Arbitrary is a generator with one size argument, and ArbitrarySized is a generator with two size arguments, which seems like an off-by-one-error.

Ah you're right, sorry, I missed that Gen contains an ULift Nat argument after unfolding -- thanks for the heads-up! In this case, the Nat parameter in (what is currently called) ArbitrarySized acts more like fuel -- the derived ArbitrarySized generator recurses on this Nat parameter and terminates when the Nat is 0.

I've renamed ArbitrarySized to ArbitraryFueled and updated the docstrings -- hopefully that's ok!

What does "terminates" mean? Does this mean that if sampling random elements of List Nat, then this will sample both smaller Nats and smaller Lists? I think this might already be the intended semantics of the ULIft Nat argument, and so you might want just arbitrarySized : Gen α

Ah, by "terminates", I mean that the generator picks one of the values in its base case to return. As an example, here is the generator that is derived for a binary tree datatype:

inductive Tree
  | Leaf : Tree
  | Node : Nat → Tree → Tree → Tree

-- Derived code below
-- (The code for the derived generator closely follows the generator that Rocq QuickChick derives)
instance : Plausible.ArbitraryFueled Tree where
      arbitraryFueled :=
        let rec aux_arb (fuel : Nat) : Plausible.Gen Tree :=
          match size with
          | Nat.zero => Plausible.Gen.oneOfWithDefault (pure Tree.Leaf) [(pure Tree.Leaf)]
          | size' + 1 =>
            Plausible.Gen.frequency (pure Tree.Leaf)
              [(1, (pure Tree.Leaf)),
                (fuel' + 1,
                  (do
                    let a_0 ← Plausible.Arbitrary.arbitrary
                    let a_1 ← aux_arb fuel'
                    let a_2 ← aux_arb fuel'
                    return Tree.Node a_0 a_1 a_2))]
        fun fuel => aux_arb fuel

When fuel = 0, we just return a Leaf.

For the List Nat example, the generator would just return the empty list when fuel = 0.

If you start with a SampleableExt, does this instance with the next one produce an equivalent SampleableExt? If not, then there should not be such an instance loop.

Thanks -- good catch! I removed this instance since it's not strictly necessary (all tests pass without this instance).

A function that creates an n-ary and from an array of terms seems potentially useful, but a combinator to create an if doElem doesn't.

Ah that's fair, thanks -- I've removed the TSyntaxCombinators.lean file altogether since the combinators there are of dubious utility for this PR.

then set it when you detect it is recursive.

It's better design not to duplicate logic, where it's implemented in slightly different ways each time. The source of truth is this loop.

Thanks, this is a very good point! Adopted this change.

Shouldn't recursive mean that ctorType contains ctorName anywhere?

Option.isSome <| ctorType.find? (·.isConstOf inductiveName)

This would admit some more possibilities than what the deriving handler actually allows however.

Thanks -- I removed the Utils.lean file altogether since this function is no longer strictly necessary. (This function was used in the parent project to analyze constructors of inductive Props when deriving generators of values satisfying the Prop, which is outside the scope of this PR.)

On a more general note, are you sure it is you that has copyright here and not AWS, given that you are being paid?

I previously asked @codyroux and he said to put my name here (we've received permission to open-source this code). I'll double check with him!

I'll check.