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

Tue Mar 27 22:11:00 UTC 2018

I'm on a train, and don't have access to the proposals, but here's are some thoughts:

* #54 is about letting users write kind signatures for type constructors,
  just as they can write type signatures for term variables.  It's
  amazing we have lasted so long without this ability, but it's really
  really hurting us.   I feel strongly that we should fix this: we need
  SOME way to write a kind signature for a type constructor.

* To write such a kind signature we need something like the
    T :: forall a b -> blah syntax, to indicate which of T's
  arguments should be written positionally (like the Int in Proxy Int)
  and which are hidden (like the * in Proxy Int).  By hook or by
  crook we must be able to express this.  And that's #81.

* The worry with #81 was whether it would be painting us into a
  corner.  Hence #102.  But I regard #102 as an existence proof that
  the corner has an exit, not as something we should espouse now.
  (Tell me if you disagree Richard.)  It is far off our radar, and
  premature to make a commitment.

  Richard: you could add the analysis in your email about "why 12"
  to the proposal.

So I suggest that we accept #54 and #81, and simply punt on #102.

Simon

| -----Original Message-----
| From: ghc-steering-committee <ghc-steering-committee-
| bounces at haskell.org> On Behalf Of Richard Eisenberg
| Sent: 27 March 2018 04:36
| To: Iavor Diatchki <iavor.diatchki at gmail.com>
| Cc: ghc-steering-committee at haskell.org; Joachim Breitner <mail at joachim-
| breitner.de>
| Subject: Re: [ghc-steering-committee] DH quantifiers (#102),
| Recommendation: accept
| 
| 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
| _______________________________________________
| ghc-steering-committee mailing list
| ghc-steering-committee at haskell.org
| https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee