Idioms / Practice implementing limited number types in F #?

Suppose you need a numeric data type whose valid values ​​fall in the specified range. More specifically, suppose you want to define an integral type whose minimum value is 0 and the maximum value is 5000. This type of scenario occurs in many situations, for example, when modeling a database data type, XSD data type, etc.

What is the best way to simulate this type in F #? In C #, one way to do this is to define a structure that implements checking the range of overloaded operators, formatting, and so on. A similar approach is described here in F #: http://tomasp.net/blog/fsharp-custom-numeric.aspx/

I really don't need a full-fledged user type; all i really want is an existing type with a limited domain. For example, I would like 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 this the best approach to implementing a custom number type as described in the aforementioned blog post?

+7
f # refinement-type
source share
2 answers

You mean what is called a type of refinement in type theory, and, as Daniel pointed out, find F * . But this is a research project.

As for F #, in addition to the Tomas post, look at designing with types .

+3
source share

My suggestion was to implement a custom structure that carries your data type (e.g. int ), just like in C #.

The idea of ​​creating this custom structure is that it allows you to “intercept” all use of the underlying data value at run time and check for correctness. An alternative is to check all of these applications at compile time, which is possible with something like F * (as mentioned above), although this is much more complicated and not what you would use for everyday code.

+3
source share

All Articles