Display multiple example types to the user in situations where we do not necessarily have a most general type

[byorgey]

In order to always be able to infer a most general type, we would have to expose a lot more complex features in the surface-level type system (qualified polymorphism, subtyping constraints, ...). The resulting types would be long and complex. So we don't do that. At the moment we can infer parametrically polymorphic types (e.g. \x.x is inferred to have type a -> a), but if there are any constraints at all (qualifiers, subtype constraints...) on a type variable then we monomorphize it before showing the result to the user. This is sound but it leads to some unexpected behavior. For example:

Disco> :type \x. x - 3
λx. x - 3 : ℤ → ℤ
Disco> :type (\x. x - 3) (1/2)
(λx. x - 3) (1 / 2) : ℚ

First, \x. x - 3 is inferred to have type ℤ → ℤ, which is certainly a valid type for it. It may be surprising, then, that the second example type checks at all: surely we are not allowed to apply a function expecting ℤ to a fraction? And indeed, if we define our own function explicitly of type ℤ → ℤ then we can't:

Disco> :type let f : Z -> Z = \x. x - 3 in f (1/2)
Unsolvable NoUnify

What's actually going on here is that \x. x - 3 is internally inferred to have a type like (N <: a, QSub a) => a -> a, that is, it has type a -> a for any a which supports subtraction and is a supertype of N; however, we can't show that to the user so we monomorphize it first, arbitrarily choosing Z for a, although Q also would have been a valid choice. However, typechecking the expression (\x. x - 3) (1/2) generates an additional constraint F <: a, and in that case Q is the only valid choice for a.

So in the case of :type \x. x - 3 I'm imagining showing the user something like this instead:

Disco> :type \x. x - 3
λx. x - 3 : (ℤ → ℤ) OR (ℚ → ℚ)

(or maybe putting each type on a separate line, or some other nice way of showing them).

In an ideal world, I would love if we could show the user a single type ONLY when we are sure it is the most general type or the only possible type. I think this should be possible if we are conservative; I don't know if it is possible to decide in general (that is, there may be situations where we show multiple monomorphized types even though there is some single most general type we could have shown?). To do a better job picking most general monomorphic types when possible we will definitely want to do something like #163 .

The other big caveat is that it's east to come up with expressions having a very large number of potential monomorphized types. For example, \a1. \a2. \a3. ... \an. a1 + a2 + a3 + ... + an has something like 4^n different types, depending on which specific numeric types we pick for each of the arguments. So in general we would probably need to cut it off at some point and just show a few options with a ... at the end, or something like that.

[byorgey]

Some preliminary code for this is in the multitype branch, https://github.com/disco-lang/disco/tree/multitype . A comment on the commit there explains what still needs to be done: https://github.com/disco-lang/disco/commit/f1ee1415bd8a9e5cc68ed640c800c69d6f1b24ad , reproduced below for ease of reference:

Mostly works, but still some combinatorial explosion problems. I think it should be ameliorated by keeping track of variable polarities and choosing solutions accordingly. We only need to generate multiple solutions for variables that occur in both positive and negative positions. Write a function to go through a type and return all its type variables but with a polarity for each. Then pass that in when calling the solver with a bunch of constraints.

[byorgey]

Note, simply finding polarities of variables in a type is not by itself enough. We also need to deal with the many unification variables generated during typechecking & constraint generation. Maybe it has to do with whether a particular unification variable occurs only as a subtype in constraints, as a supertype, or both? And maybe the polarity of variables it is related to?

[byorgey]

Abstractly, given the complete set of types $T$ which a term could have, we only want to display all the minimal ones with respect to subtyping. That is, if $\sigma, \tau$ are both elements of the set of possible types, but $\sigma <: \tau$, then we can omit $\tau$. Said yet another way, we want a minimal subset $T' \subseteq T$ such that every element of $T$ is a supertype of some element of $T'$.