[RFC FS-1071] Discussion - Quotations to contain witness information

[dsyme]

This is the discussion thread for https://github.com/fsharp/fslang-design/blob/master/FSharp-5.0/FS-1071-witness-passing-quotations.md

[dsyme]

There is an open question in this RFC which I wanted to record.

The question is to do with witnesses for "built in" constraint solutions which do not have a corresponding direct .NET method to represent a solution.

For example

    let inline f x = x  + x
    <@ f 3 @>

The call to f needs a solution for the op_Addition constraint for integers. The quotation doesn't report the witness for the solution, which is the core issue the RFC is solving. However what's the witness?

Now, because .NET IL metadata is somewhat silly it doesn't actually contain a static member op_Addition on System.Int32. Instead, the F# compiler has forever pretended that this method exists and solves the constrain as a "Builtin". During codegen of .NET code the code is inlined and ends up emitting the appropriate IL opcode.

There are about 500 of these type-specialized primitives in FSharp.Core (roughly speaking corresponding to all the various cases of +, -, *, Abs, Sin and so on).

Ideally, for quotations, CallWithWitnesses on <@ f 3 @> should report a lambda term with an implementation of Int32 addition, and likewise for all the other ~500 cases.

However, there are not really any readily available non-generic entry points in netstandard.dll or FSharp.Core.dll that implement all these type-specialized primitives: e.g. it's hard to find a single method we can call to add two numbers, let alone all the other corresponding primitives.

It seems the right thing to do to ensure that FSharp.Core exposes sufficient implementations of these witness primitives (prim-types already contains these implementations as code, but doesn't expose them).

Remember, the aim of this PR is for quotations to provide "accurate" witnesses for primitives. If they do, then quotations become "semantically complete" w.r.t. using inline SRTP code and processing quotations is much less error prone.

[7sharp9]

I had an issue which might be similar where I was creating a quotation that referenced an SRTP function but I was then calling that function with different generic parameters and using the LeafExpressionConverter to evaluate it, the end result was method not implemented due to the inline method not existing. /cc @kevmal

[dsyme]

I had an issue which might be similar where I was creating a quotation that referenced an SRTP function but I was then calling that function with different generic parameters and using the LeafExpressionConverter to evaluate it, the end result was method not implemented due to the inline method not existing. /cc @kevmal

Yes, that is essentially the problem that this whole RFC is solving at the foundational level.

[krauthaufen]

Hey, I ran into the same problems implementing constant-folding in FShade and having access to the inlined code would certainly help (or even just IL instructions would be better than nothing).

I actually tried to parse the optdata / sigdata files at runtime to resolve these SRTP calls, but I couldn't get my head around it.
Wouldn't it be nice to have the solver for these available at runtime?

This would boil down to a reflection-utility like MethodInfo.TrySolveSRTP : Type[] -> Choice<Expr, InlineIL> and maybe some others for identifying SRTP methods, etc.

Is that totally insane or do you see any chance to make this work?
Cheers

[dsyme]

The question is to do with witnesses for "built in" constraint solutions which do not have a corresponding direct .NET method to represent a solution.

I have resolved this in the implementation by using the corresponding LanguagePrimitives "Dynamic" method as the witness, e.g. op_Addition gets a witness that calls the unconstrained LanguagePrimitives.AdditionDynamic. Some new Dynamic implementations are added for some traits that didn't previously have them.

[NinoFloris]

@dsyme would it make sense to do these calls as constrained calls to structs (no allocs, JIT can fully inline) instead of FSharpFuncs for something simple as '+'? Or do you think this area is edge case enough not to worry too much? It'd be a shame not to have brought it up and be stuck with it :)

[gusty]

@dsyme At some point you might consider to remove simulated members from the internals of the F# compiler.

Maybe when extension members are visible to SRTP you can use that instead.

[eiriktsarpalis]

I'm not sure I understand the purpose of the "WithWitnesses" method is, it looks like a trivial eta expansion on the supplied lambda. Is it simply meant to provide optional debug information or is there something more to it?

[dsyme]

I'm not sure I understand the purpose of the "WithWitnesses" method is, it looks like a trivial eta expansion on the supplied lambda.

That's true if the implementation of the method is just to immediately invoke the constraint, e.g.

        let inline foo (x: ^T) = (^T : (static member Foo : ^T -> ^T) (x))

However for something like "List.sumBy" the implementation has no constraint invocations at all and the witnesses are passed to List.sumBy$W which in turn passes them on to the primitives like Operators.op_Addition$W.

(The WithWitnesses has changes to $W in the latest PR, I'll adjust the RFC)

[dsyme]

@dsyme At some point you might consider to remove simulated members from the internals of the F# compiler.

I'm not sure what you mean here - do you mean removing methods from FSharp.Compiler.Private.dll to reduce size, or something else?

[gusty]

The F# compiler internally uses static optimizations to pretend some primitive types have certain static method, as you said before, float pretends it has (+), Abs, Sin and so on.

Once you have Extension members visible to trait calls, you won't need that any longer, you can use normal extension methods instead.