search

fsharp / fslang-suggestions

The place to make suggestions, discuss and vote on F# language and core library features
345 stars 21 forks source link

Add check constraint to primitive type definition #1189

Closed xp44mm closed 2 years ago

xp44mm commented 2 years ago

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:

Please tick all that apply:

For Readers

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

Happypig375 commented 2 years ago

Aka refinement types.

abelbraaksma commented 2 years ago

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:

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 commented 2 years ago

@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 commented 2 years ago

@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 commented 2 years ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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.