New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Syntax for visible dependent quantification #81

Merged
merged 6 commits into from Sep 30, 2018

Conversation

Projects
None yet
@goldfirere
Contributor

goldfirere commented Oct 14, 2017

This proposes a concrete syntax for a kind that has existed since GHC 8.0, but cannot currently be parsed.

Rendered

@AntC2

This comment has been minimized.

AntC2 commented Oct 14, 2017

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

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 15, 2017

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

@AntC2

This comment has been minimized.

AntC2 commented Oct 15, 2017

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.

?

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Oct 15, 2017

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

@adamgundry

This comment has been minimized.

Contributor

adamgundry commented Oct 15, 2017

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

@AntC2

This comment has been minimized.

AntC2 commented Oct 15, 2017

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
@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 16, 2017

@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!

@nomeata

This comment has been minimized.

Contributor

nomeata commented Oct 16, 2017

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?

@Ericson2314

This comment has been minimized.

Ericson2314 commented Oct 16, 2017

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

@nomeata

This comment has been minimized.

Contributor

nomeata commented Oct 16, 2017

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?

@Ericson2314

This comment has been minimized.

Ericson2314 commented Oct 16, 2017

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

@AntC2

This comment has been minimized.

AntC2 commented Oct 16, 2017

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?

@andrewthad

This comment has been minimized.

Contributor

andrewthad commented Oct 16, 2017

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

Quantifier Dependency Relevance Visibility Matchability
∀ (a :: τ ). ... dep. irrel. inv. (unification) unmatchable
∀ (a :: τ ) → ... dep. irrel. vis. unmatchable
Π (a :: τ ). ... dep. rel. inv. (unification) unmatchable
Π (a :: τ ) → ... dep. rel. vis. unmatchable
τ ⇒ ... non-dep. rel. inv. (solving) unmatchable
τ → ... non-dep. rel. vis. unmatchable

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.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 17, 2017

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.

@AntC2

This comment has been minimized.

AntC2 commented Oct 17, 2017

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?

@simonpj

This comment has been minimized.

Contributor

simonpj commented Oct 17, 2017

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.

@andrewthad

This comment has been minimized.

Contributor

andrewthad commented Oct 17, 2017

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.

@Ericson2314

This comment has been minimized.

Ericson2314 commented Oct 17, 2017

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.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 18, 2017

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

@AntC2

This comment has been minimized.

AntC2 commented Oct 19, 2017

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

@AntC2

This comment has been minimized.

AntC2 commented Oct 19, 2017

  • 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 ‘->’"
@andrewthad

This comment has been minimized.

Contributor

andrewthad commented Oct 19, 2017

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.

@Ericson2314

This comment has been minimized.

Ericson2314 commented Oct 19, 2017

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

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Oct 19, 2017

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.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Nov 10, 2017

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.

@int-index

This comment has been minimized.

Contributor

int-index commented Nov 11, 2017

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?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Nov 13, 2017

The reason this proposal doesn't allow visible dependent quantification for terms is simply that doing so would cause a parsing/renaming nightmare. If I have data T = T and then f T 5 appears somewhere in the module, what T do I mean in that expression? It would depend on the type of f, checking whether f has a visible type argument or not. This is hard to untangle, and I don't wish to attack it here.

As to the roadmap in my thesis: yes, these proposals are part of a coherent whole, but I also think each individual one should be accepted on its own merit as something worthwhile to have even if we don't complete the journey outlined in my thesis. So, while I will aim to link to the thesis in future proposals, I've tried to identify slices of the work that stand on their own so we can make incremental progress.

@goldfirere goldfirere referenced this pull request Dec 20, 2017

Merged

Explicit specificity #99

@simonpj

This comment has been minimized.

Contributor

simonpj commented Dec 21, 2017

What about abstraction? Can I say

type Funny = (forall k -> k -> *) -> *

data T (a :: forall k -> k -> *) = ...

I'm happy with these kinds at the top level of the kind of a TyCon, but nowhere else. That's what GHC currently implements. Specifying this would clean up the vague and imprecise language around "This new construct will be rejected in any context that is unambiguously a type for a term."

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Dec 21, 2017

