Subtyping rules for intersection types

[gomoripeti]

@zuiderkwast wrote: What are the subtyping rules for intersection types? Do we need a rule for merging clauses, such as this?

A|C :: E
B|D :: F
---
fun((A) -> B; (C) -> D) :: fun((E) -> F)

As an example how do we check that:

fun( (integer()) -> integer();
     (float())   -> float() ) <: fun( (number()) -> number() )

[zuiderkwast]

Peter, we should sleep soon. It's 2:35.

[gomoripeti]

:D haha, ... maybe I won't sleep till new year, it's less then 24 hours, types are too exciting

[zuiderkwast]

OK, let's finish the beta release before the end of the year! :laughing:

[UlfNorell]

I find it helpful to think of f :: A -> B (pardon the syntax) as a promise that ∀ x :: A. f(x) :: B. This may or may not actually be true due to exceptions and non-termination but this is what we intend with the type.

Applying this to the problem (A -> B); (C -> D) :: E -> F, we assume we have f :: A -> B and f :: C -> D and we need to decide whether f :: E -> F. In other words we have

∀ x :: A. f(x) :: B
∀ y :: C. f(y) :: D
z :: E

and want to know if f(z) :: F. In order to say anything about f(z) we need z :: A | C (and thus E :: A | C), since we only know something about fs behaviour on A and C.

Once we know z :: A | C we can conclude f(z) :: B | D so if B | D :: F we are done. However this is a bit too strict. We would like to have (for instance) (A -> B); (C -> D) :: A -> B. Time for an ASCII Venn diagram:

A----------+   
|     +----+------+
|     |    |      |
|  E--+----+--+   |
|  |//|XXXX|\\|   |
|  |//|XXXX|\\|   |
|  +--+----+--+   |
|     |    |      |
+-----+----+      |
      +-----------C

If z is in the // part we know f(z) :: B and in the \\ part f(z) :: D. According to the documentation A and C cannot overlap (although it also says you should get a warning if they do, which I'm pretty sure is a lie), so we could assume the XX part to be empty. In that case we'd like to check ResTy :: F where

ResTy = case {glb(A, E), glb(C, E)} of
        {none(), none()} -> none();
        {none(), _}      -> D;
        {_, none()}      -> B;
        _                -> B | D
    end

Allowing overlap would be a little more work and require us to subtract the \\ part from the // part and vice versa.

Putting it all together and generalising to multiple clauses we get something like (warning: not production code):

subtype({isect, Funs}, {fun, Arg, Res}) ->
  subtype(Arg, union([ Arg1 || {fun, Arg1, _} <- Funs ]),
  ResTy = union([ Res1 || {fun, Arg1, Res1} <- Funs, glb(Arg, Arg1) /= none() ]),
  subtype(ResTy, Res)

[zuiderkwast]

Thanks for a good lecture and beautiful ASCII art! :100:

A and C cannot overlap (although it also says you should get a warning if they do, which I'm pretty sure is a lie)

Perhaps we can give a warning for this. It provides a reason to incorporate gradualizer in OTP. :grin:

As long as there is no syntax for writing intersection types as a return type or an argument type, we don't need to support intersection types in the 2nd argument of subtype, I suppose.

[Zalastax]

A and C cannot overlap (although it also says you should get a warning if they do, which I'm pretty sure is a lie)

I've gotten dialyzer warnings about overlapping domains, so I believe the warning is there.