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?

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.

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.