1. The Generator Monad: Your First Generator

Welcome to DepTyCheck! This tutorial is a hands-on guide that will help you learn the most important skill in property-based testing: generating random test data.

We will keep things practical and focus on what you need to get started. You’ll write code, run it, and see the results immediately.

Our Goal

In this tutorial, we will guide you step by step to create a generator for the following UserProfile data type:

data UserProfile = MkProfile String Nat

By the end, you will have a working program that produces random user profiles, like this:

MkProfile "Alice" 37 : UserProfile

Prerequisites

This tutorial assumes you have completed Installation and First Steps and have a working Idris 2 installation with DepTyCheck configured for your tutorial.ipkg.

Step 1: Your First Generator

Let’s start by creating a generator that always produces the same value. This will confirm our setup is working.

Create a new file named `Tutorial.idr`

import Test.DepTyCheck.Gen
import Data.Vect

%language ElabReflection

Add the following code to it. We’ll define our data type and import the necessary `DepTyCheck` modules

data UserProfile = MkProfile String Nat

Show UserProfile where
  show (MkProfile s y) = "MkProfile " ++ show s ++ " " ++ show y

-- A generator that always produces the same, constant user profile
genConstantUser : Gen1 UserProfile
genConstantUser = pure (MkProfile "Alice" 30)

Note

The pure function creates the simplest possible “recipe”: one that always returns the exact value you give it. The type Gen1 means this generator is guaranteed to produce a value.

Run your generator

To test your first generator lets do the following:

echo -e ':exec printLn =<< pick1 genConstantUser' |
    rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr

Here we do:


`echo -e` and `\|`	We are going to run Idris2 in REPL mode, pass the input, wait for the output and close
`:exec`	It is actually the Idris2 REPL command to run something in `IO` monad. For `:exec ?wat` the `?wat` is `IO _`.
`printLn =<<`	Runs generator and prints output. `:exec` alone drops results; this shows them.
`pick1 genConstantUser`	We are very close, that’s what is needed.
`rlwrap`	Not strictly needed for single runs, but reminds that Idris2 REPL lacks readline support
`pack`	DepTyCheck depends on a set of libraries, so, `pack` launches `idris2` with the full set of required things
`--extra-args="--no-banner"`	Reduces REPL output noise. Passes flag to hide Idris2 welcome banner
`repl`	It actually instructs `pack` to run `idris2` in REPL mode

You will see an output, similar to the following:

MkProfile "Alice" 30

You’ve just created and run your first generator! Now, let’s make it more interesting by adding some randomness.

Step 2: Adding Randomness

Instead of a fixed age, let’s generate a random one. We’ll use the choose function for this.

Modify your file to create a new generator

-- A generator for a user with a random age between 18 and 99
genRandomAgeUser : Gen1 UserProfile
genRandomAgeUser = MkProfile "Alice" <$> choose (18, 99)

Here’s what’s new:

choose (18, 99) creates a recipe for picking a random number in that range.

Note

The choose function randomly picks between two generators with equal probability (50/50). This gives you a simple way to add variation to your generators.

The <$> operator takes the result from the recipe on the right (our random number) and feeds it into the function on the left (MkProfile "Alice").

Run it multiple times

echo -e ':exec printLn =<< pick1 genRandomAgeUser' |
    rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr

echo -e ':exec printLn =<< pick1 genRandomAgeUser' |
    rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr

This time, you’ll see a different result with each run:

MkProfile "Alice" 22
MkProfile "Alice" 35

Success! You’ve introduced randomness into your data.

Step 3: Combining Two Random Generators

Now, let’s make the name random too. We need to combine two different random recipes.

Add a new generator that combines a random name and a random age

-- A generator for a user with a random name and a random age
genUserProfile : Gen1 UserProfile
genUserProfile = MkProfile <$> elements ["Alice", "Bob", "Charlie"] <*> choose (18, 99)

Here’s the change:

