drvink commented 6 years ago

Check well-formedness of `let rec` bindings

Some checking is currently performed at compile time to reject incorrect recursive value bindings:

let rec a = b + 1
and b = a + 1
(*
error FS0031: This value will be eventually evaluated as part of its own definition.
You may need to make the value lazy or a function.
Value 'a' will evaluate 'b' will evaluate 'a'.
*)

However, F# handles recursive value bindings via lazy initialization (this is transparent: the user need not explicitly use lazy; see §14.6.6 of the F# 4.0 specification) and issues FS0040 to warn of potential runtime failure:

warning FS0040: This and other recursive references to the object(s) being defined
will be checked for initialization-soundness at runtime through the use of a delayed
reference. This is because you are defining one or more recursive objects, rather
than recursive functions.

While such a group of bindings may be well-formed, little checking is done to ensure otherwise:

let rec x : int = (fun () -> x) ()
(*
System.InvalidOperationException: ValueFactory attempted to access the Value property
of this instance.
   at System.Lazy`1.CreateValue()
   at System.Lazy`1.LazyInitValue()
   at System.Lazy`1.CreateValue()
   at System.Lazy`1.LazyInitValue()
   at <StartupCode$FSI_0002>.$FSI_0002.main@()
Stopped due to error
*)

Recent work in OCaml (see ocaml/ocaml#556) detects and rejects such programs as malformed. The difficulty of ensuring the correctness of recursive bindings containing non-function values in ML has long been known, the BDFL himself having contributed to relevant research [1].

Pros and Cons

The advantages of making this adjustment to F# are: improved safety and closing a known soundness issue.

The disadvantages of making this adjustment to F# are: like anything, it's more work.

Extra information

Estimated cost (XS, S, M, L, XL, XXL): probably between L and XL, given the sensitivity of the work, the need to determine how it relates/translates to F#, and actual implementation; though, were it to be done, the OCaml fixes appear to only reject programs that ought not to have ever been accepted anyway, so there are no obvious drawbacks.

Affidavit (please submit!)

[x] This is not a question (e.g. like one you might ask on stackoverflow) and I have searched stackoverflow for discussions of this issue
[x] I have searched both open and closed suggestions on this site and believe this is not a duplicate
[x] 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.
[x] This is not a breaking change to the F# language design
[x] I or my company would be willing to help implement and/or test this

[1] Syme, D. (2006). Initializing Mutually Referential Abstract Objects: The Value Recursion Challenge. Electronic Notes in Theoretical Computer Science, 148(2), pp.3-25.

drvink commented 6 years ago

N.B. this is intentionally filed as a "suggestion" rather than an issue, since the language spec clearly defines the present behavior, though presumably a well-tested PR from the community would not be rejected should one be submitted (barring discussion otherwise as to why things should be kept as-is).

dsyme commented 6 years ago

In 10+ years of F# I've not seen an actual initialization bug that would be caught by any additional checking we could, practically speaking do.

Sample bugs would be welcome.

drvink commented 6 years ago

I wouldn't even describe it as a priority issue (for me, anyway), more something that might have been of interest to you given your previous work.

There were real bugs in OCaml which this improved check fixed (see Yallop's first post in the linked PR)--since we already have a check that warns of potential unsoundness in the constructs that crashed in OCaml, the improvement we would get would be that such code would instead be rejected entirely, i.e. users wouldn't be able to shoot themselves in the foot with something definitely incorrect. The amount of work needed to get there is maybe not worth it other than out of purism, though, given the unlimited number of other fish to fry :)

jdh30 commented 4 years ago

Here's a sample bug:

https://github.com/fsharp/fsharp/issues/867

I just tried it in the latest F# in VS2019 and it still crashes. I just hit a similar bug in production where I get a null reference exception which I fixed with an innocuous refactoring (and I don't understand why that would fix anything).

BillHally commented 4 years ago

@jdh30 I've added a comment to the issue you linked to explaining why the problem there is due to recursion during printing to the console by fsi rather than a bug in rec bindings (which means it's not a sample bug for this issue).

gusty commented 4 years ago

I just came across a case that compiles fine, not even a warning but throws a null reference at runtime, bypassing the null protection of the type system, here's a simplified repro:

type A = { Value : A }

let rec a = { Value =  b }
and b     = { Value =  a }

results in

type A = { Value: A }
val a : A = { Value = null }
val b : A = { Value = { Value = null } }

I think this should be either fixed or prohibited. At the very least a warning should be emitted in cases like this.

dsyme commented 2 years ago

Linking https://github.com/dotnet/fsharp/pull/12936, which contains some bug fixes in this area.

We won't specifically extend the language specification here, but I agree the case above should be fixed. I will check it is covered in https://github.com/dotnet/fsharp/pull/12936

fsharp / fslang-suggestions