Support polymorphism

[dhess]

It's unclear whether we should do this before user-defined types (#88). If we do it before those, we'll need at least something like a built-in Maybe or List type.

[dhess]

Notes from our 2020-12-02 priorities meeting:

• @brprice and @dhess expressed some concern about implicit type applications and good error messages. Also on principle we try to design around being explicit, even if it's more hassle, with the idea that it's easier to understand.
• @hmac points out that explicit type applications (as we did for Alpha), while possibly easier to implement, is more painful for users.
• Therefore @brprice will investigate an implicit style. @hmac suggests we look at Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism.
• We may want to change our representation of bound variables before doing this!

[dhess]

@brprice mentioned that #81 is possibly relevant here.

[brprice]

(Mostly a note to myself, as I was rather confused about this point. However, it may be food for thought when we design the syntax of our language)

I'm looking at Dunfield and Krishnaswami, where they have a fully implicit calculus (i.e. both type applications and type abstractions are invisible, a la Haskell without TypeApplications). This has some weird drawbacks (roughly scoped type variables style stuff familiar from Haskell), but in particular they have forall bindings in annotations scoping over the annotated term:
(λx . x : a -> a) : forall a . a -> a is a perfectly valid term, even though it looks like it has unbound as! However, this is not entirely straightforward - it doesn't happen in all cases, as in g : Nat -> forall a . a -> a ⊢ g 1 : forall a . a -> a as we don't actually "unwrap" the forall binder there. I also have no idea how the paper handles the interaction with this and alpha-equivalence!

(The term above synthesises forall a . a -> a as one would expect. The simpler term λx . x : forall a . a -> a does as well.)

I wonder if a good solution for our surface language is to have optional (maybe mandatory?) type abstraction binders in terms, simply to bring variables into scope so we can put them in annotations when required.

[brprice]

Further note, the 2019 paper https://research.cs.queensu.ca/home/jana/papers/gadts/Dunfield19_GADTs.pdf extends their higher-rank work to GADTs

[dhess]

Shall we promote this to high priority now?

[brprice]

Status: I think it will be ok to just implement the algorithm in Dunfield-Krishnaswami, assuming I can make it work ok with holes.

In the long run, to nail down the language, it would be worth thinking about the strange things GHC does in https://github.com/ghc-proposals/ghc-proposals/blob/wip/spj-deep-skol/proposals/0000-simplify-subsumption.md, and whether we explicitly care one way or the other about any of them. Also, we should consider whether to enforce, tolerate or forbid explicit type application and abstraction. [I think we are agreed that alpha-style enforcement is very clunky and awkward to use -- that is kind of the point of this bug report! But should we tolerate it, or forbid it? D&K forbid it, and I have not yet thought about if their algorithm can tolerate optional type applications/abstractions without much fuss]

[dhess]

[I think we are agreed that alpha-style enforcement is very clunky and awkward to use -- that is kind of the point of this bug report! But should we tolerate it, or forbid it? D&K forbid it, and I have not yet thought about if their algorithm can tolerate optional type applications/abstractions without much fuss]

I tried to make a point related to this during today's wrap-up call, but probably not very well. What I was trying to get at was this: what was clunky and awkward in Alpha might not be clunky or awkward in a structure editor like Vonnegut, especially if we make accommodations in the editor to make it easier. So we should be careful of drawing conclusions from Alpha (or any other text-based language) about what's ergonomic in a structure editor, because the context might be very different.

Of course, there are also two caveats to what I've just said, as well: 1. this works both ways (what is obvious/convenient in text editing might not be in a structure editor), and 2. it might still be clunky or awkward in Vonnegut, just in a different way!

[brprice]

I'm going to split this into four parts:

• Support explict-style polymorphism with no inference changes. This will get a whole bunch of stuff unblocked, like representing things well in the frontend (e.g. how does tuple-style arrows work with forall types). See hackworthltd/vonnegut#291 (EDIT: completed in hackworthltd/vonnegut#291)
• Higher kinds, unblocking parameterised ADTs. (mostly done as part of hackworthltd/vonnegut#291, but frontend cannot yet write ∀(a:*->*).…) (EDIT: backend/api completed in feat: display and edit kinds on foralls #1120)
• Do some "usage tracking" for type holes (this is probably Improved inference #81)
• Take another crack at implicit-style polymorphism and type inference, thinking about how it works with an interactive structure editor.

[dhess]

Imported from our "Useful links for Primer" issue:

• Polymorphic Gradual Typing with Holes: http://jssst.or.jp/files/user/taikai/2020/PPL/ppl3-4.pdf (Apparently they are collaborating with Cyrus Omar on extending Hazelnut.)

• Graduality and Parametricity: Together Again for the First Time: https://www.ccs.neu.edu/home/amal/papers/gradparam.pdf (Cited by Polymorphic Gradual Typing with Holes paper above.)

[dhess]

I think we can close this issue, yes? We've had a robust polymorphism implementation for over a year now, and while I think it could benefit from some improved inference, that should arguably be tracked separately.

[dhess]

I'm going to close this. #81 has some ideas for how we could improve inference in some specific cases, but polymorphism support is "done."