`type_check_expr` vs `type_check_expr_in` - unify or not?

[erszcz]

These two seem to be similar, but according to some comments here in issues and in the code they are significantly different.

The source code comments say:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% @doc Infer type of expression
%%
%% Type information should* stem from user type annotation (function specs
%% and type annotated record definitions). If an expression does not have a
%% subexpression that has a type inferred from these sources, its inferred type
%% will be `any()'.
%%
%%   *) When the option 'infer' is true, the types of literals and other
%%      constructs are also propagated.
%%
%% Arguments: An environment for functions, an environment for variables
%% and the expression to type check.
%% Returns the type of the expression, a collection of variables bound in
%% the expression together with their type and constraints.
-spec type_check_expr(env(), expr()) -> {any(), venv(), constraints:constraints()}.
type_check_expr(Env, Expr) ->

and

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Checking the type of an expression
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

type_check_expr_in(Env, ResTy, Expr) ->

As we can see already their names are a bit unfortunate, as _in, at least to me, suggests inference, but it's exactly the other way around. Maybe it's for internal?

@zuiderkwast, I've found this comment - https://github.com/josefs/Gradualizer/discussions/337#discussioncomment-885390 - mentioning that it might be worth merging these functions. In such a case, would we still want the infer option to exist or would inference become the new default with no way to opt out of it?

[zuiderkwast]

Good question. Yeah, they are fundamentally different. They are the two sides of bidirectional typechecking. (I'm not 100% sure about how bidirectional typechecking is usually implemented. Maybe it would be good to look at some introduction or paper about it.)

I think _in means inwards. The type is pushed from the outer expression into the subexpressions. It takes a type but doesn't return a type. This is used when there is a spec, where we have some type to start with.

For type_check_expr, it's inferring (or at least propagating) a type from the inside and and outwards. It returns a type.

Combining them into one would mean a function that it will take one type and push it inwards to subexpressions and propagate/infer another type which returned on the way out of the syntax tree.

The infer option is unrelated AFAICT. Originally @josefs only wanted to use -spec and -type as the source of type information, but with infer we also use literals, list and map constructs, etc. to draw conclusions about types. (I think infer should be on by default but there was no consensus at the time so it ended up being an option.)

[erszcz]

Thanks @zuiderkwast, that's really helpful!

For the record, there was a bidirectional typing talk at this year's SIGPLAN Erlang Workshop - https://www.youtube.com/watch?v=MAerjPQUKQQ - but I cannot find the implementation, it might not be open-source and the article itself is behind the ACM paywall. Outside the Erlang world, there's https://dl.acm.org/doi/10.1145/3450952 - but I yet have to get to it.

[josefs]

The big difference between these two functions is if you know the type that you want an expression to have, or if you're trying to synthesize the type. Even if you write type specs everywhere, there are places where you still need to synthesize the type because you don't really know what it has to be, e.g. in case expression. What type should we give e when typechecking case e of .... end? I hope that clear things up. It would be great if it was possible to merge the two functions in a way that also made the code simpler. But I don't know how to do that.

[michallepicki]

@erszcz

For the record, there was a bidirectional typing talk at this year's SIGPLAN Erlang Workshop - https://www.youtube.com/watch?v=MAerjPQUKQQ - but I cannot find the implementation, it might not be open-source

The impl is at https://github.com/vrnithinkumar/ETC but I found it a bit hard to understand with non descriptive names and quite a lot of modules that take different approach, probably for benchmarks and other comparisons, and I couldn't get the tests to pass

[erszcz]

I finally started reading Bidirectional Typing by Jana Dunfield and Neel Krishnaswami and here's how the paper introduces the problem:

When we implement a typing judgment, say Γ ⊢ 𝑒 : 𝐴, is each of the meta-variables (Γ, 𝑒, 𝐴) an input, or an output? If the typing context Γ, the term 𝑒 and the type 𝐴 are inputs, we are implementing type checking. If the type 𝐴 is an output, we are implementing type inference. (If only 𝑒 is input, we are implementing typing inference [Jim 1995; Wells 2002]; if 𝑒 is output, we are implementing program synthesis.)

Reading the above paragraph was a small enlightenment - "so that's what the Gradualizer naming issue was about" 🤩 Another bit from the paper says:

1. Γ ⊢ 𝑒 : 𝐴 - Under context Γ, expression 𝑒 has type 𝐴
2. Γ ⊢ 𝑒 ⇐ 𝐴 - Under Γ, expression 𝑒 checks against type 𝐴
3. Γ ⊢ 𝑒 ⇒ 𝐴 - Under Γ, expression 𝑒 synthesizes type 𝐴

However, looking at the function signatures and impls:

-spec type_check_expr(env(), expr()) -> {any(), venv(), constraints:constraints()}.
type_check_expr(Env, Expr) ->
    Res = {Ty, _VarBinds, _Cs} = do_type_check_expr(Env, Expr),
    ?verbose(Env, "~sPropagated type of ~ts :: ~ts~n",
             [gradualizer_fmt:format_location(Expr, brief), erl_prettypr:format(Expr), typelib:pp_type(Ty)]),
    Res.

...

type_check_expr_in(Env, ResTy, Expr) ->
    ?verbose(Env, "~sChecking that ~ts :: ~ts~n",
            [gradualizer_fmt:format_location(Expr, brief), erl_prettypr:format(Expr), typelib:pp_type(ResTy)]),
    NormResTy = normalize(ResTy, Env),
    ?throw_orig_type(do_type_check_expr_in(Env, NormResTy, Expr),
                     ResTy, NormResTy).

do_type_check_expr_in(Env, {type, _, any, []}, Expr) ->
    {_Ty, VB, Cs} = type_check_expr(Env, Expr),
    {VB, Cs};
...

we see that:

type_check_expr(Env, Expr) -> {Ty, _VarBinds, _Cs}
type_check_expr_in(Env, ResTy, Expr) -> {VB, Cs}

so according to:

• rule 3 above type_check_expr(Env, Expr) synthesizes (aka infers) type Ty
• rule 2 above type_check_expr_in(Env, ResTy, Expr) checks Expr against ResTy

All in all, the suffix _in seems a bit confusing, seems it might suggest inference (aka synthesising), which is not the case. However, @zuiderkwast's idea about inwards makes sense.

[xxdavid]

Excuse my incomprehension but I've been thinking about this multiple times and still don't quite get what are (in our case) the reasons/benefits for having a separate function for type inference/synthesis and for type checking.

I've tried substituting type_check_expr_in with this trivial implementation.

type_check_expr_in(Env, ResTy, Expr) ->
    NormResTy = normalize(ResTy, Env),
    {InferredTy, NewEnv, Css1} = type_check_expr(Env, Expr),
    case subtype(InferredTy, NormResTy, NewEnv) of
        {true, Css2} ->
            Css = constraints:combine(Css1, Css2),
            {NewEnv, Css};
        false ->
            throw(type_error(Expr, ResTy, InferredTy))
    end.

If I run tests with this implementation, only 64 of all the 717 tests fail. If I also enable the infer option by default (as type of literals is checked by type_check_expr_in even when infer is off), we get to only 39 failing tests. Many of the tests fail because of exhaustiveness checking (which is not performed by type_check_expr), some because the support for relational/arithmetical operations is not as good in type_check_expr as in type_check_expr_in.

But I don't see any fundamental reason why type_check_expr couldn't be improved to deal with such cases as well. I see there may be some performance benefit of doing type checking when we know the assumed type beforehand (instead of inferring the type and checking it with the assumed type). But still, type inference for Erlang code doesn't seem harder (in the computability sense) then type checking to me, provided we have type specs for all top-level functions (and assume (any(), …) -> any() type when we don't). i get it is harder when when you have higher rank types and things like that, but we don't have such things in Erlang.

---

After thinking about it more (and reading part of the Local Type Inference paper), I came up with an example where type checking makes a difference. It is related to anonymous functions (that don't have a spec) for which we run type checking (e.g. when passing them as an argument or returning as a result). The example is really silly but here it is:

-spec fivePlusSomething(fun((integer()) -> integer())) -> integer().
fivePlusSomething(Adder) -> Adder(5).

-spec six() -> integer().
six() -> fivePlusSomething(fun(X) -> X + 1 end).

-spec bad() -> integer().
bad() -> fivePlusSomething(fun(X) -> binary_to_integer(X) end).

When inferring (using the implementation above) the type of fun(X) -> binary_to_integer(X) end, the type of X is inferred as any() (which is reasonable). When type checking, X gets the type integer(), and thus can detect the type error.

But better support for type checking lambdas doesn't still seem quite worth the cost of maintaining two similar similar functions (to me). Are there other use cases where type checking makes a difference? Or do we have it because of performance reasons?

[erszcz]

My thinking, backed by https://www.pls-lab.org/en/Higher-rank_polymorphism, in response to:

I get it is harder when when you have higher rank types and things like that, but we don't have such things in Erlang.

is that we do have higher ranked types in Erlang. Or rather we don't have static types in vanilla Erlang, whereas the dynamic checking done by the runtime doesn't forbid the translated example from executing:

-spec g(_) -> integer().
g(_) -> 1.

%-spec f(fun((_) -> integer())) -> integer().
f(H) -> H(0) + H("lol").

t() ->
    f(fun g/1).

3> ranks:t().
2

We even have a similar example in our tests - test/should_fail/poly_fail.erl:

-spec poly_2(fun((A) -> A)) -> {integer(), boolean()}.
poly_2(F) -> {F(42), F(false)}.

Our constraint solver currently only supports rank-1 types, i.e. the above code fails typechecking with:

Lower bound 42 of type variable A_typechecker_3742_2686 is not a subtype of false | true

However, I think there might be room for improvement here by instantiating a new type variable instances per each call to F and constraining appropriately.

That being said, I'm not sure if it's worth having separate copies of type_check_expr and type_check_expr_in. Maybe we just have to try making all the tests pass with just type_check_expr in place? If nothing else, it might at least tell us why the other is necessary. I think it doesn't preclude bidirectional checking - it would just mean the single function that's left would alternate between checking and inference as appropriate for a given (sub)expression.

There's one more reason why I think your, as you call it, "trivial implementation", @xxdavid, is compelling. I was playing with the idea of this disjunctive normal form here - https://github.com/erszcz/Gradualizer/tree/use-disjunctive-normal-form. I expanded the test we had to two cases:

-spec tuple_case1() -> {t, a} | {t, b}.
tuple_case1() ->
    R = {t, g()},
    R.

-spec tuple_case2() -> {t, a} | {t, b}.
tuple_case2() ->
    {t, g()}.

With the disjunctive normal form tuple_case1 passes, because it follows the logic of this "trivial implementation", i.e. infers type of R, then checks if R :: {t, a} | {t, b} holds.

tuple_case2, however, doesn't pass, as the traversal tries to follow the structure of the type, therefore it goes depth-first into the union members and fails in both cases, since neither g() :: a nor g() :: b holds. I only made it work thanks to this commit, which basically implements your change, but in a narrower scope.