Intersection types in the type language

[josefs]

Intersection types in the type language

[zuiderkwast]

Yeah! So, what's the way forward?

Ideally, we convince the OTP team to include the intersection type in the official type language. My colleage Karol says that he has reported this years back but it has not been prioritized.

Until then, we can add it in our type, which we could export in the main interface module, i.e. gradualizer:type(). Then we just need to implement pretty-printing for it as a special case and handle it in the typechecker. I don't see that we need to do anything else. Do you?

Then, how should it be represented?

I suggest {type, erl_anno:anno(), intersection, [type()]}.

For the syntax (pretty-printing, documentation, etc.), I suggest the semicolon T1 ; T2. Can it only be used for fun types or do we for example ever need to intersect with any()? If it's only for fun types, I think the first of these syntaxes would be nice; otherwise the second:

-type t() :: fun((boolean()) -> its_a_bool;
                 (integer()) -> its_an_int).
-type t() :: fun((boolean()) -> its_a_bool);
             fun((integer()) -> its_an_int).

If we want to allow T1 ; T2 for any types, is there any risk of syntax ambiguity when mixing specs with intersection types?

-spec foo(boolean() | atom()) -> fun((boolean() -> its_a_bool) ;
                                 fun((atom()) -> its_an_atom) ;
         (integer()) -> its_an_int.

[gomoripeti]

I think intersection with any() could be temporary solution for handling conditional expressions before refinement types are fully implemented.

for exampe

  case get_int() of
     PosInt when PosInt > 0 -> handle_pos_int(PosInt);
    _ -> ...
  end.
-spec get_int() -> integer().
-spec handle_pos_int(pos_integer()) -> any().

We could infer the type of PosInt to be integer() ; any() (ie. some subset of integer())

(I think that intersection is most useful during internal type checking and apart from funs we don't necessarily have to allow it for arbitrary types as user definitions (ie no need to include in OTP). However pretty-printing intersection of any two types can be useful if Gradualizer type calculation arrives to such a type)

[gomoripeti]

I don't have broad knowledge of history and syntax in other languages.

Could you explain me why ; is a good fit for intersection or why it is used in specs already? To me ; feels like OR, while intersection feels like AND (aka ,).

(I understand that in specs ; is used, maybe there it also stems from a kind of OR notion, as in "function arg can be integer() OR atom()" rather than "function must handle integer() AND atom() arg")

If it is the opposite in some sense of union it could be &. (that could avoid bit of ambiguity too)

Another question: would it be allowed in fun types for the domains to not be disjoint? (eg. fun( (2) -> atom(); (integer()) -> list() ))