Language extension to allow qualified polymorphic types in top-level type signatures

[byorgey]

There's no reason we shouldn't allow qualified types to show up if students are ready for them.

See also #169.

[byorgey]

Also needed to write reasonable types for things like

injective : (a -> b) -> Prop
injective(f) = forall x y. (f(x) == f(y)) ==> (x == y)

which is (rightly) rejected because we need to know that a and b support comparison.

[byorgey]

Make this a language extension which is off by default?

What should the syntax be? Options include:

1. Use Haskell-like syntax, like comparable a => (a -> b) -> Prop
2. Put annotations on type variables inline, like (comparable a -> b) -> Prop or (a[comparable] -> b) -> Prop)
3. Put qualifiers AFTER the type, like (a -> b) -> Prop [comparable a]

I think I like putting qualifiers after the type. Not sure of the best syntax.

[byorgey]

Don't let perfection become the enemy of good. Just put it in with some syntax; the syntax is easy to change later! I think I will go with type [qualifier, qualifier ...]

[byorgey]

Worked on this for a while. Unfortunately it turned out to be much more annoying than I thought.

• Having qualified types result from inference is problematic, since in the general case we would need subtyping qualifiers as well. For example consider

  • \x y. x + y
  • \x y. x + 3

  The first one could be inferred to have type a -> a -> a [numeric a]. And you would think the second one could have the same type, but this is much trickier because we get two unification variables with some subtyping constraints between them and the base type N, as well as a numeric qualifier. In general it seems very hard to decide on a nice type to result from inference, and it would seem very magic to know when the system will infer a polymorphic type and when it will monomorphize things (as it does for all types now).

  So I think inferring qualified polymorphic types is out. (Though we could still imagine returning multiple types from type inference; see #169 .)

• Checking qualified polymorphic types seems more promising. Parsing is no problem. However the difficulty right now is this code: https://github.com/disco-lang/disco/blob/09559caa8fa0b166fc8b0aea4b7ed60d73d8bb6a/src/Disco/Typecheck/Solve.hs#L217-L222 The problem is that if there is a variable which is in the SortMap but doesn't participate in any constraints, at this point we have forgotten if it is a skolem or a unification variable! Even worse, for skolems which are in both the SortMap and constraints, this code will add the variable to the constraint graph as a unification variable, which the constraint graph solver (rightly) rejects.

[byorgey]

I've been working on this some in the qualified-types branch. Checking of top-level declarations with qualified polymorphic types now seems to work properly. For example, if poly-qualified.disco contains

lt : a -> a -> B [comparable a]
lt x y = x < y

add : a -> a -> a [numeric a]
add x y = x + y

then loading it works properly:

Disco> :load poly-qualified.disco
Loaded.
Disco> :names
add : a -> a -> a [numeric a]
lt : a -> a -> Bool [comparable a]

(On the other hand if we change, e.g., x < y to x + y then the file no longer type checks.)

The problem, however, is with using such definitions. We can already see problems if we just ask for the type of lt explicitly; the qualifier disappears:

Disco> :type lt
a -> a -> Bool

What's worse, we can call lt or add on arguments which don't satisfy the required qualifications:

Disco> add 3 5  -- ok
8
Disco> add "hi" "there"  -- o noes
user error (Pattern match failure in do expression at src/Disco/Interpret/Core.hs:978:3-11)

The problem seems to be that any code path which goes through infer or inferTop loses the information about qualifications, but I don't think I yet completely understand what's going on.

[byorgey]

Oh! Duh, the problem was that when opening up the type of something with a qualified polymorphic type (i.e. replacing the bound type variables with fresh unification variables) we have to also generate appropriate constraints based on the qualifiers. I had this code before but removed it due to my own confusion when fixing a different part of the code that seemed similar.

Now the above problems don't happen any more:

Disco> :load poly-qualified.disco
Loaded.
Disco> :type add
add : ℕ → ℕ → ℕ
Disco> add 3 5
8
Disco> add "hi" "there"
Unsolvable (Unqual QNum (TyCon (CContainer (ABase CtrList)) [TyAtom (AVar (V Unification a1))]))

However, notice that when asking for the type of add we get a monomorphized type. This is related to #169 . We might also consider adding a special case for the common case of :type <variable>, just looking up and displaying its type directly instead of going through the whole type inference pipeline.

A problem remains, however, which is basically just #177 :

Disco> lt 3 5
true
Disco> lt "hey" "there"
primValOrd: impossible! (got VCons 1 [VNum Fraction (104 % 1),VIndir 18], VCons 1 [VNum Fraction (116 % 1),VIndir 19])
CallStack (from HasCallStack):
  error, called at src/Disco/Interpret/Core.hs:1572:5 in disco-0.1.0.0-BsfB4k71bByBVmoIY8iZUq:Disco.Interpret.Core

[byorgey]

Another issue:

injective : (a -> b) -> Prop [enumerable a, comparable a, comparable b]
injective(f) = forall x, y. (f(x) == f(y)) ==> (x == y)

This does not typecheck since it complains that some unification variable (which it assigned to x and y) is not searchable. We would like to write something like

injective : (a -> b) -> Prop [enumerable a, comparable a, comparable b]
injective(f) = forall x : a, y : a. (f(x) == f(y)) ==> (x == y)

but this is currently rejected since x : a is not a valid pattern. It seems we need something like ScopedTypeVariables. Some initial thoughts on what would be required:

1. Currently termToPattern only allows TAscr if the PolyType is vacuous (i.e. there are no bound type variables). This would need to be changed.
2. To make this all work we really need to implement #177 : e.g. in this example the runtime type at which injective is called needs to be passed along to the forall so that we know how to search and how to compare for equality.
3. Up until now we've just been relying on the mechanisms of unbound-generics to keep track of which variables are bound by which binders. However, having type variables in a declaration scope over the definition would (I think) require some really invasive changes to the AST type and the way parsing is handled. We might need to bite the bullet and implement a real name resolution phase.

Alternatively, perhaps we could just write forall x, y. ... and try a bit harder to infer that the type of x and y must be a. I don't know if that would work in general. Right now we immediately throw a NoSearch error in the typecheck function if the type of the binder can't be immediately inferred to have a searchable type. We would have to generate a constraint instead. The problem (and the reason, I think, that we didn't do this before) is that searchability doesn't break down nicely via atomic rules like the other qualifiers do. However, I wonder if we could just keep it around as a non-atomic "wanted" constraint and make sure that it is eventually satisfied.

[byorgey]

Hmm, the commit above added a special case for inferTop on variables; we might want to add the same special case for prims, so if you type e.g. :type ~+~ then you get to see ~+~ : a -> a -> a [numeric a] instead of N -> N -> N (if the QualifiedTypes extension is enabled).

Ah, edited to add: this is actually problematic since we don't store types of prims directly as PolyTypes; the inferPrim function just makes up some unification variables, generates constraints, etc. In fact some prims (for example, exponentiation) don't even have nice most general types that could be written using qualified polymorphism at all. Really we'll just have to implement #169.

[shaylew]

Alternatively, perhaps we could just write forall x, y. ... and try a bit harder to infer that the type of x and y must be a. I don't know if that would work in general. Right now we immediately throw a NoSearch error in the typecheck function if the type of the binder can't be immediately inferred to have a searchable type. We would have to generate a constraint instead. The problem (and the reason, I think, that we didn't do this before) is that searchability doesn't break down nicely via atomic rules like the other qualifiers do. However, I wonder if we could just keep it around as a non-atomic "wanted" constraint and make sure that it is eventually satisfied.

There were a couple of reasons we punted on polymorphic searches, AFAIR:

1. (As you mentioned) searchability constraints don't decompose nicely. It's basically an overlapping instances situation, where if you want to figure out whether A -> B is searchable you can get there through any one of the following cases but can't immediately determine any specific constraints on A or B:

   • A is finite and B is searchable
   • A is empty (no constraints on B)
   • B is empty or unit (no constraints on A)

   (The overlap in the last two rules does actually lead to an "instance" with different behavior, but if we're passing types at runtime instead of building dictionaries we don't have to figure out ahead of time which rule applies as long as we guarantee one of them will.)

2. Allowing un-annotated quantifier bindings led to surprising behavior with defaulting, e.g. forall x. x >= 0 holds because we silently default x to type N in the absence of any other information about it. This is pedagogically (and ergonomically) less than ideal.

Allowing us to emit non-atomic wanted constraints and later either resolve or quantify over them does seem like the right way to deal with (1). And (2) could be dealt with less heavy-handedly by waiting until just before defaulting would otherwise happen to complain about a quantification at an under-constrained type -- it's fine to end up with a skolem in the searched type, it's just unsolved unification variables that present an issue.

[byorgey]

Ah, right, thanks for refreshing my memory on some of these things (and writing them up so future-me's memory can also be refreshed).

As classes are starting next week (entirely online) I'm probably not going to have much time to think about this for a while. Though I may occasionally work on it if I need something to distract me. =)

[byorgey]

I recently had a stroke of inspiration regarding the need for something like ScopedTypeVariables: the more principled way to do this, perhaps, is to allow explicit type lambdas. I was already thinking about introducing them implicitly to solve #177 . Then we could write

injective : (a -> b) -> Prop [enumerable a, comparable a, comparable b]
injective(f) = \a:Type, b:Type. forall x : a, y : a. (f(x) == f(y)) ==> (x == y)

Or possibly with different syntax for the type lambda. Of course, this is getting pretty baroque and it raises the question, why not just build injective into the language as a special primitive? But I do think making it possible to define injective in a library like this may lead to other benefits; that is, given these facilities there are probably other cool things we could define as well.

[byorgey]

I want to see how this all works with the latest changes that have been made to the type system etc. I've been working on merging the latest master branch into the old qualified-types branch, but it's a doozy. Hopefully I'll get it up and running again soon.