-
Notifications
You must be signed in to change notification settings - Fork 35
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Handling short-circuit operators #23
Comments
Just a comment on
Perhaps we should decide about which semantics are desirable. |
I also regard them as conditional constructs, as that is how the Erlang language (compiler/VM) handles them. This is also how I implemented checking them in #24, exactly to address the self-gradualizing failure on the line that you highlighted. Nevertheless the problem domain in this ticket is more generic, how to handle that the type set of a variable is possibly reduced within a conditional clause body relative to its global type. |
Type refinement would be a very powerful feature to have. But it's also non-trivial to implement and it's unclear to me how important it is. So I think the right way forward is to first try and get the gradualizer into a state where people can use it. Perhaps a version 1.0. Then we can more easily see what features people need and miss and then start to tackle them in the right order. As for my views on the boolean operators, @zuiderkwast , you are correct. They are boolean operators and both arguments should be boolean. This has to do with the underlying philosophy that I have of the gradualizer and how it's distinct from the dialyzer. The dialyzer tries to only find errors when they are guaranteed to happen. I consider this akin to how you put it @gomoripeti :
With the gradualizer I hope to provide a different experience, a typing discipline, which not only thinks about how the compiler and VM works, but is based more on the programmers intent, much like a traditional type system. One of my main motivations for starting to work on the gradualizer was to provide a typesystem-like experience for Erlang. I've seen many people being disappointed when the dialyzer didn't complain about things that a traditional typesystem would catch. Such as passing something non-boolean to a boolean operator. |
thank you @josefs, enlightening the philosophy and attitude of Gradualizer, it helps me when contributing. But I dont want to derail this discussion with lazy ops. Keeping with real conditional constructs: I'd like to argue that it is important: I actually hit this problem in practice (even with self-checking Gradualizer), let's say its second priority. (After handling all language constructs in the simplest way so that there is no crash any more). The practical problem here is that Gradualizer would emit a false warning (which is fine) but Gradualizer stops at the first warning per function so it might not be able to detect other more important issues. (It must stop of course) This is also an interesting problem, so without aiming to implement something immediately I'd be happy to discuss this non-trivial problem domain (as a naive/newbie typer). Maybe some papers around the topic. (So by the time its time to implement it there would be clear discussion and understanding around it) |
Ok, I certainly don't mind discussing these topics in general. I haven't spent very much time thinking about type refinement but if you want to dig into that subject I think that you should at the very least read Sums of Uncertainty: Refinements Go Gradual, a paper from the POPL conference last year. I haven't yet read the whole paper but I assume we will be able to borrow quite a lot from that paper. |
The general refinement is topic is interesting and I want to look at the paper when I have time. Thanks for the link! For the other topic, the lazy boolean ops, I agree with @gomoripeti that this is an interesting topic (although not first priority) as well and I like @josefs's points about the "programmer's intent" as a philosophy for the type system. In this case though, I suspect that what we can expect about the intent is not that clear. There is a trend in using them with non-booleans. I looked up the Erlang reference manual, where these operators are found not under boolean expressions but just under Short-Circuit Expressions. There is even an example with non-booleans. Quotes:
After reading this, I think that this is a matter of style and it would be controversial to regard it as a type error, even in a spec'ed function. I doubt that we have the power to dictate what is good style. We could start by suggesting changes to the reference manual, or by discussing it in the erlang-questions mailing list. It fits perhaps as a rule for the style checker Elvis. |
Thanks @zuiderkwast for the reference to the reference manual. I read that section very differently from you though. Here's my understanding: they've made the short-circuiting boolean operators tail-recursive in order to make them faster. In order to do that, they eliminated the checking of the type. In the second half of Example 2 they are just showing what is possible now, not what is good style. I'm not sure why you're including Example 1 here as the second argument of |
Oops! I missed the |
I repurposed this ticket to host discussion about handling sort-circuit operators (as topic is focusing on that anyway :) ) |
I now also read the short-circuit chapter and it really seems just an optimisation, and not encouraging the use of any type as second arg. (There is no such example in the doc indeed). However it is documented that the second arg "is no longer required to evaluate to a Boolean value" and there are certainly programs out in the wild that utilise this (I realise I was the one who added such use to gradualizer - it is a natural use for me) so Gradualizer should support such programs in some way. @josefs, you already described what is the way: the programmer should explicitly add type annotation showing such an intent. |
I'm confused by what you write. Non-boolean values as second argument are already allowed as the default behavior in Gradualizer! Just don't write any type specs! We seem to agree that this should be the default behavior. However, if there are type specs and the programmer still wants to use non-boolean values then these values must be returned from a function which has return type Here are three examples which pass the gradualizer, despite using non-boolean values as second argument to
Note that the second argument to |
Thanks for the examples. I was confused by the inferred type of literals, but that is clarified in #26. @zuiderkwast, thanks for starting a little poll on the erlang mailing list :) |
just an interesting note: I sometimes use andalso/orelse in the body of match-specs where conditional expressions are not allowed eg:
this would be equivalent with the below (but that is an illegal match-spec fun)
this is the only (very exotic) scenario I can imagine when the non-boolean return value of andalso is actually used, and not just for the side-effect. And actually this is converted to a match-spec term by a parse-transform without any op or fun objects so in reality this is not real code. |
I find this statement controversial. To me, the static types are the truth even if the types are less permissive than possible. Dynamic code that calls a function with values outside its domain is wrong. It's of course not possible to capture every dynamic pattern in static types but the ambition has to be that idiomatic code should be typeable. Deciding on I think it would be a good idea to go for the simpler alternative if this is not yet a common Erlang pattern and there exists a good alternative, otherwise I would want to follow Flow and TypeScript where |
@Zalastax, I'm sorry but I don't quite understand what you're arguing for. Would you care to elaborate on your position. What behaviour would you like Gradualizer to have in this case? As for myself, I'm starting to come around in the issue. I now have a bit of experience with running Gradualizer on existing code bases. Based on that experience I think the right thing for Gradualizer is to be very lenient and allow for common Erlang idioms. I haven't yet bumped against code which uses non-boolean values as the second argument to andalso, but if there are code bases out there which use this idiom heavily then Gradualizer might report so many errors as to be unusable for them. That would be a real shame. |
@josefs I was not really arguing for any side. Instead I was stating that I don't think we should lean on the fact that it's possible to opt out from type checking when deciding on the semantics. I want to capture idiomatic Erlang code as well but if a pattern is troublesome and not well established I think we should allow ourselves to make a statement. This particular idiom seems fairly harmless and it has a following so I'm leaning towards changing our behaviour but I could go any way. |
(just for the record, sorry I did not add it earlier) @zuiderkwast run the question through the erlang mailing list, which became a quite lengthy discussion (thread starts here: http://erlang.org/pipermail/erlang-questions/2018-July/096024.html) The short outcome was that andalso/orelse should work on bools and it is mostly when prototyping/temporary quick fixing/debug logging when it is used otherwise. Also historically the runtime check if second arg is boolean was only removed for optimisation reasons, and not in order to allow this broader usage. summary from Viktor from the mailing list:
Although I was initially supporting the broader usage I was convinced that by default Gradualizer could check for the stricter variant (and adding an option to switch to relax the spec). |
I am afraid as of master @ d74675a we have a bit inconsistent implementation. While type checking accepts any type as second argument (only needs to be subtype of the result type) Gradualizer/src/typechecker.erl Line 2276 in d74675a
type inference still expects the second argument to be boolean Gradualizer/src/typechecker.erl Lines 1531 to 1532 in d74675a
Moreover I think we can restrict the type from
|
It would be -spec andalso(boolean(), false | T) -> false | T.
-spec orelse(boolean(), true | T) -> true | T. but yes, this is a straightforward change. |
So the return type should be the same as or a subtype to the 2nd operand? Is the point of this that we need to be able to push the return type into the 2nd operand when checking or is it some other theoretical benefit? |
Well if |
We will need subtraction to implement type refinement, don't we? At least a simplified one, the simple case of union of single atoms. |
Sure. The first point still stands though: we shouldn't give a type error on |
I still don't think I understand completely. Isn't it enough to require that the 2nd operand is a subtype of the result? I though |
The second operand is an expression that should be checked against some type, not a type that should be a subtype of some other type. We can check Another way of writing the type -spec andalso(boolean(), false | T) -> false | T. is (in pseudo-erlang) -spec andalso(boolean(), R) -> R when false :: R. |
Don't we get -spec andalso(true, T) -> T;
(false, T) -> false. This spec leaks implementation details but gives the most exact static type possible. |
This is indeed the most precise type, but I don't think we have the ability to check it at the moment. |
Might be so. What about widening then? Don't we get away with |
I am little confused about what we're talking about here to be honest. The way we would actually check
which corresponds to What is the widening alternative? |
After pondering this a bit more I believe that it makes no difference to what programs type check. The only difference is whether we let widening happen to the type of the result or the type of the right argument. My intuition would have it as
or, assuming that all checks are performed with "is compatible" semantics
|
In the first case how would you pick The second case is just wrong. If |
I think there's some theory / smart technique that I don't know about here and it's unfortunate that I'm not able to communicate it better. Thanks for explaining the formalities! As you say, if we're checking against To elaborate on what I actually was going for: it's completely fine that function andalso<T>(A: boolean, B: T): false | T {
if (A) {
return B
} else {
return false
}
}
const X: false = andalso(true, false)
const Y: boolean = X |
The typing rule I suggested delivers this. We would check (since subtype(false, false)
check(true, boolean())
check(false, false) which are all clearly satisfied. The only thing we don't get is |
Good! I'm still confused why the false is needed in the right argument but I trust you. |
You are not confused about the fact that we should allow the right argument to be I guess what's causing the confusion is writing the type as -spec andalso(boolean(), false | T) -> false | T. writing it (as I did above) as -spec andalso(boolean(), R) -> R when false :: R. is closer to what the type checker would actually do, and is maybe less confusing, but equivalent. The key to understanding the former type is to note that the -spec andalso(boolean(), boolean()) -> boolean(). If we take -spec andalso(boolean(), false) -> false. We can also take -spec andalso(boolean(), false | error) -> false | error. In each of these cases it would be wrong to drop |
Does it mean that |
It fails to type check as a number: |
@UlfNorell So if I have -spec get_value() -> number().
get_value() -> 42.
-spec test(boolean()) -> false | number().
test(Pred) -> Pred andalso get_value(). will it also fail? |
No this is accepted. We will check ( subtype(false, false | number())
Pred :: boolean()
get_value() :: false | number() all of which hold. |
Essentially ```erlang -spec andalso(boolean(), false | T) -> false | T. ``` and same but with `true` for `orelse`. cc #23
Essentially ```erlang -spec andalso(boolean(), false | T) -> false | T. ``` and same but with `true` for `orelse`. cc #23
Essentially ```erlang -spec andalso(boolean(), false | T) -> false | T. ``` and same but with `true` for `orelse`. cc josefs#23
let's see the following correct function with spec
AI
inExrp2
must be the subtype ofnumber() :: integer() | float()
as the first argument of+
AI
inExrp2
isatom() | integer()
based on the spec which is not a subtype ofinteger() | float()
How could Gradualizer realise that
Expr2
is only executed when type ofAI
isinteger()
?if NOT is_atom(AI) => typeof(AI) == (atom() | integer()) & (not atom()) == integer()
- however this is not always possibleLet's see a more generic example
In this case what the type checking could do is realise that
body(A)
is only executed in a subset of cases therefor type ofA
inbody(A)
is just a subset or subtype ofinput()
. In caseinput() & required() == none()
(the intersection of the two types is empty) then we can say thatbody(A)
will always fail, but otherwise we cannot know (and have to leave type checking at runtime). This method requires to be able to calculate the intersection of two types.What is the right way to handle these kind of constructs? (
if
,case
,andalso
,orelse
, multiple function clause)The text was updated successfully, but these errors were encountered: