[ghc-steering-committee] Please review #378: Support ergonomic dependent types, Shepherd: Simon PJ

Thu Mar 11 22:17:56 UTC 2021

Hi Vlad,

Very good points. Allow me to respond.

> On Mar 11, 2021, at 10:49 AM, Vladislav Zavialov (int-index) <vlad.z.4096 at gmail.com> wrote:
> 
> There are a few issues I see with this proposal. Let me first enumerate the issues, and then I will offer possible solutions.
> 
> 1. The proposal does not live up to its name. The claim is that we want to support “ergonomic dependent types”, and yet the proposed design falls short of this claim. We will not have ergonomic dependently-typed programming until we are able to use term-level functions at the type level, and yet this is not part of the stated goals. The proposed design includes the notion of a “Static Subset”, which is not ergonomic in my opinion.

I agree that there is tension between "ergonomic" and the Static Subset. But I do not think these are in direct conflict, precisely because the Static Subset need not be a strict subset. Once the Static Subset includes the entire language -- including reduction of functions in types -- then we will have full dependent types. The wiki page does not outlaw this state of affairs; it simply does not require it. This is a key part of the design in the wiki page: it's a design we can build today and then grow bit by bit until we really do have good dependent types.

> 
> 2. The proposal is inherently ‘mutable’: it refers to GHC Wiki when it clarifies what is meant by “ergonomic dependent types”, but the Wiki can be modified without GHC Steering Committee’s involvement. In fact, it’s part of the plan to refine the design over time! For example, it is still unclear (to me) whether we want `foreach` quantification or `Relevant` constraints. There must be an immutable component included in the proposal itself, one on which we will all agree, and then any change to it will have to go through the proposal process again. Otherwise, it seems like we are basically adding an (unintentional) loophole.

While you're technically accurate here, I'm not worried about this possibility, as it would seem to require a degree of willful sleight of hand. Wiki pages have immutable histories, so we can always do archaeology if we need to. I think of the mutability here as a feature, not a bug: as we flesh out the design, we can update the wiki page. It's true that this capability could be abused, but I'd rather take that risk.

> 
> 3. The proposal does an insufficiently good job of describing our values and priorities. Sceptics worry that lots of code will break, or that GHC will become slower, or that error messages will regress, and so on. The proposal should make clear that it is part of the effort to avoid these potential problems, rather than march blindly towards a vaguely defined bright future.

I have added a list of common misconceptions to the wiki page. Might these address your concerns?

> 
> So, here are some corrections I’d like to see.
> 
> 1. Rename the proposal to something along the lines of “Support Ergonomic Dependent Types – Part I”. We will inevitably follow up with Part II about type-level functions, complete term/type unification, and such. I mean the things listed under the “The Glorious Future” section of the Wiki page. If we accept this proposal, we are not accepting everything that is claimed to be related to Dependent Haskell – we are setting our destination to a specific subset of dependently-typed features. I don’t care about the exact phrasing (could be something like “A Step Towards Ergonomic Dependent Types”, or “Foundation for Dependent Types in GHC”, or anything else). I do care that it’s made clear that this proposal is not the full story. 

I'm quite happy to drop "ergonomic", as that term is squishy and troublesome. But I actually do not think that this proposal needs a sequel, so I don't want to set it up to require one.

> 
> 2. Copy the key parts of the Wiki page into the Proposed Change Specification. The key parts are already identified there: Predictable Erasure Principle, Lexical Scoping Principle, Syntactic Unification Principle. These principles will hold in any design that we shall settle on. They represent a high-level description of what we’re trying to agree on. On the other hand, code examples and various details must stay on the Wiki page, and then get elaborated in individual feature proposals. So let’s add the essential bits to the proposal text, but not more than necessary (4-5 principles, each backed by a few sentences).

I see your point here, but I think that keeping this open and mutable is better. What do others think?

> 
> 3. The proposed change specification should explicitly state that dependent types do not become the one and only goal. We continue to care about compile times, error messages, backwards compatibility, type inference, and so on. I think the proponents of dependent types (including myself) have mistakenly assumed this to be obvious. Just writing this down will reassure a lot of people, or at least I hope so.

This is easy, and I certainly agree with the intent. I will do so shortly.

Thanks for this feedback!
Richard

> 
> Thanks!
> - Vlad
> 
>> On 9 Mar 2021, at 10:58, Joachim Breitner <mail at joachim-breitner.de> wrote:
>> 
>> Dear Committe,
>> 
>> Support ergonomic dependent types
>> has been proposed by Richard Eisenberg
>> https://github.com/ghc-proposals/ghc-proposals/pull/378
>> https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst
>> 
>> This is a meta-proposal, aimed at refining our criteria when evaluating
>> proposals, and wants us to confirm that we take compatibility with a
>> future world where Haskell gains more dependently typed features into
>> account, and welcome changes that we would likely reject if we did not
>> expect to move towards that future.
>> (My rephrasing, please have a look at least at “Motivation” and
>> “Proposed Change Specification”).
>> 
>> We might need more of a Moderator than a Shepherd here… I propose that
>> Simon PJ leads us to a decision here. I know that Simon has a strong
>> opinion on this already and might not be a “neutral moderator”. But
>> opinions are not a bad thing per se, and I think this questions
>> requires Chair-level involvement.
>> 
>> 
>> 
>> Please guide us to a conclusion as outlined in 
>> https://github.com/ghc-proposals/ghc-proposals#committee-process
>> 
>> Thanks,
>> Joachim
>> -- 
>> -- 
>> Joachim Breitner
>> mail at joachim-breitner.de
>> http://www.joachim-breitner.de/
>> 
>> 
>> _______________________________________________
>> ghc-steering-committee mailing list
>> ghc-steering-committee at haskell.org
>> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> 
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee