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

[Vladislav Zavialov (int-index)]

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.

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.

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.

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. 

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).

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.

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