What about in the type of a data constructor argument? I think that's sensible, too, because the data constructor can be used promoted. If the data constructor is used unpromoted, you'll have a hard time using it at all, because there are no terms of type forall k -> k -> k (for example).

@simonpj

This comment has been minimized.

Contributor

simonpj commented Dec 21, 2017

Yes, ok, data constructors too.

It's a bit odd to have special, top-level syntax for kinds for tycons and data cons, but it is certainly helpful to have a systematic way to denote their visibility etc. But i'd like to see the specification assoicate this notation much more tightly with tycons and datacons. At the top level only!!

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Dec 21, 2017

What do you mean by "At the top level"? What's wrong with

data T :: ((forall k -> k -> Type) -> Bool) -> Type

That doesn't appear to be at the top level.

@simonpj

This comment has been minimized.

Contributor

simonpj commented Dec 21, 2017

I know, and I am hugely dubious about such a thing. GHC cannot represent it today. And do you really mean that I can say

data T :: ((forall k -> k -> Type) -> Bool) -> Type where
  MkT ::  forall (w :: (forall k -> k -> Type) -> Bool).   ...(w S)...   -> T w

This going well beyond what we know

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Dec 21, 2017

This going well beyond what we know

Isn't that the point of a research language, such as Haskell? :)

To be, it seems short-sighted not to make the new syntax fully first-class. I don't think there would be any problems with a construct such as the one you write. I admit that I don't have an application of this idea, but I bet Iceland_jack does.

@int-index

This comment has been minimized.

Contributor

int-index commented Dec 26, 2017

@goldfirere #81 (comment)

The reason this proposal doesn't allow visible dependent quantification for terms is simply that doing so would cause a parsing/renaming nightmare. If I have data T = T and then f T 5 appears somewhere in the module, what T do I mean in that expression? It would depend on the type of f, checking whether f has a visible type argument or not. This is hard to untangle, and I don't wish to attack it here.

I think I have come up with fairly intuitive and lightweight syntax to resolve this ambiguity:

data T = T
f T 5 -- T is term-level (just like today)
f (::T) 5 -- T is type-level

I consider it intuitive because today we have two positions where types are parsed: after :: and after @. The (::T) syntax does not introduce a new lexical construct, it reuses the double colon.

I consider it lightweight because it is still shorter than both Proxy :: Proxy T and Proxy @T. It also has no runtime cost (unlike passing a proxy).

The addition of (::T) does not steal syntax, because today (::T) would mean an annotation for an "empty" expression, which is not a thing.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Dec 26, 2017

I agree that the (:: ty) syntax would work here, but if we eventually end up with real dependent types, then that construct would be out of place. 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. :)

@int-index

This comment has been minimized.

Contributor

int-index commented Dec 26, 2017

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`
@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 5, 2018

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

@int-index

This comment has been minimized.

Contributor

int-index commented Jan 5, 2018

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

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 6, 2018

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.

@aspiwack

This comment has been minimized.

Contributor

aspiwack commented Feb 23, 2018

@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?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Feb 23, 2018

I've added the examples as requested.

@aspiwack

Wow! This was swift! (and very helpful!)

I don't actually understand why it must be forbidden in types-of-terms.

Other than that, I think this proposal is quite solid


foo :: TypeRepV (Type -> Type) a -> ...

and GHC would easily infer that ``a`` should have kind ``Type -> Type``.

This comment has been minimized.

@aspiwack

aspiwack Feb 23, 2018

Contributor

Add something like:

In contrast, with TypeRep where foo would be written as

foo :: TypeRep a -> 

goldfirere added a commit to goldfirere/ghc-proposals that referenced this pull request Apr 16, 2018

@nomeata nomeata merged commit 4edb8a4 into ghc-proposals:master Sep 30, 2018

nomeata added a commit that referenced this pull request Sep 30, 2018

@bravit bravit added the Proposal label Nov 11, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment