Add check constraint to primitive type definition

[xp44mm]

I propose we ...

Add a check constraint to the type definition to further examine the primitive type. Inspired by partial active patterns and sql check constraint.
example 1:

type Natural = int & (<=) 0
let sum(i:Natural) = List.sum [0 .. i]

sum -1 // fail
sum 3 // 6

The type Natural is still a primitive type int, but it's value need to be successfully checked by additional check constraints ((<=) 0).
example 2:

type State = string & ((=)"On"|(=)"Off")
let value(st:State) = match st with "On" -> 0 | "Off" -> 1

value "On" //0 
value "xx" //fail

Note that the check constraint is a logical expression. An expression consists of many operands, which is a 't->bool function. The operator of the expression should include AND(&), OR(|) and NOT(!).

example 3:
complex type

type Point =
    {
        state:string &((=)"On" | (=)"Off")
        x:int & (<=) 0 & (>=) 999 
    }

let p = {state="xx";x=0} // fail

example 4:

The check constraint is expanded to type annotation.

let sum(i:int & (<=) 0) = ..
let value(st:string & ((=)"On"|(=)"Off")) = ..

Obviously, & and | are overload here. They may conflict with pattern matching.

The existing way of approaching this problem in F# is ...

example 1:

let sum(i:int) = 
    if 0 <= x then () else failwith ""
    List.sum [0 .. i]

example 2:

let value(st:string) = 
    if st = "On" || st = "Off" then () else failwith ""
    match st with "On" -> 0 | "Off" -> 1

example 3:

type Point =
    {
        state:string
        x:int
    }

   static member from(state,x)=
        if state = "On" || state = "Off" then () else failwith ""
        if x >= 0 && x<= 999 then () else failwith ""
        {state=state;x=x}

Pros and Cons

The advantages of making this adjustment to F# are ...

The disadvantages of making this adjustment to F# are ...

Extra information

Estimated cost (XS, S, M, L, XL, XXL):

Related suggestions: (put links to related suggestions here)

Affidavit (please submit!)

Please tick this by placing a cross in the box:

• This is not a question (e.g. like one you might ask on stackoverflow) and I have searched stackoverflow for discussions of this issue
• I have searched both open and closed suggestions on this site and believe this is not a duplicate
• This is not something which has obviously "already been decided" in previous versions of F#. If you're questioning a fundamental design decision that has obviously already been taken (e.g. "Make F# untyped") then please don't submit it.

Please tick all that apply:

• This is not a breaking change to the F# language design
• I or my company would be willing to help implement and/or test this

For Readers

If you would like to see this issue implemented, please click the 👍 emoji on this issue. These counts are used to generally order the suggestions by engagement.

[Happypig375]

Aka refinement types.

[abelbraaksma]

This probably belongs in F*. in fact, it is already in there. See here for downloads and a discussion on refinement types as researched for F7: https://www.microsoft.com/en-us/research/project/f7-refinement-types-for-f/.

I have searched both open and closed suggestions on this site and believe this is not a duplicate

You may have missed it, but there are several:

• Language Validation/Constraint Support For Types #939 (refinement types)
• Language Validation/Constraint Support For Types #1155 (discussion of 939)
• Allow Getters and Setters for Record Field Validation #516 (similar to refinement types through get/set on records)

As you can read in the other discussions, it's been declined before.

Also, you may want to read this comment, it suggests ways to prevent yourself from spending a lot of time on writing a suggestion by first discussing it in F# Slack/SO/FSharp.org forums etc. You should, of course, then link-back to these discussions from your proposal, which will help people understand the context.

[Happypig375]

@abelbraaksma @dsyme How feasible is it to incorporate F7 into the F# compiler? Will it be too esoteric (though this arguably is a missing piece in domain modelling along with anonymous unions)? Too complicated to maintain?

[dsyme]

@abelbraaksma @dsyme How feasible is it to incorporate F7 into the F# compiler? Will it be too esoteric (though this arguably is a missing piece in domain modelling along with anonymous unions)? Too complicated to maintain?

It's not really feasible I'm afraid, though such an integration might make a good student project?

[cartermp]

I think this is probably worth closing -- refinement types are very cool, but they open up the language into an entirely different style of programming that's proof-oriented. While interesting and certainly necessary in some domains, I don't think the overall direction of F# is heading towards formal verification. Limiting this only to primitive types would result in an experience that feels like it has lots of gaps compared to what people working in those domains expect, creating tension to push F# further down the road of being a proof-oriented language.

[woojamon]

Is that such a bad thing though? Isn't a "proof" of correct behaviors what teams are trying to accomplish by writing tests? I'd love stronger compile time verification of our business rules... would save having to write all those tests.

[cartermp]

It's neither bad nor good, but F# is not (and likely will never be) a proof-oriented language. If you're interested in formal verification, languages such as Coq and F* are much better-suited.

[T-Gro]

