[ghc-steering-committee] DH quantifiers (#102), Recommendation: accept

Tue Mar 27 03:35:42 UTC 2018

I'd like to restart this thread, both as the Grand Poobah of Dependent Haskell and because Proposal #102 (this one) is holding up #81 (the `forall x y z ->` syntax), which is, in turn, holding up #54 (a plan to eliminate the need for CUSKs), which is implicated in quite a few bugs.

I think Iavor makes some good criticisms below, which I'll address individually:

> On Feb 23, 2018, at 12:12 PM, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:
> 
>     * it is premature to "reserve" syntax for a future extension

This is a hard one. The full implementation of dependent types in Haskell is still years away. But decisions we make now may affect the eventual concrete syntax. While a ghc-proposal is ill-fitted with reserving syntax, I think Roman was right to request that #81 be considered in the context of the larger syntactic changes. Maybe the "right" answer here is for the committee to conclude that the proposed syntax is generally plausible, paving the way for #81 but without making a solid commitment. On the other hand, if we can identify a better syntax for the overall design of dependent types in Haskell, that might affect the syntax used in #81/#54.

>     * I am not convinced that a design with 12 quantifiers is what I'd want to use

Neither am I!

For a moment, let's take the desire for dependent types to be a given. (I'll address this more below.) GHC currently has 3 quantifiers (`forall a.`, `ty ->`, and `ty =>`). To preserve type erasure, we need to distinguish between arguments needed at runtime and those that can be erased.

Coq does this through its Set-vs-Prop mechanism, where erased arguments live in their own sort. Such a route is viable for Haskell, I think, but I've never been much enamored of it, personally. For example, the Nat in a vector type really can be erased, while Nats in many other places can't be, and it seems a shame to need two different Nat types to pull off this dichotomy.

Agda uses the term "irrelevant" to describe type indices that are ignored during type equality checks. This is related to the type erasure property, but it's not quite the same thing. It's unclear to me what types Agda can erase, and I don't think Agda gives any solid guarantees as to erasure. (As a language aiming for performance, Haskell needs to provide such a guarantee.)

Idris does whole-program analysis to determine erasability. I can't imagine this scales well.

The choice I've made in the design of Dependent Haskell is to have the user choose whether to keep an argument or not, leading to the forall/foreach distinction. This brings us from 3 quantifiers to 4. In truth, 4 is enough to power dependent types! But read on.

All dependently typed languages give a facility for the user to control the visibility of arguments. If we want to do the same, we go from 4 quantifiers to 6. (We don't go to 8 because the original -> and => already differ in visibility.) Note, though, that Coq doesn't consider visibility as a feature of a type, instead using, essentially, pragmas to control visibility. This has some benefits (higher-order usages of functions can't fall over based on visibility), but it doesn't seem well-suited for Haskell.

Quite separately, we also will likely want to allow currying in type-level operations. Partially-applied type families are currently forbidden because doing so would wreak havoc with type inference. (Imagine if we're unifying `m a` with `Maybe Int` but that `m` might unify with a type family `Id`!) The solution I've proposed here is a notion of *matchability*, described in Section 4.2.4 of my thesis (which can be read independently of the rest of it). A function is *matchable* iff it is generative and injective -- in other words, if equalities over function applications can be decomposed. When some functions (like Maybe and Either Int) are matchable and some (like Id and any other type family) are not, then type inference can decompose matchable things and not decompose unmatchable things. It turns out that all previous 6 quantifiers are useful in both the matchable and unmatchable varieties, bringing us to 12.

Note that other dependently typed languages don't have a notion of matchability. They generally also don't have injective type constructors (you can't derive (a ~ b) from (Maybe a ~ Maybe b)) and don't have the guess-free type inference Haskell has. Instead, those languages generally rely on higher-order unification, which is a best-guess algorithm (as I understand it). GHC has stayed away from guessing. We might imagine a future for GHC that allows partially-applied type functions without using matchability, but I conjecture that any such future would also have to offer weaker guarantees for the predictability and stability of type inference. It might be a fruitful debate to see which is better -- stable type inference or fewer quantifiers.

My bottom line: I don't like the 12 quantifiers either. And dependent types require really only 1 new one. Two more come along for the convenience of invisible arguments. And then we have to double for matchability. (Note that matchability can be considered quite orthogonally to dependent types -- it has even been proposed separately in #52.) Perhaps I've overshot in the design here and some healthy debate here can whittle the number down.

>     * I am not convinced about the utility of the "dependent haskell" extension in the first place.

This is the bigger question. Chapter 3 of my thesis lays out some motivation for dependent types, as does Chapter 8 of Adam Gundry's. Historically, every feature (fundeps, type families, GADTs, kind polymorphism, higher-rank types, type applications) that has moved GHC closer to having dependent types has been eagerly adopted. I've heard some push-back over the years about this, but the biggest complaint I've gotten is around termination: people don't want GHC to reject non-terminating functions. When I explain that doing so has never been part of the plan, then generally the objection is retracted.

What are the downsides of adding dependent types?

- The language becomes more complicated. Haskell already has a reputation of being impossible to learn, and if dependent types appear everywhere, this reputation will be reinforced, to the language's detriment. I am indeed worried about this. Care will have to be taken by library authors to make dependent types an opt-in experience.

- Error messages might worsen. I'm actually not terribly worried about this, as I believe clever engineering can avoid it. Other than #11198 (which is now fixed), there has not been a degradation in error messages from -XTypeInType. Errors still use the words "kind" and "type" to mean different things! Even forgetting about dependent types, I think GHC's error messages need an overhaul, basically to become more like Idris's. (That is, interactive.) Especially if we have interactivity in error messages, then there are even more ways to mitigate the potential trouble of dependent types. Note that Haskell's tradition of language extensions help us here: if a user makes a type error in simple code -- but that code might have a meaning in a dependently typed setting -- then we can use the presence or absence of language extensions to tailor the message. (In particular, we might want to be conservative in recommending that the user enable -XDependentTypes.)

- The abstraction will sometimes leak. The most glaring example of this is when the type of ($) started muttering about levity polymorphism. That was terrible! I do think that, with care, we can avoid this, by continuing to use compiler flags to tailor output and/or adding interactivity to GHC's output.

- The implementation becomes more complicated. Well, yes, though perhaps we'll lose some duplication once GHC no longer has separate Expr and Type types.

-----------------------------------------

What to do next? If others on the committee are worried about the desire/utility of dependent types, it might be good to seek input from the community. Beyond that, I'll reiterate 4 possible actions we might take on #102, specifically:

1. Reject the syntax. If we do this, I'd love to open a larger conversation of ways forward -- do we want tweaks to the syntax or a wholly new approach?

2. Put this idea on hold, with a plan to accept or reject #81 on its own merits.

3. Accept the proposal, but put implementation on the back burner. This would serve to reserve the syntax, without burdening our users until the features are more fully-formed.

4. Accept the proposal and plan to implement.

Looking forward to seeing your thoughts on this,
Richard