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
Generalized Algebraic Data Types (GADTs) are an advanced feature of Rescript's type system. "Generalized" can be somewhat of a misnomer -- what they actually allow you to do is add some extra type-specificity to your variants. Using a GADT, you can give the individual cases of a variant _different_ types.
9
+
Generalized Algebraic Data Types (GADTs) are an advanced feature of ReScript's type system. "Generalized" can be somewhat of a misnomer -- what they actually allow you to do is add some extra type-specificity to your variants. Using a GADT, you can give the individual cases of a variant _different_ types.
10
10
11
11
For a quick overview of the use cases, reach for GADTs when:
12
12
13
-
1. You need to distinguish between different members of a variant at the type-level
13
+
1. You need to distinguish between different members of a variant at the typelevel.
14
14
2. You want to "hide" type information in a type-safe way, without resorting to casts.
15
15
3. You need a function to return a different type depending on its input.
16
16
@@ -32,7 +32,7 @@ type timezone =
32
32
Using this variant type, we will end up having functions like this:
33
33
34
34
```res example
35
-
let convert_to_daylight = tz => {
35
+
let convertToDaylight = tz => {
36
36
switch tz {
37
37
| EST => EDT
38
38
| CST => CDT
@@ -43,22 +43,24 @@ let convert_to_daylight = tz => {
43
43
44
44
This function is only valid for a subset of our variant type's constructors but we can't handle this in a type-safe way using regular variants. We have to enforce that at runtime -- and moreover the compiler can't help us ensure we are failing only in the invalid cases. We are back to dynamically checking validity like we would in a language without static typing. If you work with a large variant type long enough, you will frequently find yourself writing repetitive catchall `switch` statements like the above, and for little actual benefit. The compiler should be able to help us here.
45
45
46
-
Lets see if we can find a way for the compiler to help us out with normal variants. We could define another variant type to distinguish the two kinds of timezone.
46
+
Let's see if we can find a way for the compiler to help us with normal variants. We could define another variant type to distinguish the two kinds of timezone.
47
47
48
48
```res example
49
-
type daylight_or_standard =
49
+
type daylightOrStandard =
50
50
| Daylight(timezone)
51
51
| Standard(timezone)
52
52
```
53
53
54
54
This has a lot of problems. For one, it's cumbersome and redundant. We would now have to pattern-match twice whenever we deal with a timezone that's wrapped up here. The compiler will force us to check whether we are dealing with daylight or standard time, but notice that there's nothing stopping us from providing invalid timezones to these constructors:
55
55
56
56
```res example
57
-
let invalid_tz1 = Daylight(EST)
58
-
let invalid_tz2 = Standard(EDT)
57
+
let invalidTz1 = Daylight(EST)
58
+
let invalidTz2 = Standard(EDT)
59
59
```
60
60
61
-
Consequently, we still have to write our redundant catchall cases. We could define daylight savings time and standard time as two _separate_ types, and unify those in our `daylight_or_standard` variant. That could be a passable solution, but that makes a distinction really would like to do is implement some kind of _subtyping_ relationship. We have two _kinds_ of timezone. This is where GADTs are handy:
61
+
Consequently, we still have to write our redundant catchall cases. We could define daylight savings time and standard time as two _separate_ types, and unify those in our `daylightOrStandard` variant.
62
+
That could be a passable solution, but what we would really like to do is implement some kind of subtyping relationship.
63
+
We have two _kinds_ of timezone. This is where GADTs are handy:
62
64
63
65
```res example
64
66
type standard
@@ -75,7 +77,7 @@ We define our type with a type parameter. We manually annotate each constructor,
75
77
but we've added another level of specificity using a type parameter. Constructors are now understood to be `standard` or `daylight` at the _type_ level. Now we can fix our function like this:
76
78
77
79
```res example
78
-
let convert_to_daylight = tz => {
80
+
let convertToDaylight = tz => {
79
81
switch tz {
80
82
| EST => EDT
81
83
| CST => CDT
@@ -89,7 +91,7 @@ we try to return a standard timezone from this function. Actually, this seems li
89
91
we still want to be able to match on all cases of the variant sometimes, and a naive attempt at this will not pass the type checker. A naive example will fail:
90
92
91
93
```res example
92
-
let convert_to_daylight = tz => {
94
+
let convertToDaylight = tz => {
93
95
switch tz {
94
96
| EST => EDT
95
97
| CST => CDT
@@ -102,7 +104,7 @@ let convert_to_daylight = tz => {
102
104
This will complain that `daylight` and `standard` are incompatible. To fix this, we need to explicitly annotate to tell the compiler to accept both:
103
105
104
106
```res example
105
-
let convert_to_daylight : type a. timezone<a> => timezone<daylight> = // ...
107
+
let convertToDaylight : type a. timezone<a> => timezone<daylight> = // ...
106
108
```
107
109
108
110
`type a.` here defines a _locally abstract type_ which basically tells the compiler that the type parameter a is some specific type, but we don't care what it is. The cost of the extra specificity and safety that GADTs give us is that the compiler is not able to help us with type inference as much.
@@ -127,7 +129,7 @@ let foo = add(Int(1), Int(2))
127
129
let bar = add(Int(1), Float(2.0)) // the compiler will complain here
128
130
```
129
131
130
-
How does this work? The key thing is the function signature for add. The number GADT is acting as a `type witness`. We have told the compiler that the type parameter for `number` will be the same as the type we return -- both are set to `a`. So if we provide a `number<int>`, `a` equals `int`, and the function will therefore return an `int`.
132
+
How does this work? The key thing is the function signature for add. The `number` GADT is acting as a _type witness_. We have told the compiler that the type parameter for `number` will be the same as the type we return -- both are set to `a`. So if we provide a `number<int>`, `a` equals `int`, and the function will therefore return an `int`.
131
133
132
134
We can also use this to avoid returning `option` unnecessarily. This example is adapted from Real World Ocaml, chapter 9. We create an array searching function can be configured to either raise an exception, return an `option`, or provide a `default` value depending on the behavior we want.
133
135
@@ -165,26 +167,26 @@ let flexible_find:
165
167
166
168
## Hide and recover Type information Dynamically
167
169
168
-
In a very advanced case that combines many of the above techniques, we can use GADTs to selectively hide and recover type information. This helps us create more generic types.
170
+
In an advanced case that combines the above techniques, we can use GADTs to selectively hide and recover type information. This helps us create more generic types.
169
171
The below example defines a `num` type similar to our above addition example, but this lets us use `int` and `float` arrays
170
-
interchangeably, hiding the implementation type rather than exposing it. This is similar to a regular variant. However, it is a tuple including embedding a `num_ty` and another value.
171
-
`num_ty` serves as a type-witness, making it
172
-
possible to recover type information that was hidden dynamically. Matching on `num_ty` will "reveal" the type of the other value in the pair.We can use this to write a generic sum function over arrays of numbers:
172
+
interchangeably, hiding the implementation type rather than exposing it. This is similar to a regular variant. However, it is a tuple including embedding a `numTy` and another value.
173
+
`numTy` serves as a type-witness, making it
174
+
possible to recover type information that was hidden dynamically. Matching on `numTy` will "reveal" the type of the other value in the pair.We can use this to write a generic sum function over arrays of numbers:
173
175
174
176
```res example
175
-
type rec num_ty<'a> =
176
-
| Int: num_ty<int>
177
-
| Float: num_ty<float>
178
-
and num = Num(num_ty<'a>, 'a): num
179
-
and num_array = Narray(num_ty<'a>, array<'a>): num_array
177
+
type rec numTy<'a> =
178
+
| Int: numTy<int>
179
+
| Float: numTy<float>
180
+
and num = Num(numTy<'a>, 'a): num
181
+
and num_array = Narray(numTy<'a>, array<'a>): num_array
180
182
181
-
let add_int = (x, y) => x + y
182
-
let add_float = (x, y) => x +. y
183
+
let addInt = (x, y) => x + y
184
+
let addFloat = (x, y) => x +. y
183
185
184
186
let sum = (Narray(witness, array)) => {
185
187
switch witness {
186
-
| Int => Num(Int, array->Array.reduce(0, add_int))
Not only is this quite tedious to write, and quite ugly, but we gain very little from it. The function wrappers even add performance overhead, so we are losing on almost all fronts. If we define subtypes of
216
+
Not only is this quite tedious to write and quite ugly, but we gain very little in return. The function wrappers even add performance overhead, so we are losing on all fronts. If we define subtypes of
215
217
Stream like `Readable` or `Writable`, which have all sorts of special interactions with the callback that jeopardize our type-safety, we are going to be in even deeper trouble.
216
218
217
219
Instead, we can use the same GADT technique that let us vary return type to vary the input type.
@@ -221,7 +223,7 @@ the type signature of the callback and pass this instead of a plain string.
221
223
Additionally, we use some type parameters to represent the different types of Streams.
222
224
223
225
This example is complex, but it enforces tons of useful rules. The wrong event can never be used
224
-
with the wrong callback, but it also will never be used with the wrong kind of stream. The compiler will will complain for example if we try to use a `Pipe` event with anything other than a `writable` stream.
226
+
with the wrong callback, but it also will never be used with the wrong kind of stream. The compiler will complain for example if we try to use a `Pipe` event with anything other than a `writable` stream.
225
227
226
228
The real magic happens in the signature of `on`. Read it carefully, and then look at the examples and try to
227
229
follow how the type variables are getting filled in, write it out on paper what each type variable is equal
@@ -260,35 +262,35 @@ let writer = Stream.Writable.make()
260
262
let reader = Stream.Readable.make()
261
263
// Types will be correctly inferred for each callback, based on the event parameter provided
This example is only over a tiny, imaginary subset of node's Stream API, but it shows a real-life example
279
+
This example is only over a tiny, imaginary subset of Node's Stream API, but it shows a real-life example
278
280
where GADTs are all but indispensable.
279
281
280
282
## Conclusion
281
283
282
-
While GADTs can make your types extra-expressive and get more safety, with great power comes great
284
+
While GADTs can make your types extra-expressive and provide more safety, with great power comes great
283
285
responsibility. Code that uses GADTs can sometimes be too clever for its own good. The type errors you
284
286
encounter will be more difficult to understand, and the compiler sometimes requires extra help to properly
285
287
type your code.
286
288
287
-
However, There are definite situations where GADTs are the _right_ decision
289
+
However, there are definite situations where GADTs are the _right_ decision
288
290
and will _simplify_ your code and help you avoid bugs, even rendering some bugs impossible. The `Stream` example above is a good example where the "simpler" alternative of using regular variants or even strings.
289
291
would lead to a much more complex and error prone interface.
290
292
291
293
Ordinary variants are not necessarily _simple_ therefore, and neither are GADTs necessarily _complex_.
292
294
The choice is rather which tool is the right one for the job. When your logic is complex, the highly expressive nature of GADTs can make it simpler to capture that logic.
293
295
When your logic is simple, it's best to reach for a simpler tool and avoid the cognitive overhead.
294
-
The only way to get good at identifying which the situation calls for is to try out
296
+
The only way to get good at identifying which tool to use in a given situation is to practice and experiment with both.
0 commit comments