Role of `type_check_expr` about gradualizer HOT 12 OPEN

Just a note, without expecting any answer

As a "real user" :) (running Gradualizer on a smaller open-source and big proprietary project) I can say that not only Erlang/OTP is (almost) fully type-spec'ed but any decent project is expected to have type-specs, at least the API/exported functions (if for nothing else than documentation for humans).

So it is not a real-world assumption that people will start using Gradualizer on a fully non-spec'ed code-base and have no warnings in the beginning. Because of this a switch to ignore specs from the standard lib has less impact. But it is true that even a bit less types mean bit less errors a user will start with, and the goal is to ease start using the tool.

from gradualizer.

Where did I write anything along the lines of "type_check_expr should not return type in any case"? If I did then I was clearly delusional.
The function type_check_expr has a very specific role. It tries its best to propagate the return type of functions which are called within an expression. Sometime type_check_expr does return a type which is different from any() and in those cases the type can always be traced back to a call to a type spec'ed function.

In general, the split between the functions type_check_expr and type_check_expr_in follows the principle of bidirectional typing, which, among other things, maximizes the propagation of type information. There are plenty of papers on this subject if you're interested.
That being said, the names of the functions are pretty bad. type_check_expr really should be called something akin to infer_expr and type_check_expr_in should be something like type_check_expr.

from gradualizer.

(it was actually Victor who mentioned return-no-type)

