Dependent Types for F#
I&#x27;m very much a newbie when it comes to F# but as far as I can tell this isn&#x27;t an example of what&#x27;s traditionally called dependent types, but rather is a way of providing a set of helper functions and types for &quot;smart&quot; constructors, that is providing a validation&#x2F;verification function that takes in some raw type and gives back an option of either the type you want or none.<p>As a litmus test (and I&#x27;d be happy if either the OP or someone else chimes in), as an example of dependent types, I&#x27;d expect to be able to compose constraints, e.g. having a type called<p><pre><code>    And&lt;&#x27;A, &#x27;B&gt;
</code></pre>
and<p><pre><code>    Or&lt;&#x27;A, &#x27;B&gt;
</code></pre>
that would then let me compose constraints e.g.<p><pre><code>    And&lt;GreaterThan3, IsEven&gt;
</code></pre>
and crucially <i>have their verification functions automatically compose as well</i>, instead of having to invent a whole new type<p><pre><code>   GreaterThan3AndIsEven
</code></pre>
with a whole new verification function.<p>As far as I can tell right now, that&#x27;s not possible with this library and I need to go down the route of making the custom GreaterThan3AndIsEven type.<p>Another good litmus test is whether literals also need to be passed through the verification function or not (or whether you have to pass them through the verification, get an option, and then unwrap the option with a comment indicating that it&#x27;s safe to do so); for a usage of dependent types I would expect the answer to be no usage of the verification function would be required.<p>The crucial thing that dependent types let you do is that you can manipulate types and values with many of the same tools. Composition (the and and or from above) is one hallmark of this ability. Another is being able to call a value-level function in a type signature. For example a type signature that looks like<p><pre><code>    x : if (a + b == c) then Boolean else Int
</code></pre>
FWIW I don&#x27;t mean to take away from this library; the practice of using smart constructors is something I&#x27;d love all expressively statically typed languages embrace wholeheartedly.