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

Wed Mar 28 17:10:06 UTC 2018

Agreed with all points Simon makes below -- including on punting on #102 with a personal hope to return some day not too distant from now. I'll update the proposal with my analysis from the email.

Richard

> On Mar 27, 2018, at 6:11 PM, Simon Peyton Jones <simonpj at microsoft.com> wrote:
> 
> 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