I see, so type information must always stem from specs (of functions and also records, if I see correctly) and type should be inferred from no other untyped construct.
(This is a little heureca moment for me and explains a few places in the code I didn't understand -why we fall back to any() so eagerly. I had the assumption that we should use the most type info we can sqeeze from an expression, eg from literals - but this is not the case.)

Is the reason for this (not to infer type from other constructs) is to maximize the power/effect of user intent?

(example: type_check_expr( {1.5, 2.5} ) should not infer {any(), any()} (or {float(), float()}) but any() because no specs are involved.)

from gradualizer.

there is an interesting consequence of the above (I dont know if we can call this inconsistency or just surprising for some)

This snippet fails type checking as a list is passed to g/1 which is a function with spec and expects integer() (done by type checking in type_check_expr_in)

f() ->
  g([1, 2]).

-spec g(integer()) -> any().
g(Int) -> Int + 1.

However this second snippet passes type checking because V has the inferred type of expression [1, 2] which is any(), and then any() is checked against integer() in type_check_expr_in

f() ->
  V = [1, 2],
  g(V).

-spec g(integer()) -> any().
g(Int) -> Int + 1.

from gradualizer.

Wow! Good finding Peter! Now I get a feeling of eureka too. It doesn't seem right that g([1, 2]) and V = [1, 2], g(V) are not equivalent. My intuition tells me that we should infer as much information as possible and let the principle "no errors for untyped programs" step aside a little, in favor of finding more errors. Type errors are just warnings anyway as this is not part of the compiler. Or we can type check only functions with a spec?

from gradualizer.

I'm glad to hear you're experiencing eureka moments.

Is the reason for this (not to infer type from other constructs) is to maximize the power/effect of user intent?

(example: type_check_expr( {1.5, 2.5} ) should not infer {any(), any()} (or {float(), float()}) but any() because no specs are involved.)

That's exactly right!

As for the example with the variable, I'm aware of it, and it bugs me too. But I don't know how to formulate type rules which would report an error for the second program.

let the principle "no errors for untyped programs" step aside a little, in favor of finding more errors

I disagree, because it would ruin the consistency of the overall design. The type system that I've currently designed is careful in maintaining a set of principles ("no errors for untyped programs" being one of them) which makes it easy to understand and explain when a type error will occur. Furthermore, in the long run I'm looking to formalize this type system and create a cast calculus which could form the basis for a much more efficient implementation of Erlang which takes static types into account when compiling. In order for that implementation to be sound it is important to maintain the graduality property. Now, admittedly, I haven't proven graduality of the current type system, but I'm been careful in staying as close as possible to the current state of the art so that I wouldn't mess it up too much. If we were to invent our own type rules just because we're a little concerned about information loss, we risk throwing away a lot of the future benefits of this type system. @zuiderkwast , can you point me to a gradual type system which incorporates the kind of type information that you would like, and which has the graduality property? If you can, I'd be prepared to change my mind.

On a more general note, I'm a little concerned with how I spend the little time I have on the gradualizer. While I do enjoy the discussions we have here on the bug tracker I currently don't do any hacking at all, and that concerns me. Indeed, I think some of the discussions we have here would be much better informed if we had actual users. So I'm eager to get gradualizer to the point where other people can use it in their projects in a meaningful way. I don't want to discourage discussion, but at the same time, I feel that I should probably do less of it, in favor of more hacking.

from gradualizer.

@josefs wrote

@zuiderkwast , can you point me to a gradual type system which incorporates the kind of type information that you would like, and which has the graduality property? If you can, I'd be prepared to change my mind.

Yes, the gradually typed lambda calculus in Siek 2006 "Gradual Typing for Functional Languages". Here is a quote:

Relation to the untyped λ-calculus We would like our gradual
type system to accept all terms of the untyped λ-calculus (all unan-
notated terms), but it is not possible to simultaneously achieve this
and provide type safety for fully-annotated terms. For example,
suppose there is a constant succ with type number → number. The
term (succ ”hi”) has no type annotations but it is also fully anno-
tated because there are no function parameters to annotate. The type
system must either accept or reject this program. We choose to re-
ject. Of course, if succ were given the type ? → ? then (succ ”hi”)
would be accepted. In any event, our gradual type system provides
the same expressiveness as the untyped λ-calculus. The following
translation converts any λ-term into an observationally equivalent
well-typed term of λ^?_→.

Notice that the succ function is described as a constant. Just as we can choose to use or to ignore the specs in the standard library, we can choose to use or to ignore the types of constants such as literals. Here, Siek choose to use this information in both cases. That's how I read it anyway.

from gradualizer.

@zuiderkwast, you should be a little careful to use the original gradual typing paper as a reference. The paper "Refined Criteria for Gradual Typing" describes the original paper as providing "an
incomplete formal characterization of what it means to be gradually typed." Indeed, graduality doesn't hold for the formalization in the original paper (although "Refined Criteria for Gradual Typing" fixes that problem.) Also, just to be clear, when I use the term "graduality" I'm referring to how they use it in the paper "Graduality from Embedding-Projection Pairs."

Before I respond in detail to your comment, I'd like to explain why I have the "no errors for untyped programs" rule. I feel like perhaps I haven't explained well enough why I designed the type system with this rule as an overarching principle.

Suppose you're working on a large Erlang project (like the SGSN-MME) and you want to try out the gradualizer. It is very important that you do not get too many type errors reported initially, in particular in the unannotated parts of the program, because then you're just going to give up. It's going to be overwhelming and simply not cost effective to fix all those errors. I've seen this happen to other, excellent tools, which reported genuine bugs. But they reported too many bugs and therefore was rejected. I'm not at liberty to provide more details in this public forum, but it's very important to me that the gradualizer doesn't suffer the same fate.

Another argument in favor on not giving any errors for untyped programs is that if the gradualizer becomes popular enough, it might even be integrated into the Erlang compiler by default. This would be a huge boost for the Erlang language! But if that is going to happen, it is absolutely essential that we don't report any type errors for unannotated programs, because we don't want people's Erlang programs to all of a sudden be rejected by the compiler.

Ok, let's get back to the original gradual typing paper. I'm surprised that you use that as an argument in favor of your position, since they don't provide any argument as to why they make the choice they make. It's an arbitrary choice to them. But for us it's not an arbitrary choice, for the reasons that I've stated above. For us, the right choice is to let constants be dynamically typed. Furthermore, as they explain in the last sentence you quoted, in order to silence the errors, the programmer must perform the translation of the program that they outline, which is a real problem if you want to try out the gradualizer on an existing project. The reason that they have to make this arbitrary choice is that their language lacks type annotations on expressions (i.e. "e :: t"). If they had these kinds of annotations then the choice they make is actually the wrong one. With this type of annotation it is possible to encode both STLC and DTLC only if you choose not to give constants a static type. Now, Erlang doesn't have type annotations on arbitrary expression, but in the long run that is something that we should absolutely extend the language with, as it is very useful and natural in certain situations.

I feel that this question is a big distraction and time-sink for me. @zuiderkwast, we've debated this both here and irl, and so far you haven't said anything to convince me of your position. And I don't seem to be able to convince you of mine. I'm going to let this discussion rest until we have publicly announced gradulizer 1.0.

from gradualizer.

It would still be nice to have a switch to report typing failures in untyped sections so as to know what is missed.

from gradualizer.

Thanks Josef for the thorough answer and the references to the other papers! I'm sorry that you feel that this discussion is a distraction. I think it is valuable and I hope others too find this interesting. Perhaps this material can serve as some inspiration for a manual in the future.

It's true that it's an arbitrary choice in the first paper, but at least it seemed to be a possible choice. I only wrote it because you asked me for an example. I never claimed that I have a good understanding of the theory.

I thought that it seems odd to use the return types of typed standard library functions while not using types of literals as both can be regarded as constants. Also, Peter's example with the variable V was bugging me.

from gradualizer.

@zuiderkwast, sorry for my unnecessarily abrasive last post. I've been rather frustrated that I don't have much time to work on the gradualizer right now, but it's unfair to take it out on you. I apologize for my harshness.

All in all, it's a good thing that you got me to spell out my rationale behind some of my decisions. Indeed, as you suggest, it'd be good to include such reasoning in a manual.

I thought that it seems odd to use the return types of typed standard library functions while not using types of literals as both can be regarded as constants.

Hmmm. I haven't thought about it in this way before. But as we discussed previously, it'd be good to be able to turn off types from the standard library.

Also, Peter's example with the variable V was bugging me.

Indeed, it's bugging me as well. What I would like to be able to do, is let type information "flow backwards" from the usage of the variable to its binding site. But standard type systems typically don't let you do that. However, some form of constraint based formulation of the type system might be able to achieve this. It would be a major undertaking though, I don't know of anyone who's ever tried to do a constraint based gradual type system.
If someone has a bright idea here, I'm all ears.

@OvermindDL1, yes, long term I think it might be an option to consider.

from gradualizer.

Thanks for the feedback Péter. I'd love to hear more about your experience running Gradualizer on various projects. Do you have any success stories to share? Any bugs found?

As for point about the amount of specs in a code-base, your point is well made.

from gradualizer.