Questions about Gradualizer about gradualizer HOT 11 CLOSED

@josevalim Cool idea! If my_length/1 is inlined, and inlining is done in the AST before type checking, then you would catch the type error for computes_length/1. Perhaps this is not at all how things are done but I thought I can mention it. :-)

I'm not using Elixir myself, but I assume the Elixir world is evolving a bit faster than the Erlang world. It would be pretty cool if gradual typing becomes part of the Elixir compiler or tool chain.

from gradualizer.

I think currently this github thread is enough for general questions, for specific things github issues can be created

from gradualizer.

Regarding partial evaluation, the upcoming ACM SIGPLAN Erlang Workshop has a paper (Typing the Wild in Erlang) which evaluates that idea and contributes some other thoughts a well. Worth a read!

from gradualizer.

Hi @josevalim

Thanks for your interest in the gradualizer!

First question:
As an example, let's consider a function which returns an integer(). We can give it many return types, including term() and any().

-spec int_term() -> term().
int_term() -> 5.

-spec int_any() -> any()
int_any() -> 5.

I guess this is the reason you wonder about the difference between term() and any(). The difference comes in when we want to use the result of these function in another function. Suppose we have a function which takes an integer() as an argument, e.g.:

-spec int_arg(integer()) -> integer()
int_arg(I) -> I + 1.

Here's the difference between term() and any(): the call int_arg(int_any()) is ok because we're passing something untyped to a typed function, whereas the call int_arg(int_term()) is not ok because we're passing a value of a much larger type (term()) to something which only accepts a smaller type (integer()). (We currently seem to have a bug, as the call int_arg(int_term()) is not rejected, but that should be fixed.)

Second question:
If a function is not spec'ed (and it doesn't matter if it's in the same module, or a different one) it is always considered untyped, i.e. all the arguments are of type any() and the result type is any().

I hope these explanations make sense to you.

As for the right forum to ask these kinds of questions; it's fine to ask them here. However, I've been thinking about setting up some kind of mailing list, google group, or something else which would provide a natural place to discuss things about the gradualizer. What do you think about that. @gomoripeti @zuiderkwast @tim2CF , do you think it'd be good to set up some kind of forum for gradualizer?

EDIT:
My explanation about the difference between term() and any() is completely bogus. A better example for showing the difference is these two functions:

-spec any_int(any()) -> any().
any_int(I) ->
    I + 1.

-spec term_int(term()) -> term().
term_int(I) ->
    I + 1.

The first function is ok, while the second function is not. The gradualizer rightly complains about the second function:

The operator '+' on line 17 is given a non-numeric argument of type term()

from gradualizer.

Here's the difference between term() and any(): the call int_arg(int_any()) is ok because we're passing something untyped to a typed function, whereas the call int_arg(int_term()) is not ok because we're passing a value of a much larger type (term()) to something which only accepts a smaller type (integer())

Perfect. Thank you.

If a function is not spec'ed (and it doesn't matter if it's in the same module, or a different one) it is always considered untyped

I have been considering partial evaluation to improve the depth of type checking. But it does come with an increase in CPU and memory.

I will close this since my questions have been answered but feel free to reopen it if you want to keep the discussion going. :)

from gradualizer.

Re forum: I also agree that github issues are ok for now. We can tag them as question and discussion (whereas tagging real "issues" as bug and enhancement)

from gradualizer.

Regarding partial evaluation: Currently, we don't want to do type inference or partial evaluation of unspec'ed functions, because if no types are written, it is considered dynamically type code, which means we don't want compile time type errors for these functions.

Re forum: I also agree that the issue tracker is good for now and that we can use label if there are many issues. We could also use the github wiki for notes/theory/FAQ and things like that.

from gradualizer.

Regarding partial evaluation: Currently, we don't want to do type inference or partial evaluation of unspec'ed functions, because if no types are written, it is considered dynamically type code, which means we don't want compile time type errors for these functions.

Right. Let me expand on my thoughts a little bit. :)

