F#: arithmetic operator and loss of polymorphism (value restriction?)

Question

This code doesn't compile:

let f = fun x y -> x <<< y // bit shift
let g = fun x y -> x <<< y

[<EntryPoint>]
let main _ =
  printfn "%d" <| f 1 10
  printfn "%d" <| f 1L 10 // error
  printfn "%d" <| g 1L 10
  0

(7,21): error FS0001: This expression was expected to have type
    int
but here has type
    int64

• http://ideone.com/qktsOb

I guess the unifier fixed the type parameters associated with f and g upon seeing their first occurrences. What governs this process? I think this is very similar to "value restriction" but f and g are already eta-expanded! This is a hard problem.

• http://en.wikipedia.org/wiki/Value_restriction

I would surely imagine there's some black magic behind typing predefined operators with ad-hoc polymorphism over integral types, but that's just my speculation. Any information appreciated.

Policeman

Answer 1

Generic numeric programming is done using static member constraints, which can't be represented in the .NET type system. They exist only in F# and therefore must be marked inline.

Your code could be written this way:

let inline f x y = x <<< y // bit shift
let inline g z y = z <<< y

[<EntryPoint>]
let main _ =
  printfn "%d" <| f 1 10
  printfn "%d" <| f 1L 10 // works too
  printfn "%d" <| g 1L 10
  0

More info on MSDN:
Inline Functions
Statically Resolved Type Parameters

Lemke

I wonder how long it could have took me to find these pages by myself! – Policeman

I would like to expand on this answer, which has actually two parts: 1) Defining a syntactic function instead of a right-hand-side lambda function solves the value restriction problem: let f x y = x <<< y, and 2) the inline solves the operator constraint problem. B.t.w., System.Int32 does not really have a static member op_LeftShift. The F# compiler implicitly augments the type with it, which further complicates type inference. – Khudari

@MarcSigrist I think let f x y = x <<< y is just a syntax sugar for let f = fun x y -> x <<< y. I was just desperate in getting my code compile, so I used the most verbose form trying to get any possible clues. It should be compared against the partial application form let f = (<<<) and this one should be vulnerable to value restriction. – Policeman

@nodakai: There is a meaningful distinction in F# between syntactic functions and function values. Only syntactic functions can be inlined. – Lemke

@Lemke Could you point me towards some in-depth explanation of the difference between syntactic functions and function values? – Prehensible

I would probably start with Automatic Generalization (especially the section on value restriction) on MSDN. This blog post on "the finer points" is also very good. The essence of F#'s behavior is captured by this sentence in the first article: The compiler performs automatic generalization only on complete function definitions that have explicit arguments, and on simple immutable values. – Lemke

Answer 2

I think it is how F# performs automatic generalization of function parameters. On first appearance it infers that the function 'f' could have type ('a -> 'a -> 'a) but the second appearance is not match this signature because it has a different signature ('b -> 'a -> 'a) because it consider int64 and int as different types.

Inlining functions could sometimes solve this problem as @Daniel mentioned

Slightly more info could be found here: http://msdn.microsoft.com/en-us/library/dd233183.aspx

Some more info on static member constraints could be found in this post by Tomas Petricek: http://tomasp.net/blog/fsharp-generic-numeric.aspx/

Renatarenate

"On first appearance it infers that the function f could have type ('a -> 'a -> 'a)" I don't think that is how HM works. HM infers the most general type of a function (a term, in general) just by looking at its definition (body.) (In this case ^a -> int32 -> ^a when ...) – Policeman

Note the difference between my problem and max 2.0 3 in the MSDN page you quoted. My f and g are essentially identical, so when the first and the third line of the body of my main function compile fine, there shouldn't be any reason for the second line not to compile (unless... complications like "static method" are involved.) OTOH the problem with max 2.0 3 is simply that the definition of max itself was not general enough to support such a usage. – Policeman

I'll make time to read through Tomas' article. Thank you very much for the valuable information! – Policeman