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
Static types gives you a consistent vocabulary you can use to communicate an API's contract to client developers. What must client code do in order to make a valid method or function call? What guarantees can client code rely on? <ahref="/encapsulation-and-solid">Encapsulation</a>, in other words.
421
421
</p>
422
+
<insdatetime="2025-01-20">
423
+
<p>
424
+
<strong>P.S. 2025-01-20:</strong>
425
+
</p>
426
+
<p>
427
+
For a type-level technique for modelling the relationship between rod size and price list, see <ahref="/2025/01/20/modelling-data-relationships-with-f-types">Modelling data relationships with F# types</a>.
image_alt: "A box labelled 'library' with a 'sandbox' area inside. To its left, another box labelled 'Client code' with an arrow to the library box, as well as an arrow to a box inside the sandbox area labelled 'Client computation'."
The overall idea should look familiar to practitioners of statically-typed functional programming. Instead of plain functions and data structures, we introduce a special 'context' in which we have to run our computations. This is similar to how <ahref="/2023/01/09/the-io-monad">the IO monad</a> works, or, in fact, most monads. You're not supposed to <ahref="/2019/02/04/how-to-get-the-value-out-of-the-monad">get the value out of the monad</a>. Rather, you should inject the desired behaviour <em>into</em> the monad.
97
97
</p>
98
98
<p>
99
-
We find a similar design with existential types, or with the <ahref="https://hackage.haskell.org/package/base/docs/Control-Monad-ST.html">ST monad</a>, on which the ideas in the GDP paper are acknowledged to be based. We even see a mutation-based variation in the article <ahref="/2024/06/24/a-mutable-priority-collection">A mutable priority collection</a> where we may consider the <code>Edit</code> API a variation of the ST monad, since it allows 'localized' state mutation.
99
+
We find a similar design with existential types, or with the <ahref="https://hackage.haskell.org/package/base/docs/Control-Monad-ST.html">ST monad</a>, on which the ideas in the GDP paper are acknowledged to be based. We even see a mutation-based variation in the article <ahref="/2024/06/24/a-mutable-priority-collection">A mutable priority collection</a>, where we may think of the <code>Edit</code> API as a variation of the ST monad, since it allows 'localized' state mutation.
The <code>trySize</code> member function issues a <code><spanstyle="color:#2b91af;">Some</span><spanstyle="color:#2b91af;">Size</span><<spanstyle="color:#2b91af;">'a</span>></code> if the <code>candidate</code> is within the size of the price array. As discussed above, we can't completely avoid a run-time check, but now that we have the proof, we don't need to <em>repeat</em> that run-time check if we wanted to use a particular <code>Size</code> value with the same <code>PriceList</code>.
164
+
The <code>trySize</code> member function issues a <code><spanstyle="color:#2b91af;">Some</span><spanstyle="color:#2b91af;">Size</span><<spanstyle="color:#2b91af;">'a</span>></code>value if the <code>candidate</code> is within the size of the price array. As discussed above, we can't completely avoid a run-time check, but now that we have the proof, we don't need to <em>repeat</em> that run-time check if we wanted to use a particular <code>Size</code> value with the same <code>PriceList</code>.
165
165
</p>
166
166
<p>
167
-
Notice how immutability is an essential part of this design. If, in the object-oriented manner, we allow a price list to change, we could make it shorter. This could invalidate some proof that we previously issued. Since, however, the price list is immutable, we can trust that once we've checked a size once, it remains valid. You can also think of this as a sort of <ahref="/encapsulation-and-solid">encapsulation</a>, in the sense that once we've assured ourselves that an object, or here rather a value, is valid, it remains valid. Indeed, <ahref="/2024/06/12/simpler-encapsulation-with-immutability">encapsulation is simpler with immutability</a>.
167
+
Notice how immutability is an essential part of this design. If, in the object-oriented manner, we allow a price list to change, we could make it shorter. This could invalidate some proof that we previously issued. Since, however, the price list is immutable, we can trust that once we've checked a size, it remains valid. You can also think of this as a sort of <ahref="/encapsulation-and-solid">encapsulation</a>, in the sense that once we've assured ourselves that an object, or here rather a value, is valid, it remains valid. Indeed, <ahref="/2024/06/12/simpler-encapsulation-with-immutability">encapsulation is simpler with immutability</a>.
168
168
</p>
169
169
<p>
170
170
You probably still have some questions. For instance, how do we ensure that a size proof issued by one price list can't be used against another price list? Imagine that you have two price lists. One has ten prices, the other twenty. You could have the larger one issue a proof that <em>size 17</em> is valid. What prevents you from using that proof with the smaller price list?
You may consider the <code>cut</code> function a 'secondary' issuer of <code><spanstyle="color:#2b91af;">Size</span><<spanstyle="color:#2b91af;">'a</span>></code> proofs, since it returns such values. If you wanted to call <code>cut</code> again with one of those values, you could.
223
223
</p>
224
224
<p>
225
-
Compared to the previous article, I don't think I changed much else in the <code>cut</code> function than the initial function declaration, and the last line of code, but for good measure, here's the entire function:
225
+
Compared to the previous article, I don't think I changed much else in the <code>cut</code> function, besides the initial function declaration, and the last line of code, but for good measure, here's the entire function:
The <code>cut</code> function is part of the same module as <code><spanstyle="color:#2b91af;">Size</span><<spanstyle="color:#2b91af;">'a</span>></code>, so even though the constructor is <code>private</code>, the <code>cut</code> function can still use it.
250
250
</p>
251
251
<p>
252
-
Thus, the entire proof mechanism is for external use. Internally, the library code may take shortcuts, so it's up to the library author to convince him or herself that the contract holds. In this case, I'm quite confident that the function only issues valid proofs. After all, I've lifted the algorithm from <ahref="/ref/clrs">an acclaimed text book</a>, and this particular implementation is covered by more than 10,000 test cases.
252
+
Thus, the entire proof mechanism is for external use. Internally, the library code may take shortcuts, so it's up to the library author to convince him- or herself that the contract holds. In this case, I'm quite confident that the function only issues valid proofs. After all, I've lifted the algorithm from <ahref="/ref/clrs">an acclaimed text book</a>, and this particular implementation is covered by more than 10,000 test cases.
253
253
</p>
254
254
<h3id="dcbcbee557a54a8aaa701484ad89e90f">
255
255
Proof-based solve API <ahref="#dcbcbee557a54a8aaa701484ad89e90f">#</a>
As the paper describes, the GDP trick hinges on rank-2 polymorphism, and the only way (that I know of) this is supported in F# is on methods. An object is therefore required, and we define the abstract <code><spanstyle="color:#2b91af;">PriceListRunner</span><<spanstyle="color:#2b91af;">'r</span>></code> class for the purpose.
335
+
As the paper describes, the GDP trick hinges on rank-2 polymorphism, and the only way (that I know of) this is supported in F# is on methods. An object is therefore required, and we define the abstract <code><spanstyle="color:#2b91af;">PriceListRunner</span><<spanstyle="color:#2b91af;">'r</span>></code> class for that purpose.
336
336
</p>
337
337
<p>
338
338
Client code must implement the abstract class to call the <code>runPrices</code> function. Fortunately, since F# has <ahref="https://learn.microsoft.com/dotnet/fsharp/language-reference/object-expressions">object expressions</a>, client code might look like this:
F# only supports rank-2 polymorphism in method definitions, which makes consuming a GDP API more awkward than in Haskell. The need to create a new type, and the few lines of boilerplate that entails, is a drawback.
441
441
</p>
442
442
<p>
443
-
Even so, the GDP trick is a nice addition to your functional tool belt. You'l hardly need it every day, but I personally like having some specialized tools lying around together with the everyday ones.
443
+
Even so, the GDP trick is a nice addition to your functional tool belt. You'll hardly need it every day, but I personally like having some specialized tools lying around together with the everyday ones.
444
444
</p>
445
445
<p>
446
446
But wait! The reason that F# has support for rank-2 polymorphism through object methods is because C# has that language feature. This must mean that the GDP technique works in C# as well, doesn't it? Indeed it does.
0 commit comments