5. DeriveGen Signatures: Controlling What Gets Generated

In the previous tutorial, we saw how deriveGen can automatically create generators. But how do we tell it what kind of data we want? For example, should the length of a Vect be given as an argument, or should it be randomly generated?

The answer is the function signature. The signature is not just a type; it is a blueprint of your intent that tells deriveGen exactly what to do.

Our Goal

In this tutorial, we will learn to command deriveGen by writing three different function signatures for the Vect type. By the end of this tutorial, you will have built:

A generator for a Vect of a specific, given length.
A generator that produces a Vect of a random, generated length.
A flexible generator that takes both a given length and an external generator for its elements.

This will give you a deep understanding of how to use signatures to control deriveGen.

Prerequisites

All previous tutorials, especially Measuring Your Test Coverage.

Step 1: The Setup

First, let’s create our file and add the necessary imports. We will be using Vect throughout this tutorial.

Create a new file named `DeriveTutorial.idr`

Add the following boilerplate

This includes the ElabReflection pragma and all the modules we will need.

import Deriving.DepTyCheck.Gen
import Data.Vect
import Data.Fuel

import Test.DepTyCheck.Gen
import System.Random.Pure.StdGen

%language ElabReflection

%hint
genStr : Fuel -> Gen MaybeEmpty String
genStr _ = elements ["a", "b", "c", "d", "f", "g", "h"]

public export
data VectString : (len : Nat) -> Type where
  Nil  : VectString Z
  (::) : (x : String) -> (xs : VectString len) -> VectString (S len)

Show (VectString n) where
  show xs = "[" ++ show' xs ++ "]" where
    show' : forall n . VectString n -> String
    show' Nil        = ""
    show' (x :: Nil) = show x
    show' (x :: xs)  = show x ++ ", " ++ show' xs

Note: For the following steps, you can put all the code in the same DeriveTutorial.idr file and temporarily rename the main function you want to run as main before compiling.

Step 2: Scenario A - Generating a `Vect` of a Given Length

Our first goal is to create a generator that produces a Vect of a specific length that we provide as an argument. To do this, we simply place the argument before the Fuel parameter in the signature.

The signature (n : Nat) -> Fuel -> Gen MaybeEmpty (Vect n String) tells deriveGen: “You will be given a Nat named n. Your job is to produce a Vect of that exact length.”

Define the generator:

genVectOfLen : Fuel -> (n : Nat) -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty (VectString n)
genVectOfLen = deriveGen

Let’s write a main function to call our generator, providing 5 as the length.

runVect : IO ()
runVect = do
  putStrLn "--- Generating a Vect of a given length (5) ---"
  Just v <- pick (genVectOfLen (limit 10) 5)
    | Nothing => printLn "Generation failed"
  printLn v

The output will show a Vect that always has exactly 5 elements, filled with random strings from the default String generator.

Compile and run:

--- Generating a Vect of a given length (5) ---
["a", "b", "c", "d", "e"]
The length is: 5

By placing n before Fuel, you have successfully commanded deriveGen to use it as a fixed input.

Step 3: Scenario B - Generating a `Vect` of a Random Length

What if we don’t want to provide a specific length? What if we want the generator itself to invent a random length? To do this, we use a dependent pair in the return type.

The signature Fuel -> Gen MaybeEmpty (n ** Vect n String) tells deriveGen: “Your job is to first generate a random Nat (which you will call n), and then generate a Vect of that length. When you are done, give me back both n and the Vect.”

Define the generator:

genRandomVect : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty (n ** VectString n)
genRandomVect = deriveGen

This time, when we call the generator, we don’t provide a length. The generator will produce a pair containing the length it chose and the vector it created.

Prepare a test for it:

runRandomVect : IO ()
runRandomVect = do
  putStrLn "--- Generating a Vect of a random length ---"
  for_ (the (List Int) [1..3]) $ \_ => do
    Just (n ** v) <- pick (genRandomVect (limit 10))
      | Nothing => printLn "Generation failed"
    printLn n
    printLn v

You will see vectors of different, random lengths each time you run it.

Compile and run:

--- Generating a Vect of a random length ---
3
["a", "b", "c"]
0
[]
5
["d", "e", "f", "g", "h"]

By moving the parameter n from an input to a generated part of the output using the ** syntax, you have completely changed deriveGen’s behavior.

Step 4: The Flexible Generator - Combining Patterns

Let’s combine the patterns we’ve learned. Our first generator is flexible enough: it is taking a Nat as a given input, but it is also taking an external generator hint for the element type using the => syntax which will be overridden by the following exapmple.

To call this generator, we must provide both the length n and an element generator via the @ syntax.

Prepare a test for it:

runFlexi : IO ()
runFlexi = do
  putStrLn "--- Generating a Vect of length 7 with overridden Str generator ---"
  let myStrGen = \fuel => elements ["A", "B", "C"] -- Our custom generator for the elements
                                                   -- It is created manually, so no need to use `fuel`.

  Just v <- pick (genVectOfLen (limit 10) 7 @{myStrGen})
    | Nothing => printLn "Generation failed"
  printLn v

  Just v' <- pick (genVectOfLen (limit 10) 7 @{genStr})
    | Nothing => printLn "Generation failed"
  printLn v'

Compile, run, and observe

You will see a Vect of length 7, filled with numbers between 100 and 200, proving that deriveGen correctly used both your given length and your external generator.

--- Generating a Vect of length 7 with overridden Str generator ---
["A", "C", "B", "A", "A", "A", "C"]
["b", "c", "f", "a", "b", "b", "h"]

Next Steps

Now that you know how to control deriveGen through signatures, you are ready for more advanced topics:

Want to understand how recursion affects generation? Continue to Beyond Fuel: Structural Recursion to learn about SpendingFuel vs StructurallyDecreasing recursion.
Want to generate types with proof constraints? Continue to Generating GADTs with Proofs to see how deriveGen handles types like SortedList.