Is that such a bad thing though? Isn't a "proof" of correct behaviors what teams are trying to accomplish by writing tests? I'd love stronger compile time verification of our business rules... would save having to write all those tests.

To add onPhillip's (good) response, you can still define and consume types like NaturalNumber, NonEmptyArray, NonEmptyString etc. in today's F# and many teams do for the exact reasons you listed. There is of course the overhead of having to write boilerplate for protection, construction and unwrapping of the value, but that is code which is easily testable and rarely needs to change.
I also believe that the boilerplate around it could be solved by writing a Myriad plugin.

The part where I am not aware of any F#-automated solution, but also the most difficult part about constrained types, is how they propagate throughout common operations. Only a way-richer type system could (?) help here, at the moment this has to be written by hand.
Examples of what I mean by common operations:

NaturalNumber (+) NaturalNumber -> NaturalNumber
NaturalNumber (-) NaturalNumbner -> int

filter predicate NonEmptyArray -> array
groupBy f NonEmptyArray -> NonEmptyArray<'a,NonEmptyArray>

[xp44mm]

The part where I am not aware of any F#-automated solution, but also the most difficult part about constrained types, is how they propagate throughout common operations.

no to propagate, Test only when explicitly declared, not at other times. Other times it is treated the same as the base type.

let value(s:string & ((=)"On"|(=)"Off")) = 
    s + s // return string type value

[abelbraaksma]

no to propagate, Test only when explicitly declared, not at other times. Other times it is treated the same as the base type.

Why? That would lead to highly unpredictable code. You don't add extra safety to lose it the moment you use it, then you could just as well not have the feature to begin with. Don't forget that F# is statically type-safe. If we improve the type system, we'd do it everywhere, or not at all.

Consider Phillip's suggestion, if you're interested in this kind of thing, in particular, I can recomment "Coq", it's great, quote:

If you're interested in formal verification, languages such as Coq and F* are much better-suited.

[xp44mm]

Why?

Defensive programming for external data and non-defensive programming for internal data. Immutable data only needs to be checked once when it is created. If validated, it makes no difference whether the data type is a string type or a kind of stricter string types .

[abelbraaksma]

Immutable data only needs to be checked once when it is created.

Oh, absolutely! I didn't mean anything else. But data can be mapped, or the constructor can be used as a function, it can be inlined, it can be made external, or the logic can be part of an interface. Also, users can opt-in to use mutable, which we should possibly disallow in this case, which means special-casing a million situations. And then there's deconstruction, which can happen everywhere a pattern is allowed. That's what was meant with "across the board" and "to propagate". The change proposed here is extremely hard to implement in a resilient way (see the F* implementation for reference and extrapolate that to the much larger code base of F#).

[xp44mm]

Also, users can opt-in to use mutable, which we should possibly disallow in this case, which means special-casing a million situations. And then there's deconstruction, which can happen everywhere a pattern is allowed.

No to propagate means that any operation is returned to the base type.

match "On" : string & ((=) "On" | (=) "Off") with
| x -> x.GetType().Name // return string

He only verifies once the value at the explicit type annotation. equals:

match (fun x -> if ((=) "On") x || ((=) "Off") x then x else failwith "ill") x with
| x -> x.GetType().Name // return string

[abelbraaksma]

No to propagate means that any operation is returned to the base type.

Ehm, I think you meant the opposite? It means that we maintain the (check constraint) type information across the board, so that the compiler can check. If we don't and turn it into, say, a string, we cannot enforce anything and we loose everything we'd like to gain from this feature.

While the compiler may erase that information ultimately in compiled binaries (like it does with UoM), which would mean GetType() in your example above says it's a System.String. while compiling, it needs to maintain that information.

I.e.:

[<Measure>]
type cm

let x = 10<cm>
let f() = x + 10  // error
let g() = x.GetType() // returns System.Int32
let h() = 10<cm> * 3
let apply f = f()
let apply h  // propagated, returns int<cm>

That's what was meant above with propagation. The type information of the restricted types becomes part of the TAST and, even though it may be erased ultimately, it must be propagated to have any meaningful application.

Other languages support this feature and they do exactly that. It is a good feature, but just out of scope for F# (it is not a proving language like Coq). However, you may be interested in the ongoing discussions on type-erased unions. It is not the same, but allows you to have types like type Foo = string | int | decimal. There, too, the type propagation is what makes it so hard to integrate.

[xp44mm]

The unit of measurement provides additional useful information that needs to be propagated, while the verification information is discarded out of the box, and the data itself already says that the verification passes.

I modified the previous comment, please see the equivalent code.

"On" : string & ((=) "On" | (=) "Off")
// ==
(fun x -> if ((=) "On") x || ((=) "Off") x then x else failwith "ill") "On"

[abelbraaksma]

Well, then I’m sorry, then I don’t understand and don’t really see the value. Doesn’t make sense to me to special case something like that with any orthogonality or support from the compiler.