Discussion on: Function Intersection Types Considered Surprising

[Max Heiber]

Update 1:

Stavros Aronis kindly shared a link to their experimental work on better intersection types for Dialyzer. This version of Dialyzer caught 22 discrepancies in OTP, and got better behavior for behaviors overall.

After the front matter, the paper is in English

Update 2: My description of what Dialyzer does left out a lot. Here's a fuller picture of how Dialyzer currently handles functions with specs that contain intersections:

-spec baz(integer()) -> boolean(); (float()) -> float().
baz(1) -> true;
baz(1.0) -> 1.0.

1. Find the success typing. In this case it is number() -> 'true' | float(). Dialyzer doesn't currently infer intersection types for functions, as far as I can tell.
2. Collapse the intersections in the spec by taking the union of the domains and union of the ranges. Then we get number() -> (boolean() | float()). Dialyzer seems to always immediately collapse intersections in specs, so the only motivation for writing specs with intersections (for now) is for better documentation for humans.
3. The final type is the intersection of the specced type and the success typing. Which is done by intersecting the domains and ranges, respectively. So we end up with number() -> 'true' | float().

Update 3

Update 2 was wrong.

Dialyzer does remember and use the mapping of arg types to return types for function specs with intersections. The action happens in dialyzer_contracts:get_contract_return(C :: contract, ArgTypes). The collapsing into union types I described in the previous update also happens, as does the pairwise intersectioning of domain and and range I wrote about in the post. So there isn't one answer to "how does Dialyzer handle function intersections?"

running typer on a sample.erl with these contents:

-module(sample).
-export([main/1]).

main(_Args) ->
    bar(10) + bar(20).

-spec bar(10) -> 10; (20) -> 20.
bar(X) -> unknown_module:f().

generates:

-spec main(_) -> 30.
-spec bar(10) -> 10
    ; (20) -> 20.