Not so much a comment as a lament:
what has become of the Haskell I knew and loved, that forall k -> k -> * is even a thing? In

data T k (a :: k)

I see two type parameters that are not the same, albeit they are related. So T's kind must also have two parameters. Why isn't the kind (with explicit foralls) forall k1 k2. k1 -> (k2 :: k1) -> * ?

Also BTW, what can I put as a data constructor on RHS of that data decl? The only thing I can get to work is

data T k (a :: k) where
  MkT ::  Type -> (a :: Type) -> T Type a

You kindaholics keep telling me that with TypeInType, type :: kind is just like term :: type programming. I'm not seeing it.

Why aren't there two kind parameters for the kind of T? Then we'd be able to forall them with a conventional .(?)

@AntC2 suggests that the declaration data T k (a :: k) should mean that T :: forall k1 k2. k1 -> (k2 :: k1) -> Type. I disagree here: that kind says that T first visible parameter has kind k1 -- whereas I mean for the first visible parameter to be k1. I mean for the first visible parameter to have kind Type. In addition, your kind means that the second parameter should have kind k2 (which, in turn, would have kind k1) -- but this also isn't what the declaration for T means.

And, while I'd like type :: kind to be just like term :: type eventually, I fully agree we're not there yet. This is one place where type :: kind is ahead of term :: type.

Thanks @goldfirere, let's take a step back. For that declaration of T:

• How many visible parameters should T's kind have? (I think 2.)
• Are they necessarily the same kind? (I think not.)

The distinction you draw above between having kind k1 vs. being k1 is eluding me. I'd expect you to say ... be Type (or be Constraint or be some concrete kind starting upper case). I think Haskell's type/kind algebra doesn't have the capability of expressing 'has' vs. 'be'. And I'm not seeing that forall k -> ... is drawing that distinction. (Is this some new form of quantification/binding never anticipated by Frege or Russell or Church?)

Why not T :: forall k. Type -> k -> Type? I suppose you're going to say that doesn't display the type/kind dependency. T :: forall k1 k2. (k1 ~ Type) => k1 -> (k2 :: k1) -> Type ? (Seems to be illegal.)

In data T k (a :: k): parameter k denotes a type-as-kind; parameter a denotes a type-as-type. So we lift that to the kind for T: the first parameter denotes a kind-for-a-kind; the second parameter denotes a kind-for-a-type.

?

Perhaps another way of phrasing @AntC2's question is: are the following two forms equivalent? (And moreover, will GHC parse both forms under this proposal?)

• forall k -> k -> Type
• forall (k :: Type) -> k -> Type

I would intuitively expect them to be the same, since dependently typed languages like Idris use a similar syntax (in Idris, it would be (k : Type) -> k -> Type).

I'm in favour of the original proposal.

@RyanGlScott the tv_bndrs grammar production includes both forms, so yes, they will both be parsed (perhaps the proposal should say this explicitly). They are equivalent after kind inference (i.e. forall k -> k -> Type is essentially syntactic sugar for forall (k :: _) -> k -> Type, and kind inference fills in the _ with Type).

I suspect some of the confusion stems from the fact that in "traditional" Haskell, the forall a . s vs x -> t distinction includes several different aspects that are only "accidentally" aligned (see Hasochism). When giving the type of a term:

• invisible vs. visible: at use sites, an argument standing for a cannot be written (without TypeApplications), but an argument of type x must be written explicitly;
• dependent vs. non-dependent: a can occur in s, but the argument of type x cannot occur in t (it does not even have a bound name);
• implicit kind vs. explicit type: the kind of a is inferred (although it can be written explicitly as forall (a :: Type) . s, given KindSignatures), whereas x is the type in the second case;
• syntactic category of types vs. syntactic category of terms: an argument standing for a must be drawn from the grammar of types, but an argument of type x must be drawn from the grammar of terms;
• parametric vs. non-parametric: the choice of argument standing for a cannot affect the result of evaluation (because it is erased at runtime), but the choice of argument of type x is available at runtime.

When giving the kind of a type:

