[RFC FS-1071] Witnesses passing for trait-constraints w.r.t. quotations

[dsyme]

Implementation for RFC FS-1071 - Witness passing for quotations using SRTP-constrained functions and methods

F# quotations of code using SRTP constraint trait calls don't contain sufficient information to represent the semantic intent of the code. Specifically the quotations are missing any record of the resolution of SRTP constraints or how to execute constraint calls.

This RFC addresses this problem by incorporating the necessary information into both quotations and the code laid down for dynamic interpretation of quotations.

Continuation of #6345

[cartermp]

@dsyme given the outstanding TODOs should this be marked as WIP?

[dsyme]

@dsyme given the outstanding TODOs should this be marked as WIP?

Yes. The core of the work is cracked but there are some painful edge cases (super-rare, but they should still be dealt with)

[cartermp]

The diff in prim-types is enormous. Is that intended?

[dsyme]

The diff in prim-types is enormous. Is that intended?

@cartermp We need to discuss this. I'm torn about a few things in this RFC and its implementation but in my heart I know that it is logically the right thing and (roughly speaking) the right way to solve this problem at the core.

I'll try to capture the issues in the RFC and then lets discuss. Basically to make interpreting quotations smooth and reliable we need some kind of executable witnesses for all the "built in" ops we've traditionally compiled away through inlining code down to IL ops. There are many more of these than might be appreciated, e.g. left shift operations on all the integer sizes, etc. etc.

By an executable witness I mean a method we can call at runtime to perform a primitive operation corresponding the satisfaction of a primitive constraint. For example, if the "left shift" operator is called in unsigned 16 bit integers we need a method we can call to actually do that left shift. If the UInt16 type actually had the left shift operation defined on it then it would be easy. But it doesn't.

There are (to some extent) executable witnesses available for (some of) these in the .NET core libraries but there is nothing systematic.

It's a really nasty problem - but quotations will never be a fully reliable basis for meta-programming in the presence of SRTP operations like + and - (including the use of quotations for compile-time meta-programming when writing type providers) until we get a grip on this fundamental issue.

It could be we could continue to rely on adhoc resolution in clients of quotation processors for "built in" cases and only use the witness passing for the more nasty unresolvable cases where only the F~ compiler knows the answer. But considerthis code in a quotation consumer:

https://github.com/dotnet/fsharp/pull/6810/files#diff-5ce60fdfe5066ce67d7dd5d354792434R514-R548

or this

https://github.com/fsprojects/FSharp.TypeProviders.SDK/blob/master/src/ProvidedTypes.fs#L14153-L14737

where 600+ lines are required to list out the different cases in every consumer of quotations, when in contrast you could instead just process a single case of CallWithWitnesses where the quotation contains the answer and a method to call:

https://github.com/dotnet/fsharp/pull/6810/files#diff-5ce60fdfe5066ce67d7dd5d354792434R650

[dsyme]

@cartermp I've simplified the change to prim-types so it doesn't add anywhere near as many new public methods, see fsharp/fslang-design#357 (comment)

[dsyme]

I've now resolved all the open outstanding design issues for this PR, updated the testing and updated the RFC.

It's a significant chunk of work and I've been working to minimize the diff. I can probably minimize it a bit further (there are some useful cosmetic changes in IlxGen.fs and Linq.fs which I could minimize further).

I'd appreciate an initial cosmetic review at some point to help guide me to make another iteration.

[dsyme]

I've also had a chance to talk this whole RFC over with @eiriktsarpalis, and he confirms it would have been useful for any of his prior working with quotations.

[dsyme]

Yay, this one is green at last. I've added the "Candidate for F# 5" label

[cartermp]

@dsyme note that we're using that label for work that is no longer WIP - ready for review with aim to merge and release in a preview. The vNext label might be more appropriate at this stage.

[cartermp]

Ah I see you've removed the WIP

[dsyme]

@dsyme note that we're using that label for work that is no longer WIP - ready for review with aim to merge and release in a preview. The vNext label might be more appropriate at this stage.

Yes, this is ready for review. I'd expect an iteration or two but I've nothing more specific to do on it

[TIHan]

Did another round of review. Only a few nits and questions.
Everything seems to be working as intended when I was playing around with it.

I think once the nits and questions are resolved I will mark this as approved and can be merged. :)

// cc @cartermp @dsyme @jonsequitur

[dsyme]

I think once the nits and questions are resolved I will mark this as approved and can be merged. :)

resolved! :)

[KevinRansom]

The code looks good, not sure I understand how it all goes together.

[TIHan]

@dsyme @cartermp There a few more nits + questions that I had.

[dsyme]

I fixed the build break here

[dsyme]

@TIHan My apologies for missing so many of your comments! I've addressed them all now

[TIHan]

It looks great! Excited to get this in.

[cartermp]

From March 20th 2019 until June 6th 2020 - hooray!

[dsyme]

@alfonsogarciacaro asked this:

@dsyme I was hoping that this or #6810 would extend the TypedTree with information that could help Fable (or other compilers) resolve the SRTPs, but I see BasicPatterns.TraitCall remains unchanged so it's going to be very difficult to support this feature.

I will look at this now.

This is actually also a really motiviatio for getting this issue addressed - it helps allows FCS-based compilers like Fable to be written that are more accurate w.r.t. the intended semantics of F#