Idioms/Practices for Implementing Constrained Numeric Types in F#?

Question

Suppose one needs a numeric data type whose allowed values fall within a specified range. More concretely, suppose one wants to define an integral type whose min value is 0 and maximum value is 5000. This type of scenario arises in many situations, such as when modeling a database data type, an XSD data type and so on.

What is the best way to model such a type in F#? In C#, one way to do this would be to define a struct that implemented the range checking overloaded operators, formatting and so on. A analogous approach in F# is described here: http://tomasp.net/blog/fsharp-custom-numeric.aspx/

I don't really need though a fully-fledged custom type; all I really want is an existing type with a constrained domain. For example, I would like to be able to write something like

type MyInt = Value of uint16 where Value <= 5000 (pseudocode)

Is there a shorthand way to do such a thing in F# or is the best approach to implement a custom numeric type as described in the aforementioned blog post?

Condemn

If you're looking for full-fledged value dependent types you might check out F*. – Lagrange

Answer 1

You're referring to what are called refinement types in type theory, and as pointed out by Daniel, look for F*. But it is a research project.

As far as doing it with F#, in addition to Tomas' post, take a look at the designing with types series.

Preponderant

Answer 2

My suggestion would be to implement a custom struct wrapping your data type (e.g., int), just as you would in C#.

The idea behind creating this custom struct is that it allows you to "intercept" all uses of the underlying data value at run-time and check them for correctness. The alternative is to check all of these uses at compile-time, which is possible with something like F* (as others mentioned), although it's much more difficult and not something you would use for everyday code.

Conventional

How would that work since a struct has a default constructor which allows validation to be bypassed? – Lagrange

Others members of the struct -- e.g., custom operators -- should validate the struct as well. So if you use the default value for the struct, you won't immediately know it's invalid, but you'll find out the first time you use the value. – Conventional

That seems strange since the point of defining a type is to ensure certain guarantees about the data. – Lagrange

Maybe so, but sometimes you have to make compromises in practice. With this technique, you still get those guarantees -- the compromise is that you potentially won't know right away when the type's invariants are violated. I find that as long as you know this possibility exists when you start writing the code, I'm extra careful about making sure no default values can find their way into the core code. – Conventional