• the first three aspects remain essentially the same;
• both forms quantify over the syntactic category of types;
• the parametricity/erasure story becomes more complicated (let's not get into that now).

The point of this proposal is to start teasing these distinctions apart, so we can use "visible" quantification in kinds while leaving everything else alone. I hope that one day we'll gain access to this in the types of terms as well. 😉

Thanks @RyanGlScott for trying to help. My question is really: what's happened to the . after forall to demarcate what are the bound vars and what is their scope? With . in a type signature, I can happily put parens round the scope it binds :: forall k (a :: k). (k -> a -> *) How do I read the forall quantifier with ->? Is it forall (k -> k -> *) or (forall k) -> k -> * or (forall k -> k) -> * or forall (k -> k) -> *? Might there be a kind forall k1 -> forall k2 -> k1 -> k2 -> *?

If your two forms are parsed and equivalent (thanks @adamgundry), and/or @goldfirere's distinction about having vs. being, then how about these?:

• forall (k :: Type) -> (k :: Type) -> Type
• forall (k :: Type) -> (k :: k) -> Type -- k _is_ Type, allegedly
• forall (k ~ Type) -> (k :: k) -> Type

@AntC2, let's perhaps approach understanding the new form by relating it to something that's existed in Haskell from the beginning, polymorphism. Witness

id :: a -> a
id x = x

With this definition, we can say id True or id 3 without problems.

Now, let's add TypeApplications.

id :: forall a. a -> a     -- actually, we don't need the "forall" yet, but it's perhaps more perspicuous to
id x = x

If I use visible type applications, then I can say id @Bool True and id @Int 3. Note that the two parameters passed to id have different types, even though both parameters are written a in the type signature. The first parameter is a (which has kind Type), while the second parameter has type a.

The only difference between forall a. and forall a -> is that the latter means that the argument is required to be passed. In the former, the argument is often omitted, unless the user uses visible type application. Though this proposal does not propose visible, dependent quantification in types (really, the only reason it doesn't is because the parser would be at an utter loss to distinguish types from terms), here is what it would look like:

id :: forall a -> a -> a
id _ x = x

Now, calls would look like id Bool True and id Int 3. Note that there is no @, because the @ can be seen as a mechanism to provide an invisible argument visibly -- not necessarily as a "the next argument is a type" operator. (Thanks, @adamgundry, for mentioning the Hasochism paper, which lucidly describes how Haskell has conflated many independent notions.)

Returning back to this proposal, our data T k (a :: k) has kind forall k -> k -> Type. Here, T has two visible arguments; the first has kind Type while the second has kind k. This is just like how in id's type, the first parameter has kind Type while the second has kind a -- even though both parameters are written just with a. It would perhaps be more telling to say T :: forall (k :: Type) -> k -> Type -- except that the :: Type annotation is unnecessary.

Other points raised above:

• Yes, @RyanGlScott's two forms have the same meaning.

• This is not a new form of binding, but one that would be present in any dependently-typed, fully-explicit language.

• I'm not sure what the distinction between "type-as-kind" is vs "type-as-type". Since GHC 8.0, kinds and types are simply the same thing.

• As for the parentheses, I suppose the best I can do is forall (k) -> k -> Type. None of the other parenthesizations work out.

• Yes, forall k1 -> forall k2 -> k1 -> k2 -> Type is fine. It means the same as forall k1 k2 -> k1 -> k2 -> Type and would classify data S k1 k2 (a :: k1) (b :: k2).

• Any type mentioning (k :: k) is wrong, as no type variable can mention itself in its own kind. (Though others have thought that this kind of thing might be sensible. They're called very dependent types.)

I hope this all helps!

Those people who stand high enough on shoulder’s to see into the Dependent Haskell future: Does this proposed syntax line up for eventual visible dependent parameters that are not kinds?
I.e., will we eventually have repeatV :: forall x. forall (n :: Nat) -> x -> Vec n x?

@nomeata that specific example would need a relevant binder: pi (n :: Nat) ->. But yes that syntax is still valid and correct for other use-cases.

So basically forall x → is equivalent to pi (x :: _) →? Then why not use the latter syntax already, if this is where, in fact, we do have (some form of) pi types in GHC already?

@nomeata visibility and parametricity/relevancy are orthogonal. forall x . pi x . forall x -> pi x -> are all valid, and proposed, in @goldfirere's thesis.

Thank you @goldfirere for that explanation via polymorphism and visible TypeApplication. That lifeline has helped a lot. I hope the line is well secured at your end, I'm going to pull hard ;-).

I should have said at the outset: I'm +1 that if there's a kind GHC infers, but you can't declare in source, that is "just plain silly". So we need a new bikeshed; the only question is the colour.

Like @nomeata, I'm wondering if we need to anticipate how the signatures are going to look for dependent types?

Is this binding like a big-pi or big-lambda (as you might use for polymorphism)? I notice they both still use the ..

What's the inferred kind with forall under this proposal for:

data T2 b k (a :: k)

And in what order do I supply the kind/type parameters? What if I want to use visible TypeApplication to give a kind for b?

• By type-as-kind I mean: yes it's now all just types; OTOH some types can legitimately appear in a type signature to the right of ::, others can't. And you [Richard] give the game away by representing them with k rather than a, b.

• Why is k:: k wrong? In this case you've told me k is Type. So k :: k is Type :: Type, which is TypeInType(?) If not, what is the kind of Type?

I am +1 on this proposal. For those interested in where this fits on the road to dependent haskell, it's only necessary to read chapter 4 of Richard's thesis, which is extremely approachable even for a lay person like myself. The chapter concludes with this table (I've removed the matchable quantifiers since they aren't relevant to this discussion):

To address @nomeata's question a little more, forall and pi differ in relevance, and so they should not be collapsed into a single construct.

Thanks, @andrewthad, for posting that table. I hope that resolves many of the questions above.

As for @AntC2's example: if we have data T2 b k (a :: k), then we have T2 :: forall {k2 :: Type}. k2 -> forall k -> k -> Type. Note that a and b never get mentioned, because neither variable is quantified dependently (neither is used to classify an argument later in T2's kind). The k2 variable is inferred by the type-checker. According to the design of visible type application, variables inferred by the type-checker and never mentioned in the source are not available for type application. There is thus no way to use type applications to choose the value for b's kind.

As another specific answer to a specific question: k :: k is no good because the scoping rules for type variables say that a type variable cannot appear in its own kind. This does not conflict at all with Type :: Type, as Type isn't a type variable. It's true that if k ~ Type, then k :: k would make some sense, but k is not Type in the examples in play.

I hope that resolves many of the questions above.

It's adding to the confusion. Is this a proposal to tweak a bit of syntax for a kind GHC already infers? Or is this a proposal to adopt the whole of the syntax in @goldfirere's thesis? (I'm not saying that's a bad thing, but let's get straight what we're discussing.)

There's already proposals (currently in abeyance) for the matchable vs unmatchable arrows.

Had we better make sure this also integrates with whatever is the syntax for linear types (another under-the-radar proposal)? Do we have to support both matchable and unmatchable lollipops for both dependent and non-dependent types/kinds that are either relevant or irrelevant and/or in/visible? forall k ~⊸ .... (That's a wiggly lollipop, in case your browser murders it.)

we have T2 :: forall {k2 :: Type}. k2 -> ...

Uh-oh. Curly braces. Is that some innovation I missed?

I'm -1 on this proposed syntax. When I see forall I want to see a .. I propose using a different binder keyword -- especially since big-pi seems to be in the wings. Isn't this visible kind doing the same as big-lambda Λ t. t -> ... at the polymorphic type level?

I think we should have syntax to write down kinds like this.

As to concrete syntax I'm fairly relaxed. Options on the table appear to be

• forall k -> blah
• pi k. blah

Any others? The nice thing about forall k -> blah is that I'm used to treating forall as introducing a binder, and -> as introducing something I have to write as an explicit argument. pi has neither of those cues.

Richard's thesis suggests that one day all of these would be valid:

Data Type Declarations
(a) data Foo :: forall k. k -> Type where ...
(b) data Foo :: forall k -> k -> Type where ...
(c) data Foo :: pi k. k -> Type where ...
(d) data Foo :: pi k -> k -> Type where ...

Function Type Signatures
(e) bar :: forall k. k -> Type
(f) bar :: forall k -> k -> Type
(g) bar :: pi k. k -> Type
(h) bar :: pi k -> k -> Type

Currently, only (a) and (e) are accepted by GHC. Although all of them are on the path to full dependent types, the proposal being discussed here only suggests allowing (b). So, to answer @simonpj, I don't think we should use pi x. for this because the long-term plan is for that to be the relevant invisible quantifier.

It's adding to the confusion.

Is this a proposal to tweak a bit of syntax for a kind GHC already infers?

Yes

Or is this a proposal to adopt the whole of the syntax in @goldfirere's thesis?

No

The title is "visible dependent quantification". That exactly corresponds to one row, but just one row, of the table, as @andrewthad points out.

There's already proposals (currently in abeyance) for the matchable vs unmatchable arrows.

Matchability is yet another axis of variation, and one unmentioned in this proposal. It's not relevant here.

Had we better make sure this also integrates with whatever is the syntax for linear types

Squigly and lollipop indeed don't get along well, but matchability and squigly are immaterial to this proposal. The arrow in forall _ -> can undergo the same variations as the plain arrow. Conversely, . already lacks potential alternatives, but also already is in use in forall _.; therefore this proposal neither needs new solutions or introduces new problems as far as other potential quantifiers are concerned.

Uh-oh. Curly braces. Is that some innovation I missed?

That's just indicating that the quantification is inferred. Not sure if it's just informal syntax or something ghci might already print out.

I propose using a different binder keyword -- especially since big-pi seems to be in the wings. Isn't this visible kind doing the same as big-lambda Λ t. t -> ... at the polymorphic type level?

Π would be the unicode syntax for pi (Upper-case being what's used in the literature; keywords being conventionally lower case in Haskell). I haven't seen anyone propose (here or elsewhere) the distinct use of Π/π like Λ/λ in System F.

Isn't this visible kind doing the same as big-lambda Λ t. t -> ... at the polymorphic type level?

Yes in that all quantification in System-F is visible, and ∀-quantification (introduced by Λ) is irrelevant.

@andrewthad and @Ericson2314 very much have the right idea. Thanks for your posts. Let me add my own small points to theirs:

• Yes, this proposal is about only adding one line of that table to GHC. Given that some have wondered about future compatibility with more dependent types, looking at that table may be helpful as a way to discover what will eventually be proposed. But we're not there yet!

• The curly braces are part of the syntax that -fprint-explicit-foralls can print. They are not currently accepted as input. See the manual (second-to-last bullet).

• Pi-abstraction, forall-abstraction, and lambda-abstraction are all different and are all useful. One is not an abbreviation or alternate spelling of another. One is not a degenerate case of another. Every dependently typed language I know of has all of them (in various guises). Since the advent of kind-polymorphism, GHC has actually supported all of them as well, but it didn't know it. (The kind of kind-polymorphic datatypes and type families are really Pi-quantified, not forall-quantified, but this proposal doesn't address this historical inaccuracy.)

• The curly braces are part of the syntax that -fprint-explicit-foralls can print. They are not currently accepted as input.

Then should that syntax be accepted? Can we tack it on to this proposal; and with the same motivation:

The syntax ... that is printed in GHCi ... is not currently parsed.
... This is just plain silly.

• Pi-abstraction, forall-abstraction, and lambda-abstraction ... Every dependently typed language I know of has all of them (in various guises).

Then what varieties of syntax constructs do those languages use to express them? Do they use both forall _ . ... and forall _ -> ...?

If kind-polymorphic datatypes are "really Pi-quantified, not forall-quantified", why isn't this proposal for Pi-quantified? There's no historical inaccuracy (yet), because forall _ -> ... isn't currently parsed.

I kinda suspect the answer is going to be: because that's not what's in @goldfirere's thesis. Then the claim that this proposal is about "just one row, of the table" is bogus. If this syntax gets accepted for dependent kinds, it'll be fait accompli for function type signatures.

What worries me is not providing a succinct syntax to suit yous brain-the-size-of-a-planet dependent type-acrobats; but the newbie who makes a typo (for example missing out a . after a forall) and gets an avalanche of impenetrable errors suggesting they intended DependentTypes/TypeInType/PolyKinds. This first is too easily mistyped as the second:

f :: forall a b c. a -> b -> c
f :: forall a b c -> b -> c         -- GHC currently reports "parse error on input ‘->’"

succinct syntax to suit yous brain-the-size-of-a-planet dependent type-acrobats

There's no need for backhanded compliments.

To address one of your concerns, the error messages would actually be better if GHC admitted the dependent irrelevant visible quantifier. Here's a more simple version of the example you gave:

{-# LANGUAGE RankNTypes #-}
foo :: forall a. a -> a

In GHC 8.2, the error we get is:

bad.hs:5:17: error: parse error on input ‘->’
  |
5 | foo :: forall a -> a -> a
  |                 ^^

The parser simple cannot handle this. But, if the parser could recognize it, then the error could come from a later stage (possibly the type checker although I'm really fuzzy on where this would actually happen). We could then have an error like this:

bad.hs:5:17: error: type used as function argument
  |
5 | foo :: forall a -> a -> a
  |        ^^^^^^^^
This type signature suggests that the function takes a type as an argument.
Perhaps you meant:

    foo :: forall a. a -> a

Alternatively, you may enable DependentHaskell to allow this behavior.

The error message can actually provide instruction on how to fix the problem, which it doesn't currently do.

Then what varieties of syntax constructs do those languages use to express them? Do they use both forall _ . ... and forall _ -> ...?

To make the visible/invisible distinction, agda uses curly braces. It uses the function arrow regardless of whether the type variable is visible. Idris is similar is that it always uses an arrow and uses curly braces to handle visibility. For example:

Agda
foo :: ∀ x y -> x -> y -> y   -- visible
foo :: ∀ {x y} -> x -> y -> y   -- invisible

Idris
foo :: (x : Type) -> (y : Type) -> x -> y -> y
foo :: {x, y} -> x -> y -> y   -- invisible

Dependent Haskell
foo :: forall x y -> x -> y -> y   -- visible
foo :: forall x y. x -> y -> y   -- invisible

To be more like other dependently typed language, haskell could use curly braces to make type variables invisible. But, that would be strange since we already have syntax for doing this. Richard's thesis takes this into account, preserving our existing syntax for invisible type variable while introducing a new syntax for visible type variables that (a) does not break any currently compiling code and (b) is very consistent with the way other languages handle this. That's why I'm in favor of this syntax.

@AntC2

but the newbie who makes a typo...

There's a really easy solution: just make a beginner mode that doesn't mention non-whitelisted extensions. As @andrewthad mentions, being able to parse this will still help the error message: in this mode, it can simply be "please replace forall <stuff> -> with forall <stuff> ." (along with the usual line quoting).

(Off topic) I really find these education-vs-advanced-users debates extremely unproductive. Obviously there's no way to have a single language that suits everyone's needs! But, there's no reason GHC can't simultaneously implement all the langauges needed to cover that (such that they can import one another). The Racket people, who have actually studied CS education empirically, have been doing this for years.

The curly-brace syntax indeed should be accepted. And a collaborator of mine should be posting a proposal to that effect in short order. I don't think the change belongs here.

There already is historical inaccuracy. I can say data Proxy :: forall k. k -> Type. But that should really be pi. This proposal is orthogonal. The appearance of pi (instead of forall) in datatype kinds is in my thesis, although I don't believe it's addressed in the text.

Conversation seems to have died down here. I believe this proposal is ready to submit to the committee, @nomeata.

The long conversation above did not result in any changes to the proposal. It is essentially a Q&A session... but as every reader will have their own questions, I don't think any of it needs to be put in the proposal itself. A committee member may choose to skim through the commentary to see if a question they have is addressed. In particular, I want to publicly express my gratitude to @adamgundry, @andrewthad, and @Ericson2314 for helping to explain aspects of this proposal -- I fully agree with all of their statements above.

Template Haskell will have to be updated, and we'll have to make sure no terms can get these strange new types.

Surely there isn't a fundamental reason why terms couldn't have visible dependent quantification? Is this just to limit the scope of the proposal?

if we eventually end up with real dependent types, then that construct would be out of place

I shall refer you to the second paragraph of your own comment #81 (comment), where you ask to consider this proposal in isolation 😃

When we consider -XDependentHaskell, a lot of other constructs would be out of place, and in more fundamental ways (for example, type families would compete with actual type-level functions).

I don't think it's impossible to merge the type and term parsers... just not a problem I want to fix in this proposal

I don't think that it's even a problem worth solving for the time being, even adding pi quantification would not, strictly speaking, require it.

There are several reasons I would like to incorporate (:: ty) into this proposal:

• this would eliminate an unnecessary special case for terms
• visible dependent quantification for terms is a feature useful today

In many APIs using forall a -> instead of forall a would mean that:

1. AllowAmbiguousTypes is no longer required to use the API
2. the need to specify the type is evident from the type signature
3. the users do not face mysterious errors when they forget to use type application because a proper error about a missing argument can be emitted

I am not sure, but perhaps this could also allow eta-reduction of type-abstracted terms?

foo, bar :: forall a. ty
bar = foo @a -- the `@a` is required

foo, bar :: forall  a -> ty
bar = foo -- eta-reduction of `forall`

@int-index You make good arguments, but you're suggesting a fundamental change to this proposal: the proposal as is discusses adding concrete syntax for an already-existing feature. You're describing a brand new feature (with plausible syntax). While I would find such a proposal interesting and perhaps compelling, I don't wish to tie the much more basic proposal here with this grand new idea.

Okay, but can you tell how much work adding this check implies?

This new construct will be rejected in any context that is unambiguously a type for a term. (For example, it will be rejected in type signatures of terms, but allowed in type synonyms, which can be used in kinds.) No term-level definition can have a type that has a visible dependent quantifier.

If it's a trivial check then it makes sense to postpone handling this case for later, in a separate proposal. If it'll require non-trivial changes to the compiler, it would be a shame to introduce them just to rip them off later (maybe in the same release, if I manage to get the (:: ty) proposal accepted and implement it).

The check (now more fully described) would be quite easy to implement. GHC already does what it calls "validity checking", and prohibiting forall -> syntax would fit right in there. You'd also need a check to make sure that no expression was checked in a bidirectional way against a type with forall ->, but that, too, is easy.

Also of note is that I have posted #102, by request of the committee, which describes a broader approach to quantifiers in (Dependent) Haskell. I believe this proposal stands alone, but the committee wanted to see where this is all going, and #102 gives a sketch.

@goldfirere

To wit, this new construct would be forbidden in the following places:

Could we have an example of rejected behaviour for each of these bullet point.

In a similar fashion, are there examples where we could use either forall k. … and forall k -> …? What difference would that make?

I've added the examples as requested.

The proposal says

A data constructor can use forall ... -> in its type (as given in GADT-syntax) or arguments, but any use of such a constructor in terms (as opposed to in a type) will be an error.

But that radically under-specifies what is intended for GADT declarations. Remember that GADT data constructors have their own declaration syntax, involving bangs and record fields for example. So with dependent forall, which of these are OK?

data T where
  T1 :: forall a -> a -> T a
  T2 :: Int -> forall a. a -> T a
  T3 :: Int -> forall a -> a -> T a
  T4 :: Int -> (forall a -> a -> T a)

cf GHC ticket 18389

Perhaps we should simply strike out this line of the proposal, leaving it open to do something a bit more ambitious for later.

See #393.