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

[Simon Peyton Jones]

I said three weeks ago:

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

Richard agreed to punt on #102.

Are we agreed to accept these two?
 * #54 https://github.com/ghc-proposals/ghc-proposals/pull/54
 * #81 https://github.com/ghc-proposals/ghc-proposals/pull/81

RSVP.  I'd really like to unglue this log-jam!

Simon

PS: Richard hasn't yet formally submitted #54, but will do so later today


|  -----Original Message-----
|  From: ghc-steering-committee <ghc-steering-committee-
|  bounces at haskell.org> On Behalf Of Simon Peyton Jones
|  Sent: 27 March 2018 23:11
|  To: Richard Eisenberg <rae at cs.brynmawr.edu>; 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'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-
|  committ
|  | ee
|  _______________________________________________
|  ghc-steering-committee mailing list
|  ghc-steering-committee at haskell.org
|  https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-
|  committee