f1 : (formatter -> 'a -> unit) -> formatter -> (('a * int list) * 'a clause) list -> unit
and
f2 : 'a -> 'b -> unit.
f1 is a pretty printer that admits a second function to do some additional printing. In this case f2 is really a null function (let f2 _ _ = ()). But partial application f1 f2 produces weak types. Even if I manually annotate the result, the type inferencer insists that the composed type is:
formatter -> (('_a * int list) * '_a clause) list -> unit
What may be the likely cause of this? I am on OCaml 4.10.2.
Not pretending I know why this happens (been too long since I studied ML type inference with :=) but I think it has to do with the fact that the result of computingf1 f2 is something that exposes a polymorphic value. So it needs to either not compute, or be fully-applied with arguments of non-polymorphic type. Something like that.
And you added the “l” arguments, yes? Yeah, this is a classic example of where you have to add the abstraction. B/c otherwise, the value is polymorphic and toplevel, and that’s … not allowed. It seems silly, but IIRC there was an involved proof and set of counterexamples for other methods of type-checking, back in … 1994-ish. Maybe a little before.
It’s actually not silly, once you know the details. Luckily, we almost never need to know the details, and can get on with other stuff, while the OCaml designers and implementors deal with it.
In Caml (and other ML-like languages) polymorphism is only introduced via let, and not in particular as a result of function application (such as f1 f2). See FAQ - Core language
Any idea why I don’t see that message about partial application referenced in the FAQ? I only get a warning that the module signature contains weak type.
Sorry, which error message? I don’t think you would see an error message but instead the result term will be assigned a different type (weak type variables vs polymorphic type scheme).
it would be, uh, an unending task, to document all the ways in which you can write ML programs that fail to typecheck, yes? For those us,who wish to really become experts in the type system, there are papers and parts of the manual (I forget where exactly, but last time I asked, someone pointed them out to me); for the rest of us, it suffices to just have a few rules of thumb to get out of jams.
In the case of partial application the weak type designation can be too conservative. It is easy for the compiler to do what the programmer does by hand: instantiate putative polymorphic types and check to make sure they are not weak. There may be performance reasons to not do so in the past but it is doubtful such reasoning holds nowadays. I believe it is better to not leave a “gotcha” here in order to save some cpu cycles.
The restriction has nothing to do with performance but rather with soundness of the type system. To see this, consider the following function make_fake_id : unit -> 'a -> 'a defined by
let make_fake_id =
let last = ref None in
fun x ->
match !last with
| None -> last := Some x; x
| Some y -> y
Then the application make_fake_id () must (and is) be given a type involving weak type variables _weak1 -> _weak1, as it would not be sound for the result of make_fake_id () to be applied to arguments of different types.
Since it is not possible to tell whether a function depends or not on mutable state in general, the type system overapproximates and treats the result of any function application as potentially depending on mutable state, and gives it a “weak” type.
If you want to know more about this, you can look up “value restriction”, or read the part of the manual where it is explained OCaml - Polymorphism and its limitations
You are right but that is not what I was suggesting. I was pointing out that in my case the compiler could have treated the declaration:
let f = f1 f2
as if I had:
let f x y = f1 f2 x y
instead, and check to see if there is any weak type variable leaking out. In my case it didn’t try until it is explicitly forced to. I am not suggesting that weak type variables should leak or that it should not err on the conservative side if it has trouble figuring out. But in the cases that can be easily solved I think the compiler could do a little more to be more precise.
Ah, but that would change the semantics of your code. Remember that thea key idea in ML is that you can take an untyped version of your program, run it, and get the same result (modulo erasing types) as taking the typed version of your program and running that.
Your suggested code change will break that property. And it’s a really, really, really important property (to us systems jocks, at least).
ETA: for example, if f1 f2 raised an exception, or had some other side-effect.
ETA2: this is what I meant when I wrote "computingf1 f2"
I am not suggesting actually changing the code. I am suggesting type checking it with the putative change in addition to type checking it as is so as to be more precise. Right now I actually have to change the code in order to appease the type checker.
I wonder if anybody’s done any thesis work on this problem: keep in mind that a naive way of doing this would introduce nondeterminism (aka backtracking) and hence might blow up the time complexity of type-checking.
Not really, as stated previously, the semantics of
let f = f1 f2
and
let f x y = f1 f2 x y
are completely different. Thus, it does not make much sense to typecheck let f = f1 f2 as if it was let f x y = f1 f2 x y. The root issue is more than the type system is not precise enough to know if f1 f2 is effect-free (and thus can be generalized) or not (and thus should not be generalized).
Thanks!