[ghc-steering-committee] Status

[Richard Eisenberg]

> On Mar 10, 2021, at 12:04 PM, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:
> 
>  Yes, we want to consider a cohesive language design, but this doesn't mean that everything has to depend on everything.  The nice benefit of the extension system is that it allows us to experiment with language changes modularly.  As I see it, here we have a choice between:
>    A. a modular opt-int design that is close to what is already used by a lot of a projects (i.e., something like `sizeOf @Bool`), and
>    B. an alternative design (i..e, `sizeOf Bool`) that depends on an unrelated feature (dependent types), that we have zero experience with, and require major changes to how something as basic as name resolution works.
> 
> It sounds like #378 is asking us to always make choice B.

Ideally, we wouldn't have to choose between these. In other proposals, we have worked hard to find a design that meets both your A and B. (These are essentially the same as the (1) and (2) from https://github.com/goldfirere/ghc-proposals/blob/dependent-types/proposals/0000-dependent-type-design.rst#motivation-for-why-we-need-this-proposal -- glad we agree on this starting point.) The problem is that we don't seem to have a design for #281 that satisfies both A and B. Proposal #378 essentially says that, when considering the Haskell language and how a new feature fits in, we consider the language sketched in https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell, in addition to all the features in today's Haskell.

>    I think a better plan is to prefer option A, as we have been for a long time now.  I don't think that precludes the work on dependent types in any way (ergonomic or not, whatever that means).

I disagree here. A critical part of the design for dependent types is the Syntactic Unification Principle from the wiki page:

> Syntactic Unification Principle (SUP). In the absence of punning, there is no difference between type-syntax and term-syntax.

The idea here is that programmers should not have to worry about whether a piece of syntax is a type or a term. Indeed, my hope is that programmers simply stop making this distinction, as I don't think it is a helpful one -- indeed, I've discovered I don't even really know what that distinction means in a dependently-typed language. (A difference between *compile-time* information and *runtime* information is critical and an important pillar of the design of dependent types.)

Requiring a programmer to put an @ before some arguments but not others would be very strange in such a world. It violates the SUP.

>   Once that work is done, it might subsume some existing extensions, and folks would have a choice to write things one way or another depending on their needs.  I expect in the long run, one of the designs might become the common way to do stuff, and eventually we might depreciate some of the extensions that are not used any more.     To me, this seems to be the right way to grow a living language like Haskell. 

This is a plausible way forward, yes. But it will require a breaking change to the language, one we can avoid with a little forward planning now.
> 
>  As I mentioned before, I find `sizeOf @Bool` more readable than `sizeOf Bool` exactly because I don't need to keep in my head yet another thing (i.e., which `Bool` are we talking about here).

Yes -- exactly! I also don't want to keep another thing in my head: whether the argument to sizeOf is in term-syntax or type-syntax.

>   By the way, in case the `Bool` example seems absurd, using `newtype`s is quite common when doing FFI bindings, and the normal pattern there is to use the same name for the value and type constructor, so this is something that we should not gloss over lightly.

This is a good point. There are several ways forward:

* Users can always use `sizeOf (type Bool)` if they want to. This is documented in https://github.com/int-index/ghc-proposals/blob/visible-forall/proposals/0000-visible-forall.rst#43secondary-change-type-herald

* Nothing stops us from having sizeOf :: forall a. KnownSize a => Int; this would still work with sizeOf @Bool. We could have both sizeOf :: forall a -> KnownSize a => Int (which uses sizeOf Bool) and the other one, perhaps exported from different modules, and then users can choose which one they prefer.

* Users can make a type-level module alias using the syntax in #270. This would allow sizeOf T.Bool.

* Users can avoid punning by changing the names of their constructors.

These choices are all (except the last one) entirely local. Note that nothing anywhere here requires a change from the status quo, which is today's sizeOf.

Richard