Amend 281 to use atype instead of ktype

[int-index]

The current grammar allows expressions like

g x = f (type Maybe Int)

Simon found it surprising during code review. It's better to require explicit parentheses:

g x = f (type (Maybe Int))

So I propose we amend the grammar to use atype instead of ktype. This also avoids a shift/reduce conflict in the parser, which is nice.

[simonpj]

I don't have a strongly held position myself -- but yes, I did fid it surprising.

[phadej]

can g x = f (type Maybe Int) be understood in any other way than g x = f (type (Maybe Int))? There are already outer parenthesis, and this change would require double parenthesis for any non-trivial usage, feels silly (and looks ugly):

explicitId (type (forall a. a -> a)) id -- instead of
explicitId (type forall a. a -> a) id

servantClient (type (ApiWith SomeArgument AndAnother)) -- instead of
servantClient (type ApiWith SomeArgument AndAnother)

EDIT: The only example in the proposal of non-atomic type is explicitly parenthesized

t = typeRepVis (type (Maybe String))

It's quite subtle to hide such visible grammar choice into just single example.

[int-index]

@phadej The end-goal is to write your examples as

explicitId (forall a. a -> a) id
servantClient (ApiWith SomeArgument AndAnother)

This is possible with part 2 of this proposal. You still have the choice to write out an explicit type, but if you're the sort of person to prefer an explicit type keyword when it's not necessary, perhaps you also the sort of person to prefer extra parentheses for clarity.

can g x = f (type Maybe Int) be understood in any other way than g x = f (type (Maybe Int))?

Yes, it can be understood as g x = f ((type Maybe) Int). Now imagine that instead of Int we had something that used punning, e.g. g x = f (type Maybe [Int]) — is [Int] written it type syntax or term syntax? Instead of answering, I suggest we outright reject.

[int-index]

this change would require double parenthesis for any non-trivial usage, feels silly (and looks ugly)

@phadej For what it's worth, this was my initial thinking when I put ktype there, so past me agrees with you. What changed my opinion is that two years later (i.e. now) I looked at the examples like fn (type Int -> [a]) and had to double check the specification if it was supposed to be fn ((type Int) -> [a]) or fn (type (Int -> [a])).

And then Simon had a similar question, which tipped the scales for me. So now I believe that we should support two styles

1. Explicit, with both type and parentheses: fn (type (Int -> [a])).
2. Concise, with neither type nor parentheses: fn (Int -> List a). This one requires you to avoid punning, so I changed [a] to List a.

[nomeata]

can g x = f (type Maybe Int) be understood in any other way than g x = f (type (Maybe Int))?

To me it reads as f ((type Maybe) Int). If Int is in both name spaces, the two things mean different things, don’t they?

Maybe once I am trained to read type as a keyword I might parse it as f (type (Maybe Int)), but until then the usual juxtaposition-is-left-associative intuition will lead me astray, so I understand the desire to add parentheses here.

[phadej]

@nomeata type is a keyword. You cannot have (any) binder named type:

Prelude> let type = foo

<interactive>:1:5: error: parse error on input ‘type’

I see type not much different than case or \, or forall in that perspective, with BlockArguments you really should be able to say

id type Int

It's weird at first, but I think it is consistent: everything after a keyword is part of the "type".

Even things like id type Int :: Type.

($$) :: (forall (a :: Type) -> f a) -> forall (b :: Type) -> f b
f $$ type x = f type x

Would original proposal require to write f $$ (type x)?

[nomeata]

As a variant of your last example, what happens to

type a `foo` b = …

So here type scopes over a, foo and b, but not the RHS, under the keyword regime, but only over a indeed the like-function-application regime (ignoring the possible confusion with type alias declaration)?

I see good points for both variants. Tricky.

[int-index]

Would original proposal require to write f $$ (type x)?

Yes, it's a different problem. We have

        exp ::=
          | 'type' ktype
          | ...

