You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
@@ -6,79 +6,155 @@ But what if you have a custom data type that needs a special, handwritten genera
6
6
7
7
## Our Goal
8
8
9
-
We will define a `SpecialString` newtype and write a custom generator for it. We will then create a larger `User` type that contains a `SpecialString` and see how `deriveGen` automatically discovers and integrates our manual generator without any special syntax.
9
+
In this tutorial, you will:
10
+
11
+
1. Define a custom type with a handwritten generator
12
+
2. Mark that generator with `%hint` for automatic discovery
13
+
3. See `deriveGen` automatically find and use your generator without explicit passing
14
+
4. Compare implicit (`%hint`) vs explicit (`@{...}`) generator passing
15
+
16
+
You will see output like:
17
+
18
+
```text
19
+
--- Testing mixed generation ---
20
+
MkUser (MkSpecialString "root") 5
21
+
```
22
+
23
+
---
10
24
11
25
## Prerequisites
12
26
13
-
This tutorial assumes you have completed [Tutorial 5: DeriveGen Signatures](t05-derivegen-signatures.md).
27
+
- Completion of [Tutorial 5: DeriveGen Signatures](t05-derivegen-signatures.md)
28
+
- Understanding of the `=>` syntax for explicit generator constraints
29
+
- Idris2 source file `./src/Mixed.idr` with the header:
30
+
31
+
```idris
32
+
import Test.DepTyCheck.Gen
33
+
import Data.Fuel
34
+
import Deriving.DepTyCheck.Gen
35
+
import System.Random.Pure.StdGen
36
+
37
+
%language ElabReflection
38
+
```
14
39
15
40
---
16
41
17
-
## Step 1: A Type That Needs a Custom Generator
42
+
## Step 1: Define Types and a Handwritten Generator
18
43
19
44
Imagine we have a `SpecialString` type that should only ever contain specific, predefined values (e.g., usernames with special privileges). A fully random `String` generator is not appropriate here.
20
45
21
-
1.**Create a new file** named `Mixed.idr`.
46
+
### Create a new file named `Mixed.idr`.
22
47
23
-
2.**Define the types and a handwritten generator.**
48
+
### Define the `SpecialString` type with a `%hint` generator.
24
49
25
-
```idris
26
-
module Mixed
50
+
```idris
51
+
-- A type that needs special generation
52
+
data SpecialString = MkSpecialString String
27
53
28
-
import Test.DepTyCheck.Gen
29
-
import Test.DepTyCheck.Runner
30
-
import Data.Fuel
54
+
Show SpecialString where
55
+
show (MkSpecialString s) = "MkSpecialString \{show s}"
We have defined `genSpecialString` to only produce three possible values. Notice it has the standard `Fuel -> Gen MaybeEmpty ...` signature.
65
+
```idris
66
+
-- Standard domain types
67
+
data User = MkUser SpecialString Nat
68
+
69
+
Show User where
70
+
show (MkUser s i) = "MkUser (\{show s}) \{show i}"
71
+
```
72
+
73
+
🔍 **Notice:**
74
+
75
+
- Signature `Gen MaybeEmpty SpecialString` (no `Fuel ->`) is used for manually defined generators
76
+
- The `%hint` pragma marks `genSpecialString` for **auto-implicit search** in Idris 2. It makes this function a candidate for automatic insertion - no explicit `@{genSpecialString}` required!
77
+
78
+
From Idris 2 docs: `%hint` marks functions for auto search, similar to unnamed type class instances. The compiler prioritizes these hints during unification when explicit arguments are absent.
79
+
80
+
---
43
81
44
-
## Step 2: Automatic Derivation Finds the Manual Generator
82
+
## Step 2: Create the Derived Generator
45
83
46
84
Now, let's define a generator for `User` using `deriveGen`. A `User` contains a `SpecialString` and a `Nat`. `deriveGen` knows how to generate a `Nat` by default. What will it do for `SpecialString`?
47
85
48
-
1. **Add the derived generator** to `Mixed.idr`.
86
+
### Add the derived generator to `Mixed.idr`.
49
87
50
-
```idris
51
-
%language ElabReflection
88
+
```idris
89
+
-- Add deriveGen for the User
90
+
genUser : Fuel -> (Fuel -> Gen MaybeEmpty SpecialString) => Gen MaybeEmpty User
91
+
genUser = deriveGen
92
+
```
52
93
53
-
-- Add deriveGen for the User
54
-
genUser : Fuel -> Gen MaybeEmpty User
55
-
genUser = deriveGen
56
-
```
94
+
🔍 **Notice:**
57
95
58
-
2. **Test it in the REPL.** Load your `Mixed.idr` file.
96
+
- Automatic derivation by `deriveGen` requires `Fuel ->`
97
+
- The constraint `(Fuel -> Gen MaybeEmpty SpecialString) =>` tells `deriveGen` it needs a generator for `SpecialString`
98
+
- Normally, you'd pass it explicitly: `genUser @{genSpecialString} fuel`. But `%hint` enables automatic resolution - Idris finds and inserts `genSpecialString` automatically!
99
+
100
+
---
101
+
102
+
## Step 3: Test the Generator
103
+
104
+
Let's create a main function to see our automatic discovery in action.
105
+
106
+
### Add a test function to `Mixed.idr`.
107
+
108
+
```idris
109
+
main : IO ()
110
+
main = do
111
+
putStrLn "--- Testing mixed generation ---"
112
+
Just u <- pick (genUser (limit 10))
113
+
| Nothing => putStrLn "Generation failed"
114
+
printLn u
115
+
```
116
+
117
+
### Compile and run.
118
+
119
+
```bash
120
+
pack build Mixed && pack exec Mixed
121
+
```
122
+
123
+
Expected output (will vary):
124
+
125
+
```text
126
+
--- Testing mixed generation ---
127
+
MkUser (MkSpecialString "root") 5
128
+
```
129
+
130
+
---
59
131
60
-
```idris
61
-
:exec pick1 (genUser (limit 10))
62
-
-- MkUser (MkSpecialString "root") 5 : User
132
+
## When to Use %hint?
63
133
64
-
:exec pick1 (genUser (limit 10))
65
-
-- MkUser (MkSpecialString "admin") 12 : User
66
-
```
134
+
`Constraint + %hint` approach is recommended for custom types.
67
135
68
-
It works! `deriveGen` automatically found and used our `genSpecialString` function when it needed to produce a `SpecialString`. It did this simply by looking for a function in the current scope with the required type signature (`... -> Gen ... SpecialString`).
136
+
**Pattern:** Mark your generator with `%hint`, add constraint to derived generator:
69
137
70
-
## When to Use Implicit vs. Explicit (`=>`) Generation
138
+
```idris
139
+
%hint
140
+
genMyType : Gen MaybeEmpty MyType
141
+
genMyType = map MkMyType (elements ["a", "b"])
71
142
72
-
`DepTyCheck` now offers two ways to combine generators:
1. **Implicit (this tutorial):** `deriveGen` automatically finds a generator in scope for a specific custom type (`SpecialString`).
75
-
* **When to use:** This is the best method when you have a custom data type and you *always* want to use one specific generator for it.
147
+
**Call site:**
148
+
```idris
149
+
pick (genContainer fuel) -- No @{...} needed!
150
+
```
76
151
77
-
2. **Explicit (`=>` syntax):** As seen in Tutorial 4, you can add a `(Fuel -> Gen MaybeEmpty String) =>` constraint to the signature.
78
-
* **When to use:** This is best when you want to provide a generator for a *primitive* or *built-in* type (like `String`, `Nat`, `List`), or when you want the caller to be able to supply *different* generators in different contexts.
152
+
**Best for:** Custom types where you want automatic discovery with explicit dependencies in the signature.
79
153
80
154
---
81
155
82
156
## Next Steps
83
157
84
-
* **Continue to the next tutorial:** [Generating GADTs with Proofs](t10-generating-gadts-with-proofs.md) to see how these techniques apply to even more advanced types.
158
+
***Continue to the next tutorial:**[Generating GADTs with Proofs](t10-generating-gadts-with-proofs.md) to see how these techniques apply to even more advanced types with proof constraints.
159
+
***Experiment:** Try creating your own custom type with a `%hint` generator and see if `deriveGen` finds it automatically.
160
+
***Read more:** Check out the Idris 2 documentation on `%hint` for advanced auto-implicit search patterns.
0 commit comments