This is the part where I seize the opportunity to bash strict type systems for low-level (or even intermediate) languages, and preach the virtues of proof-based correctness. ;)
On Sat, Dec 27, 2014 at 12:56 PM, Jonathan S. Shapiro <[email protected]> wrote: > I'm beginning to understand why F# is not seeing wildly enthusiastic uptake. > :-) The generalization mechanism is just plain broken where you would really > like it to work, which makes it challenging to see the potential. As far as > I can tell, the problem is a CLR limitation. > > If I fire up fsharpi (the interactive environment) and type: > > > type Complex = > { Re: double > Im: double } > static member ( + ) ( left: Complex, right: Complex) = > { Re = left.Re + right.Re; Im = left.Im + right.Im };; > > > let first = { Re = 1.0; Im = 7.0; };; > let second = { Re = 2.0; Im = -10.5; };; > > > first + second;; > val it : Complex = { Re = 3.0; Im = -3.5; } > > let sum x y = x + y;; > val sum : x:int -> y:int ->int > > let csum (x : Complex) y = x + y;; > > val csum : x:Complex -> y:Complex -> Complex > > > Note that the (+) operator is not parametric. Which is pretty sad, because > when you start playing with genericity to wrap your head around it, the very > first thing you play with is extensions to arithmetic. Don Syme (the F# guy) > is a really smart guy, and it turns out he's the guy who came up with the > generics mechanism for CLR, so he surely knows this, so what's going on? > > F# has a constraint system of sorts, and one of the constraints is a static > member constraint. So why not take the position (which CLR already does, > sort of) that "int" is actually a value type that provides a static > implementation of + (actually several). > > Well actually, that's exactly what it says on page 42 of the standard. The > F# library defines the + operator with the following signature: > > val inline (+) : ^a -> ^b -> ^c > when (^a or ^b) : (static member (+) : ^a * ^b -> ^c) > > So now if I try: > > let inline sum x y = x + y;; > > > sure enough it generalizes. And yup. Right there on page 42 it says: "Use of > overloaded operators do not result in generalized code unless definitions > are marked as inline." > > Actually, that statement strikes me as incomplete. What actually seems true > here is that the library definition of (+) is using "statically resolved > type variables". Which is to say: type variables that must resolve at static > compile time. That, in turn, appears to be driven by the (well hidden) > requirement that an F# member constraint cannot be applied to a conventional > type parameter. As it turns out, this is a CLR limitation. CLR doesn't have > member constraints on generic types, so there's no way to carry this > constraint down to the level of CIL. > > So why is the requirement that we inline the function? Actually, I think > that's a mistake, though I could be wrong. > > The requirement from the CLR perspective is that we be able to statically > identify the types so as to enforce the member constraint. We already know > that much from the presence of statically resolved type variables. The > "inline" keyword doesn't tell us anything new here. It seems to me that we > could arrive at a satisfactory alternative using compile-time > polyinstantiation. We can't export the function beyond the unit of > compilation, but strictly speaking we don't need to inline it. > > The underlying problem is that CLR expands generics at run time, and > therefore needs a way to check at static compile time that the expansion > will succeed. That's where the missing member constraint comes in. CLR just > can't express the requirement. > > The end result is that F# is obliged to put a monomorphism constraint on > such procedures in order to remain within the expressiveness limits of CLR. > I'm guessing, but I suspect Don was faced with two bad options: (1) impose > the monomorphism rule, or (2) provide some mechanism to emit a bunch of > selected overloads and say which ones are callable. > > My impression is that this would impact BitC on CLR as well. Anybody see a > reason to believe otherwise? > > > shap _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