I have implemented a static type inference system for intersection types and unions and very quickly I ran into some of theoretical concerns related to inference of intersection types: namely there is an explosion of clauses to be analyzed. This Elixir code:

def some_fun(a, b, c) do
  a && b || c
end

Had to consider 27 different clauses, since both && and || has clauses for false, nil and then everything else. It also led to very broad union types.

In my mind, type inference is out of the game, unless we want to change the language semantics (which I personally do not). The alternatives to me then became gradual typing or partial evaluation (at least in my limited understanding). Possibly a combination of both, since partial evaluation would allow us to check code that was not explicit typed, which is part of the benefits of inference. Although partial evaluation comes with its own costs and choices, such as local or global evaluation, and the depth. Hence my questions. I should probably have been clearer from the beginning but at the end of the day it is just my curiosity :)

from gradualizer.

@josevalim , thanks for clarifying your thoughts. My goal for the gradualier (at least in the short- to medium term) is to not have any inference. One of the reasons for this is that it makes the gradualizer compatible with all existing Erlang code bases. If there are no specs, then the program will always pass. Starting from zero specs, the programmer can gradually add specs at his or her own leisure and at the places where they are most important. Consequently, gradualizer will only check part of the program. And that's ok!
If we were to introduce inference, then the type checker would start barking even at un-spec'ed programs. If you already have a large code base then you might be overwhelmed by the amount of barking and decide to stop using the tool.
In the longer term it might make sense to do inference in one form or another, but I don't plan to spend any cycles thinking about it any time soon.

I see now why you were talking about partial evaluation. I didn't understand how it related to your question before, so thanks for the clarification. Partial evaluation would indeed be a lot of work to implement, but that is not my biggest concern. I would be more worried about how the programmer could understand the types that the typechecker would infer. If the inferred type depends on how much partial evaluation is performed, it would be nearly impossible for the programmer to figure out what types would be inferred. Hence it would be maddeningly difficult to understand the type errors, or even why a type error doesn't happen. I would strongly advice from taking this route.

The advantage of the choices we've made in the gradualizer is that it's super simple to understand the types involved and why a type error happens. Just doing type checking and not type inference it admittedly boring and unsexy, but it helps to keep everything simple.

from gradualizer.

Thanks @josefs!

I was not thinking about partial evaluation to do inference per se, only to add depth to the type checking. Imagine this code:

-module(example).
-compile(export_all).
-spec computes_length(list()) -> float().
computes_length(List) -> my_length(List).

my_length(List) -> length(List).

Let's assume that you know the type of erlang:length/1 since it is a built-in.

The code above will typecheck because it calls my_length/1, which was not typed, and therefore has type (any() -> any()).

However, since you know the argument given to my_length/1 is of type list(), you can perform the partial evaluation of my_length(list()) and conclude that the return type is actually integer(). AFAIK, there is no extra complexity in this, because the process of evaluating my_length(list()) is exactly the same as checking any other typed function.

If my_length/1 is called N times with different types as inputs, you would partially evaluate it N times with those different inputs. This increases type checking time. You could cache those evaluations at the cost of memory, but the only purpose of a cache would be to speed up type checking and not to infer a type.

In this approach you still have control over when things are type checked. After all, my_length/1 is evaluated with the caller's types and ONLY IF the caller has been typed. Error reporting can be quite good to. I can see this being useful at least for local functions, as it would effectively require us to only type public functions, giving us more freedom on how our private functions are structured (also helpful when refactoring).

There are different ways you could control the evaluation. It can be only local or remote too. You can also limit the depth. Anyway, I am not proposing this feature in Gradualizer itself. Just curious. :)

Thanks for your time! 👍

from gradualizer.

@zuiderkwast For now Elixir simply relies on the typespec notation from Erlang, so everything that works for Erlang should just work for Elixir, including Gradualizer. This means in this particular area we are moving as fast or as slow as Erlang, which can be good news or bad news depending on who you ask. 😄

from gradualizer.