Can we prove that type constructors are "distributive"?

[Blaisorblade]

In lampepfl/dotty#6023 @anatoliykmetyuk asked a theoretical question, and @smarter forwarded it to me, to investigate it in DOT.

I have not found a proof anywhere that F[A] & F[B] <:< F[A & B] for all covariant F[+_]. However, this property is featured in tests and docs, and there is a deliberate logic in the sources to distribute type parameters for covariant type constructors.

DOT assumes F[A & B] =:= F[A] & F[B], but F[A & B] <: F[A] & F[B] holds for any covariant F (because by covariance F[A & B] <: F[A] and F[A & B] <: F[B]), so F[A] & F[B] <:< F[A & B] is the only open question — and the DOT literature doesn't discuss it.

DOT doesn't have general type constructors (yet), but it has three primitive type constructors that are covariant: functions (x: A) => X, value members {a : X} and type members { A >: L <: X }. The existing DOT formalizations are silent on this issue, but I have a different DOT formalization where it's easier to check if a new typing rule is true (because you needn't modify existing proofs), and I have some initial results. I'll write them up in comments.

[HuStmpHrrr]

I am very interested in this issue too.

Did you mean Dotty assumes F[A & B] =:= F[A] & F[B]? Effectively, none of the distributivities (data fields, return types of functions) can be proved in general in DOT (in neither Wadlerfest DOT nor OOPSLA DOT), and each would require its own axiom. Adding those would add significantly more case analysis to DOT in the easiest case.

Another related question is, how distributivity should treat recursive types and record types? More fundamentally, should there be any distributivity between recursive types and record types? Lots of questions can be raised if distributivity and intersection types must come into play.

[Blaisorblade]

Did you mean Dotty assumes F[A & B] =:= F[A] & F[B]?

Yes, or so I hear from @smarter. And also F[A | B] =:= F[A] | F[B], and variants for all co-/contravariant types. The logic is in https://github.com/lampepfl/dotty/blob/master/compiler/src/dotty/tools/dotc/core/TypeComparer.scala, methods {and,or}Type, distribute{And,Or}, {glb,lub}Args, and it seems fully symmetric, but I haven't explored the exact consequences.

And indeed, that doesn't follow in DOT as published (only one direction does, e.g. F[A & B] <: F[A] & F[B] and F[A] | F[B] <: F[A | B]). But I'm working in Coq on a different proof approach.

Basically, I (and colleagues) map types to set of values, and then I study the properties of those sets of values — which is, arguably, how one explains types to programmers. But here we manage to use this formally and to handle abstract types (which require a different notion of sets). Slides on https://twitter.com/Blaisorblade/status/1097973979879559168.

One important caveat: the set of "values v of a type T" is defined here semantically; some of those values might correspond to code that behaves like elements of type T but is not given type T by the type system. For instance, the set of values in A => B is essentially the set of functions that, applied to arguments of type A, give results of type B.

Positive results

DOT primitive type constructors distribute in X. That is, ((x: A) => X1) & ((x: A) => X2) <: (x: A) => (X1 & X2), {a : X1} & {a : X2} <: {a : X1 & X2} and { A >: L <: X1 } & { A >: L <: X2 } <: { A >: L <: X1 & X2 }.

Positive conjectures

I also started working through other cases (intersections and recursive types), but I got interrupted halfway.

Contravariant constructors

Dotty seems to also assume (in something like G[A | B] =:= G[A] & G[B] and G[A | B] =:= G[A] & G[B] for contravariant G (in DOT, function types). Or at least, the code and @smarter suggested that (I haven't had a chance to test that out).

You can justify that '(A1 => B) & (A2 => B) =:= (A1 | A2) => B: a functionfgives aBfrom an argument in eitherA1orA2ifffmaps bothA1toBandA2toB`.

Potential problems

But since we're talking about functions, you should only expect laws from Heyting algebra (intuitionistic logic) to hold, not all laws from Boolean algebra (classical logic). But I'm not sure you can produce counterexamples in Scala for these failures, or that these problematic laws actually work in Scala. So, right now, these are open problems.

For instance, you also have that (A1 => B) | (A2 => B) <: (A1 & A2) => B, but the reverse seems to fail: if a function requires an argument in both A1 and A2, it doesn't mean the function is either in A1 => B or A2 => B. What's true is that you can only call (A1 => B) | (A2 => B) with arguments of type A1 & A2, so this might be okay?

Also (A1 => B1) & (A2 => B2) doesn't equal (A1 | A2) => (B1 & B2). You can write a function that gives a B1 on A1 and a B2 on A2, but that function never gives B1 & B2. However, I'm not yet sure the typechecker would ever assign type (A1 => B1) & (A2 => B2) to a function that isn't also in (A1 | A2) => (B1 & B2). Concretely, take this function in pseudocode

def f(a: ???) = a match {
  case a1: A1 => new B1()
  case a2: A2 => new B2()
}

Semantically, this function is in (A1 => B1) & (A2 => B2) but not in (A1 | A2) => (B1 & B2), but I think Dotty wouldn't recognize that. Still, I can't prove rule (A1 => B1) & (A2 => B2) =:= (A1 | A2) => (B1 & B2) is typesafe in general.

[smarter]

And also F[A | B] =:= F[A] | F[B]

No: https://github.com/lampepfl/dotty/blob/48233081c03918dc56662caca1353ded01a98843/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L1771-L1778

[Blaisorblade]

@sstucki In typesystems with variant subtyping, do you expect all laws from Boolean algebra (and not just Heyting algebra) to hold, including (co,contra)variant types distributing over intersections and unions? That is, do you expect F[A & B] =:= F[A] & F[B], F[A | B] =:= F[A] | F[B], G[A | B] =:= G[A] & G[B] and G[A & B] =:= G[A] | G[B] for covariant F and contravariant G? Some of the rules seem problematic, and I suspect that's about Boolean-vs-Heyting, but I haven't gotten to the bottom yet. Is this a known question in the literature?

[HuStmpHrrr]

I am not too worried about type equivalence.

if the problem is about what algebraic structures DOT should admit, then the approaches that have been taken so far are fundamentally mistaken: algebraic structures should come before subtyping.

the problem with distributivity and intersection types is more important: you cannot get { foo : A} /\ { foo : B} <: { foo : A /\ B } simply says foo cannot be of type A /\ B.

on the other hand, union types have no such problem: union types being the least upper bound can be relaxed to less precise types anyways. namely {foo : A} \/ {foo : B} <: {foo : A \/ B} is provable after all.

[LPTK]

@Blaisorblade in MLsub, which is a type system with subtyping, variance, record types, and recursive types, all these equivalences hold axiomatically in order to have the lattice properties required for complete type inference (see Fig.3 of the paper). The main difference between DOT and MLsub are, obviously, abstract, path-dependent and self types. No idea if they cause problems with this nice state of affairs. Also, Dotty has pattern matching on union types, which kind of breaks parametricity, so that could be another reason some of these properties might not hold.

Also (A1 => B1) & (A2 => B2) doesn't equal (A1 | A2) => (B1 & B2). You can write a function that gives a B1 on A1 and a B2 on A2, but that function never gives B1 & B2.

Why not? Of course, it can give B1 & B2. Consider:

trait A { def foo: Seq[Int] }
trait B { def foo: List[Any] }
class C extends A with B { def foo: List[Int] = Nil }
// C <: A & B
(new C : A & B).foo : Seq[Int] & List[Any]

Concretely, take this function in pseudocode

def f(a: ???) = a match {
  case a1: A1 => new B1()
  case a2: A2 => new B2()
}

Semantically, this function is in (A1 => B1) & (A2 => B2)

No, that doesn't make sense. Consider A1 = A2 = Any and B2 = Nothing. You would have f.type <: Any => Nothing, which makes no sense since only the first case is actually relevant to the function's semantics – the function should semantically be of type Any => B1. A more appropriate type could be (A1 => B1) & ((A2 \ A1) => B2) where \ denotes type difference.

[Blaisorblade]

@LPTK

You can write a function that gives a B1 on A1 and a B2 on A2, but that function never gives B1 & B2.

Why not? Of course, it can give B1 & B2

English ambiguity — I mean that you can write at least one function that never returns B1 & B2.

Concretely, take this function in pseudocode

def f(a: ???) = a match {
  case a1: A1 => new B1()
  case a2: A2 => new B2()
}

Semantically, this function is in (A1 => B1) & (A2 => B2)

No, that doesn't make sense.

Oh right, A1 and A2 should be disjoint in that example.

[Blaisorblade]

@HuStmpHrrr

the problem with distributivity and intersection types is more important: you cannot get { foo : A } /\ { foo : B } <: { foo : A /\ B } simply says foo cannot be of type A /\ B.

Not sure I'm parsing that sentence right. But { foo : A } /\ { foo : B } <: { foo : A /\ B } can be shown in my DOT model, even tho it doesn't follow from the existing rules (so we could add it as a type rule, and I'm doing it), while { foo : A /\ B } <: { foo : A } /\ { foo : B } is provable in standard papers.

on the other hand, union types have no such problem: union types being the least upper bound can be relaxed to less precise types anyways. namely {foo : A} \/ {foo : B} <: {foo : A \/ B} is provable after all.

Rules for intersections and unions are symmetric, so the rule you give follows by covariance but {foo : A \/ B} <: {foo : A} \/ {foo : B} doesn't (yet, just proved it in this model).

I am not too worried about type equivalence.

In DOT, type equivalence is just subtyping in both directions: A = B means A <: B and B <: A, so the two questions aren't distinct. And as far as I understand, when Dotty tests A <: B, it uses certain type equivalences to simplify both A and B.

if the problem is about what algebraic structures DOT should admit, then the approaches that have been taken so far are fundamentally mistaken: algebraic structures should come before subtyping.

I'm curious to hear more, but I expect that sort of statement is hard to explain in here. I hope there's a better chance at some point. It sounds like the philosophy in the MLSub paper and thesis, but I confess I don't understand the deeper parts of that thesis.

BTW: @LPTK thanks for the pointer to MLSub's rules.

The main difference between DOT and MLsub are, obviously, abstract, path-dependent and self types. No idea if they cause problems with this nice state of affairs. Also, Dotty has pattern matching on union types, which kind of breaks parametricity, so that could be another reason some of these properties might not hold.

Right now, an even bigger difference is how you give semantics to types. What MLSub does doesn't fit the paper, but their equations on types are preserved by adding values — which is not the case in my (much simpler) model. I was busy enough on abstract types that I was happy enough with intersections and unions when all the given rules worked.

Ignoring term variables, my type semantics [[ T ]] v (which says whether value v belongs to T) is defined so that [[ A /\ B ]] v = [[ A ]] v /\ [[ B ]] v and [[ A \/ B ]] v = [[ A ]] v \/ [[ B ]] v, and function types involve implication; both disjunction and implication are Coq's, hence they're constructive. That's the only reason I mention Heyting algebras; I haven't even proven that all Heyting algebra axioms hold here. In fact, Wikipedia mentions a "weak de Morgan law" ¬(x ∧ y)= ¬¬(¬ x ∨ ¬ y), and I don't know how to prove that here (or if I should expect it to hold); it surely doesn't hold as a type equality, and I can't even prove it as a biimplication.

[Blaisorblade]

@HuStmpHrrr

In DOT, type equivalence is just subtyping in both directions: A = B means A <: B and B <: A, so the two questions aren't distinct.

After skimming your WIP master thesis, let me step back to: in existing DOT papers and in my messages, the two concepts are identified. I'm not sure what happens in your thesis.

[Blaisorblade]

@smarter Thanks for the correction. But looking at distributeAnd, I suspect that (A1 => B1) & (A2 => B2) is still simplified to (A1 | A2) => (B1 & B2). Can you confirm that? Because that's the most surprising rule.

[HuStmpHrrr]

Not sure I'm parsing that sentence right. But { foo : A } /\ { foo : B } <: { foo : A /\ B } can be shown in my DOT model, even tho it doesn't follow from the existing rules (so we could add it as a type rule, and I'm doing it), while { foo : A /\ B } <: { foo : A } /\ { foo : B } is provable in standard papers.

Yes, because your method is logical relations and that means the semantics is compatible with this, but what I was saying is both Wadlerfest DOT and OOPSLA DOT cannot prove the first direction in general. I don't think what we said is contradictory here.

I have some issue in general with induced equivalence of preorders, because very often the definition is too broad to use (including mutual subtyping in DOT as you pointed out). Intuitively, we expect some equivalence that is more precise. For example, T1 /\ T2 == T2 /\ T1 holds without any concern of the context. This layer deserves its own equivalence, and this equivalence is purely algebraic and context independent. Then subtyping comes after this layer of equivalence, and this equivalence should be congruent in subtyping everywhere. I hope that makes sense. An analogy is definitional equality in Martin Lof theory. I kept thinking about it since last year, but had no time to see what if algebras are applied separately.

[sstucki]

In typesystems with variant subtyping, do you expect all laws from Boolean algebra (and not just Heyting algebra) to hold, (...)

@Blaisorblade, the short answer is: I don't know.

I don't know of any system in the literature that combines 1) higher-order subtyping, 2) variance tracking and 3) intersection/union types, though there are plenty of system that feature 2 out of 3 of those (cf. Adriana Compagnoni's work on HO-subtyping with intersections). Maybe the algebraic subtyping people have more to say about this, but I don't know much about these systems.

I'm a bit confused about the question though. I'm not sure what Heyting vs. Boolean algebras have to do with this. It's not like Heyting algebras don't feature distributive laws, and I don't see how Boolean algebra would help to answer this question either. Neither of these algebras have much to say about type constructors in general, apart from those that happen to correspond to the algebraic operations (union, intersection, implication, bottom, top). Here's an example: as you noted yourself, sets form a Boolean algebra (with intersection, unit, set complement) but sets having a Boolean structure has nothing to say about whether e.g. the cartesian product operator preserves this structure, simply because cartesian products are not part of the language of Boolean algebras.

What you really want to know is whether arbitrary type constructors are homomorphic (or functorial) w.r.t. the lattice structure. But I'm afraid that question isn't easily settled by looking at existing DOT papers or individual set-theoretic models. Existing DOT papers don't tell you what ought to be true (only what has been proven to work), while set-theoretic models can give an intuition, but may be misleading. Here's an example: I can easily define a set-theoretic function that is monotone but not homomorphic w.r.t. to limits (i.e. doesn't "distribute"): define f({}) = {} and f(A) = {*} for any non-empty A. Since the empty set is a subset of any other set, this is clearly a monotone function, but f({1}&{2}) = f({}) = {} != {*} = {*}&{*} = f({1}) & f({2}). Hower, f is probably not definable in DOT (or most other sensible type systems). What your model may be able to answer is whether all the basic type formers in DOT preserve limits, and that may be enough to prove that any operators definable within some sort of HO DOT/Scala should be too.

Not sure whether this is helpful.

[LPTK]

@Blaisorblade

I mean that you can write at least one function that never returns B1 & B2.

What examples do you have in mind, besides pattern matching?

I really don't think intersections should be used to type pattern matching (match types should be used there), or to type overloading either, for that matter (which is another thing intersections have been proposed for, but the operational semantics would require somehow reifying subsumptions or using runtime types reflectively). I think it's much better to get these two ill-behaved applications of intersection types out of the way, if that allows us to make function types behave more algebraically.

By the way, food for thought: in a system where pattern matching can refine types and where unions can appear in negative position (neither is true in MLsub), it's a loss of information to go from something like { tag: 0, a: Int } | { tag: 1, a: Bool } to { tag: 0 | 1, a: Int | Bool }. See also https://github.com/lampepfl/dotty/issues/5420. I'm pretty sure a system that allows such "dependent" refinements in pattern matching could be used to encode GADTs (since we can put abstract types in those record types too). So, given type F[+A,+B], we should indeed have that F[T0, T1] | F[S0, S1] is not the same as F[T0 | S0, T1 | S1] (take type F[+A,+B] = { tag: A, a: B }), which goes in the same direction as the quoted comment in @smarter's answer, though the example of the comment itself is not convincing. I don't see why List[T] | List[U] should not be the same as List[T | U] – for all intents and purposes they can only behave the same, AFAICT (due to type erasure preventing matching them apart).

[smarter]

Not sure whether this is helpful.

I for one found it helpful :)

[smarter]

I don't see why List[T] | List[U] should not be the same as List[T | U] – for all intents and purposes they can only behave the same, AFAICT (due to type erasure preventing matching them apart).

Hmm, I can't remember if something goes wrong when you assume distributivity given the current typing rules, but doing so would prevent future improvements I think, e.g.:

object Test {
  def foo(l: List[Int] | List[String]) = l match {
    case (x: String) :: xs =>
      val z: List[String] = xs // Doesn't work, but should
    case (x: Int) :: xs =>
      val z: List[Int] = xs // Same
    case Nil =>
  }
}

This doesn't work at all currently (in fact, the pattern matcher seems very confused by this example), but it seems like something we could implement (/cc @liufengyun @AleksanderBG to correct me if I'm wrong), and it relies on List[Int] | List[String] being a proper subtype of List[Int | String].

[Blaisorblade]

@sstucki Thanks for the prompt reply!

What your model may be able to answer is whether all the basic type formers in DOT preserve limits, and that may be enough to prove that any operators definable within some sort of HO DOT/Scala should be too.

Indeed, that’s what I can do right now without changing the model. One could then try some day to model variant type constructors as functions that are not just monotone but also distributive in some sense. But that’s for a future time. Re Heyting vs Boolean, that might indeed be unrelated.

While speculating on alternative models: @HuStmpHrrr What you say suggests one could (1) first quotient types by the equivalences we demand (2) then try defining a logical relation on quotiented types, so that it’s forced to respect all the equations (including ones that currently don’t hold, e.g. the ones on functions that hold in MLSub but not here). I suspect logical relations on calculi with non-trivial type equivalence (say, definitional equality) can be described this way, tho I haven’t seen this point brought up. I’ve never seen this attempted for congruences other than definitional equality, and it sounds much harder than what I’m doing; one would have to study the world of MLSub types to see if this has a chance of working.

[Blaisorblade]

@LPTK

What examples do you have in mind, besides pattern matching?

Nothing concrete. I just know my semantics supports this example, and I don’t know if it’s a bug or a feature. If it’s a bug, it’s far from trivial to fix.

[abgruszecki]

I don't see why List[T] | List[U] should not be the same as List[T | U] – for all intents and purposes they can only behave the same, AFAICT (due to type erasure preventing matching them apart).

Hmm, I can't remember if something goes wrong when you assume distributivity given the current typing rules, but doing so would prevent future improvements I think, e.g.:

object Test {
  def foo(l: List[Int] | List[String]) = l match {
    case (x: String) :: xs =>
      val z: List[String] = xs // Doesn't work, but should
    case (x: Int) :: xs =>
      val z: List[Int] = xs // Same
    case Nil =>
  }
}

This doesn't work at all currently (in fact, the pattern matcher seems very confused by this example), but it seems like something we could implement (/cc @liufengyun @AleksanderBG to correct me if I'm wrong), and it relies on List[Int] | List[String] being a proper subtype of List[Int | String].

@smarter this is a wonderful example! I think we'll be able to type it properly once we allow constraining l.type (or the singleton type of scrutinee in general) by matching on it.

[Blaisorblade]

Today I realized that distributivity fails in DOT already with intersections and unions. The missing rule is Γ ⊢ (S ∨ T) ∧ U <: (S ∧ U) ∨ (T ∧ U), which makes DOT types into a distributive bounded lattice (like MLSub); the other direction is already provable, and distribution of unions over intersection follows. Of course that rule is provable in my model, since I interpret types as predicates (and yes, I've proved it in Coq).

The standard DOT rules make DOT a bounded lattice; distributivity cannot be proven, at least not from the bounded lattice laws, because there exist bounded lattices that are not distributive. Other subtyping rules complicate the picture, but it'd be strange if they allowed proving distributivity.