rather than

        fexp ::=
          | 'type' ktype
          | ...

You could contemplate the consequences of adding the type production to aexp, fexp, infixexp, or exp. Unfortunately, if you actually try to do that, you'll get reduce/reduce conflicts. The reason is that we allow naked TH splices at the top level

makeLenses ''MyT

We parse it as infixexp. But we also have type synonyms

type T a b = ...

So now imagine we extend infixexp with type. This means we'd parse the following as a naked TH splice:

type T a b

Suddenly the left-hand side of a type synonym looks like a naked TH splice, and that's hugely problematic.

It's somewhat unsatisfactory to be constrained by the implementation here, and if someone is particularly motivated, perhaps they could find a way to work around this. But we don't have to do it now.

To sum up, there are two design questions here

1. What do we expect to the right of type?
   • 'type' atype
   • 'type' btype
   • 'type' ctype
   • 'type' ktype
   • (some other option)
2. Where do we put the type production?
   • aexp
   • fexp
   • infixexp
   • exp
   • (some other option)

In its current form, the proposal is ambitious on the first point (using ktype) but conservative on the second (using the exp). The amendment makes the proposal conservative on both accounts. You seem to want to make it ambitious on both accounts to minimize parentheses. There are two reasons not to do it

• Difficult to implement (due to conflict with naked TH splices).
• Not immediately intuitive (data points: Simon, Joachim, and I). You also seem to agree that it's "weird at first".

And I will also admit that it's not a very important issue to me, as I do not plan to use the type keyword all that much. My personal preference and recommendation is to lean heavily on part 2 of the proposal and simply omit type where possible. You still have it when you need it, but if it's used rarely/sparingly, then extra parentheses are a good thing! If you see something rarely, you're probably not entirely used to the syntax, so the parentheses are as important to the person reading the code as they are to the compiler.

[int-index]

So here type scopes over a, foo and b, but not the RHS, under the keyword regime, but only over a indeed the like-function-application regime (ignoring the possible confusion with type alias declaration)?

@nomeata Excellent example, and I find that your summary "tricky" is also a point in favor of simply requiring parentheses. We could spend a lot of time discussing this and trying to find the best option, then even more time trying to implement it, only to condemn our users to read code like this and say "tricky".

ignoring the possible confusion with type alias declaration

And let's not ignore this. It's a legitimate implementation concern. Our parser is LALR, conflicts like this are a burden.

[tomjaguarpaw]

If we choose the option of requiring parentheses now does it allow us to defer a possible choice of precedence until later?

[int-index]

If we choose the option of requiring parentheses now does it allow us to defer a possible choice of precedence until later?

Yes, I think so.

One thing to keep in mind is that when faced with type A -> B, we should parse it neither as (type A) -> B nor as type (A -> B). This doesn't immediately follow from the grammar in the proposal. The precedence of -> relative to type is somewhat underspecified, as section 7.1 plays fast and loose with the nonterminals, using "exp" to mean "expression" but not any particular expression nonterminal.

It's a corner case, but I'm aware of it and will account for it in the implementation.

[phadej]

@int-index It looks like I don't understand what type in expressions is meant to do.

For example with non-visible type application:

@(Int)

on the top level doesn't make sense.

Similarly,

type Int

as visible type-application on top-level shouldn't make any sense. The only way to interpret type keyword on type-level is as type alias definition statement.

---

Continuing with non-visible type application:

The only place where it makes sense is when parsing applications, i.e.

foo @SomeType

As far as I can understand, the new usage of type keyword should only be possible there

foo (type SomeType)

and there the (type ...) is always parenthesised.

Thus I don't even understand what foo ((type A) -> B) could mean.

---

The 281 proposal is about visible type application. I could understand the problems if goal was to allow embedding types into terms anyhere, and having type as a keyword to mark the switch, but 281 is not about that - it's only about type applications. The part of name resolution can be understood as accidental. I argue that without further clarification, it should be restricted to only the application positions, so you can write