elements ["Alice", "Bob", "Charlie"] creates a recipe for picking a random name from a list.
The <*> operator is the key: it lets us combine two recipes. It runs the name recipe and the age recipe, then feeds both results into MkProfile.

Run your new generator a few times

echo -e ':exec printLn =<< pick1 genUserProfile' |
    rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr

echo -e ':exec printLn =<< pick1 genUserProfile' |
    rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr

You’ll now see completely random user profiles!

MkProfile "Alice" 33
MkProfile "Bob" 47

Step 4: Choosing Between Generators

What if you want to generate more varied data? For example, maybe you want to generate a user who is either an “Admin” or a “Guest”, with “Guest” being more common.

DepTyCheck provides oneOf for equal choices and frequency for weighted choices.

Add these new generators to your file

-- A generator for a user role, with each role having an equal chance
genRole : Gen1 String
genRole = oneOf [pure "Admin", pure "User", pure "Guest"]

-- A generator for a user type, where "Standard" is 4x more likely than "Premium"
genUserType : Gen1 String
genUserType = frequency [ (4, pure "Standard"), (1, pure "Premium") ]

oneOf takes a list of generators and chooses one of them with equal probability.
frequency takes a list of (weight, generator) pairs. The weights determine the probability. Here, there are 5 total “parts” (4+1), so “Standard” has a 4/5 chance and “Premium” has a 1/5 chance.

Run them in the REPL

echo -e ':exec printLn =<< pick1 genRole' |
    rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr

echo -e ':exec printLn =<< pick1 genUserType' |
    rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr

Sample output:

"Guest"
"Standard"

If you run pick1 genUserType many times, you will notice that "Standard" appears much more often than "Premium".

Step 5: Dependent Generation

So far, the random values we’ve generated (name, age) have been independent of each other. But what if the type of one value needs to depend on the value of another?

This is the core challenge of generating dependent types. For example, let’s generate a pair containing a random length n and a Vect that has exactly n elements. The type Vect n Bool depends directly on the value n.

This is called dependent generation. We must first generate n, and then use that value to create a generator for a vector of that specific type. We use do notation for this.

Add this generator to `Tutorial.idr`. It will create a dependent pair `(n ** Vect n Bool)`

-- A generator for a dependent pair: a random length `n` and a vector of that length
genDependentVect : Gen1 (n ** Vect n Bool)
genDependentVect = do
    n   <- choose (1, 5) -- Step 1: Generate a random length `n`
    vec <- vectOf {n} (elements [True, False]) -- Step 2: Generate a vector of that exact length
    pure (n ** vec) -- Step 3: Package them into a dependent pair with (**)

This do block is a sequence of dependent instructions:

n <- choose (1, 5): A random Nat is generated. Let’s say the result is 3.
vec <- vectOf {n} ...: Because n has the value 3, this line creates and runs a generator for the type Vect 3 Bool. We have to pass it as a named argument because it is used at the type definition of vectOf.
pure (n ** vec): The value 3 and the generated vector (e.g., [True, False, True]) are bundled into a dependent pair using the ** constructor.

Run it in the REPL:

echo -e ':exec printLn =<< pick1 genDependentVect' |
    rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr

For multiple times the output might be:

(3 ** [False, False, False])
(5 ** [True, True, True, True, True])
(2 ** [True, False])

Notice that the length of the vector in the output always matches the number next to it. This powerful technique is what allows DepTyCheck to generate valid data for complex, dependent types.

Step 6: Generating a Collection

Finally, let’s generate a list of test users. You can use the listOf combinator to run your generator multiple times and collect the results.

Add one last generator to your `Tutorial.idr` file

-- A generator that produces a list of 5 random user profiles
genFiveUsers : Gen1 (List UserProfile)
genFiveUsers = listOf {length=pure 5} genUserProfile

The listOf function takes a length generator (which we provide as a constant 5), and creates a new recipe that runs the generator how a provided length generator generated times.