Drop the --infer flag #573
Conversation
There was a problem hiding this comment.
To be honest, I never fully understood why infer wasn't the default (and only) mode. If I recall the discussions correctly, it was added by @zuiderkwast but never fully supported by @josefs, as @josefs wanted to rely solely on typespecs as part of the gradual typing paradigm ("without typespecs, no checking happens, it is up to the programmer to enable checking by adding typespecs, the programmer is in control of what is checked and what is not"). I don't really share this perspective on gradual typing (but I do respect it!) and I agree with you that literals are a trustworthy source of type information.
The pull request itself seems legit to me and I personally approve it, but that's only my take on it.
test/typechecker_tests.erl
Outdated
| %% Although there is no spec for f/1 - inferred arity does not match | ||
| ?_assertNot(type_check_forms(["-spec g() -> fun(() -> integer()).", | ||
| "g() -> fun f/1.", | ||
| "f(_) -> ok."], | ||
| [infer])) | ||
| "f(_) -> ok."])) | ||
| ]. | ||
|
|
||
| infer_types_test_() -> | ||
| %% Checking type_check_expr with inference enabled |
There was a problem hiding this comment.
I think comment can be now reworded.
| %% infer exact type of record index | ||
| ?_assertMatch("2", | ||
| type_check_expr(_Env = "-record(r, {f}).", | ||
| _Expr = "#r.f", | ||
| [infer])) | ||
| _Expr = "#r.f")) | ||
| ]. |
There was a problem hiding this comment.
This is now checked in the propagate_types_test_ as well.
This removes the --infer CLI and #env{} option.
The Erlang VM does dynamic type checking based on type tags embedded in values.
This means that it's safe to infer type information from literals and operators
according to the same rules that the VM enforces at runtime.
Actually, these are one of the few completely credible sources of information,
unlike type specs, in which there's room for human error.
Removing the option along with the branching in the typechecker should somewhat
minimise the amount of code to maintain.
erszcz
force-pushed
the
drop-infer-flag
branch
from
a394b13 to
d3968cf
Compare
|
Since I'm no longer active in this project, I don't have an opinion on this PR. But since I was pinged, I thought I'd like to clarify my position here. When I set out build gradualizer, an important goal for me was to be able to start with an existing Erlang code base and run gradualizer without any errors (or perhaps, if there was already some erroneous type specs, they would be highlighted, but nothing more). Being able to apply gradualizer with minimal cost to an existing code base without being overwhelmed with type errors immediately would lower the threshold to adoption. Then, one could progressively add more and more type specs and get gradually more benefit from gradualizer. The goal was to provide a pay-as-you-go experience. Enabling inference could be added later, as it could potentially generate a lot of type errors up front. It certainly would have for the code base I used to work on. I had planned, but never implemented, a strict mode which would require type specs everywhere in a file, no |
|
Hey Josef! I'm not that active either anymore. Eqwalizer has a strict and a non-strict mode, I believe. They seem to provide some real guarantees by not supporting the detailed type hierarchy (no subtyping?), but it may be a more useful tool in practice? (I don't know.) David, thanks for reminding me of the discussions around this. I recall that Josef's idea initially was to rely on typespecs only and nothing else, and I supported that. The more we implemented and tested it, though, the more it became apparent that this approach had some problems, like all the OTP library functions having type specs, while arithmetic operators and literals not having any, was a bit problematic. I argued that we should consider other sources of type information too. (What should be used as type information and why?) The graduality guarantee ("gradual soundness") vs eliminating false positives was another balance between theoretical correctness and practical usefulness, and I believe still is. I found it hard to accept that we can't fully achieve both. (I still haven't accepted it. 😁) |
… return type Even when a function does not have a spec, we still know that it is a function and that is of certain arity. This is probably related to making the infer flag default in josefs#573, as without infer, we always assumed any() when there wasn't a spec for something.
This removes the
--inferCLI and#env{}option. The Erlang VM does dynamic type checking based on type tags embedded in values. This means that it's safe to infer type information from literals and operators according to the same rules that the VM enforces at runtime. Actually, these are one of the few completely credible sources of information, unlike type specs, in which there's room for human error. Removing the option along with the branching in the typechecker should somewhat minimise the amount of code to maintain. Moreover, requiring users to know the available options might lead to a worse impression of what the typechecker is capable of, since if they're not used, the tool is not showing it's full potential.