foo $$ type Bar

but not

type Bar `someThing` foo

as it can be undestood as type (Bar someThing` foo).

However if we want to allow embedding types everywhere (for some later needs), that IMHO should be proposed separately, if nothing else, than to allow better reference.

The proposal 281 does it somewhat sneakily. IMO some new special token (for sake of example foo @@Bar) could been proposed.

However it does say:

A type embedded into a term with the type marker follows type-level name resolution rules (i.e. uses of punned identifiers resolve to the type namespace), both at binding sites and at use sites.

It can be understood as "switching to as far left as parenthesizing allows" (like forall or \).

[phadej]

And a separate question, will it be allowed to write

foo @(type Int)

Why or why not? 281 doesn't have an example AFAICS.

[phadej]

Somewhat unrelated, why BlockArguments allow to write foo \x -> x,but not Maybe forall a. a.

And it the latter were allowed, would in part 2 not only foo Int but also foo forall a. a be possible?

(EDIT: IMHO nothing of that should work, and BlockArguments was a mistake to accept&implement).

[int-index]

I could understand the problems if goal was to allow embedding types into terms anyhere, and having type as a keyword to mark the switch, but 281 is not about that - it's only about type applications.

@phadej The type keyword is a namespace/syntax disambiguation mechanism. Say we start with this

f :: forall a -> ...

x = f Int

This is a valid call to f that instantiates type variable a to Int. Now imagine I define a conflicting name

data MyType = Int | Bool | Char   -- data constructors!

Now the Int in f Int will refer to the data constructor Int, which may not be what I want. So I have to write f (type Int) instead. This namespace disambiguation doesn't need to happen at the outer level of a function application, for example I could have

y = f (Either (type Int) (type Bool))

That's completely different from @, which acts at the outer level of a function application to override visibility, i.e. turn an invisible type argument (one that should've been inferred by the compiler) into a visible one (one explicitly specified by the user).

You are correct in your observation that type Int is not valid at the top level, so it's illegal to write this:

top = type Int   -- bad

But this is the same problem as this:

top = Int   -- also bad

Visible forall can function perfectly fine without type; however, type is only useful in conjunction with visible forall. The initial version of the proposal didn't even contain type, and I personally do not intend to use it ‒ I'd rather avoid punned identifiers. Someone convinced me to add type to the proposal and structure the specification around it, but for me it was a compromise.

[phadej]

@int-index

None of what you wrote prevents making type extend the switch of namespace to as far right as parenthesizing allows.

[int-index]

None of what you wrote prevents making type extend the switch of namespace to as far left as parenthesizing allows.

By "left" you probably mean "right", and yes, I did not touch on that because I was answering this part of your message:

Thus I don't even understand what foo ((type A) -> B) could mean.

I hope it is clear now that type (A -> B) and (type A) -> B differ in what namespace is used to look up B.

The way we parse this example is an arbitrary decision, my idea is to require explicit parenthesization as a conservative solution that avoids committing to any precedence.

[phadej]

I hope it is clear now that type (A -> B) and (type A) -> B differ in what namespace is used to look up B.

Partly. (->) is bad example as far as I know -> cannot appear in terms. Will the future parser recognise -> in terms too?

Currently it doesn't:

GHCi, version 9.6.2: https://www.haskell.org/ghc/  :? for help
Prelude> 'x' -> 'y'

<interactive>:1:5: error: [GHC-58481] parse error on input ‘->’

[int-index]

Will the future parser recognise -> in terms too?

Yes. Section "7.1 Syntax" introduces the so-called "types in terms", including the function arrow.

[phadej]

For reference, here's this PR version of 281: https://github.com/ghc-proposals/ghc-proposals/blob/cc6fe47e00b6106f11add1ed5f98b8e0be795195/proposals/0281-visible-forall.rst

Properly reading it makes me more convinced that having 281 add forall ... -> and types-in-terms as small part was bad mistake. The latter should been proposed (and implemented) separately (even there are no real use case without visible forall).

Types-in-terms is conceptually a lot bigger change than forall ... ->, and that got unnoticed by me, as I didn't think that forall ... -> proposal has anything that interesting in it.

[Ericson2314]

Being able to use type namespace-bound identifiers but not types violates equational reasoning. IMO the proposal was right to propose both at once.

[int-index]

The latter should been proposed (and implemented) separately (even there are no real use case without visible forall).

The accepted proposal #378 introduces the Syntactic Unification Principle (SUP), it is well established by now that we want to support type-level syntax in terms and vice versa. So there is no question whether to have types-in-terms, the question is where, when, and how to specify them. In my opinion, #281 was a perfectly fine place to do that, as types-in-terms are useful in conjunction with visible forall.

and that got unnoticed by me.

No problem, you noticed it now. Is there something about this part of the proposal that you'd like to change? It's not too late to tweak the specification. My plan is to do implementation for GHC 9.10, we have plenty of time to discuss the finer points and propose small amendments like this one.

[phadej]

No problem, you noticed it now.

This is not helpful comment.

Is there something about this part of the proposal that you'd like to change?

It's not about that. This proposal process was meant to bring visibility to what changes are happening in GHC. This instance is a partial failure as far as I can say.

But at the very least, amend the title to include types-as-terms. As I said, I see that as a lot bigger concrete language change than adding forall ... ->

And please don't refer to proposals by just their numbers (like in the title of this one).

[nomeata]

But at the very least, amend the title to include types-as-terms. As I said, I see that as a lot bigger concrete language change than adding forall ... ->

I sympathize with this, proposal #281 has much more fundamental content than ”just” a new type binder, and thus I keep forgetting where types-in-terms has been introduced. But it does makes sense that it's in the first proposal that allows to make use of them, and was already mandated in a way by the overall plan for dependend types in #378.

Anyone opposed of we add “and types in terms” to the title of #281 (text and PR), to make hovering the PR number more useful? It certainly would help me!

[int-index]

Anyone opposed of we add “and types in terms”

@nomeata We need to find a better way to phrase this, as "Visible forall in types of terms and types in terms" is grammatically ambiguous. Is it "Visible forall in [types of terms and types in terms]" or "[Visible forall in types of terms] and [types in terms]"? We want the second interpretation to be clear. Maybe use a semicolon? Though it's not much better. I don't know.

[tomjaguarpaw]

"Visible forall in types of terms, and types in terms"?

[int-index]

Serial comma, classic. Yeah, I'm not opposed to that.

[nomeata]

Done

[int-index]

Glad to see this issue resolved. Can we now return to the topic of atype vs ktype? I lost track of where we are at. @phadej, what's your stance on this after I explained how (type A) -> B and type (A -> B) are both possible?

[phadej]

@int-index

My stance that I'd rather treat type as a context switch extending as far right as possible, instead of current unspecified fixity prefix operator. (EDIT: I guess extending as far right as possible is still a prefix operator behavior, but with specified fixity, binding looser than anything else)

[JakobBruenker]

Worth noting that if we treat type as extending as far to the right as possible, we lose the symmetry of how type is handled in patterns vs in expressions

[int-index]

Worth noting that if we treat type as extending as far to the right as possible, we lose the symmetry of how type is handled in patterns vs in expressions

I'm not sure I understand. Expressions and patterns use the same grammar — we probably couldn't lose symmetry if we tried to. In fact, extending as far to the right as possible is achieved simply by using ktype, i.e. that's the design of the current proposal. This amendment tries to limit this behavior so that type only extends to cover a single atomic type.

[JakobBruenker]

Ah, no, for some reason I was interpreting "as far to the right as possible" as essentially "to the end of the line", i.e. I was ignoring the "as possible" part

[int-index]

@nomeata Let's submit this to the committee.

[goldfirere]

This proposal has now been accepted. Thanks, all!