The proposal, as written, affects only type signatures and class declarations. It does not cover datatype declarations, though perhaps it should. This seems to be an oversight. A key problem with this notation in type declarations is that H98-syntax datatype and class declarations do two things: they create a new type and they also inform the types of term-level definitions. In the case of a datatype, the terms are the constructors; in the case of a class, the terms are the methods. Suppose we want to make term-level definitions suppress a certain variable but not to suppress this variable in the type definition? For example, perhaps we want data Proxy k (a :: k) = P, where Proxy :: forall k -> k -> Type, but P :: forall {k} (a :: k). Proxy k a. Note the different visibilities at the different levels. We can boil it down to one rule for these situations: RULE. Braces used in type declarations affect only the types of terms declared within the declaration. The braces have no effect whatsoever on the kind of the type(s) declared. With this in mind, I'll answer the questions below:

On May 1, 2018, at 12:56 PM, Iavor Diatchki wrote:

-- 1) The "normal" case. I've written the types of the introduces names underneath, are they correct? data T1 {k} (a :: k) = C1 -- T1 :: forall {k::Type}. k -> Type -- C1 :: forall {k::Type} (a :: k). T1 {k} a

I would say we get T1 :: forall (k :: Type) -> k -> Type -- T1 has *2* visible arguments C1 :: forall {k :: Type} (a :: k). T1 k a -- C1 has one inferred and one specified type argument

-- Am I correct in assuming that while GHC could print the types like that, but users are not allowed to actually write those types (i.e., `T1 {k} (a::k)` is not a valid type).

GHC will print braces only around inferred-variable binding sites, not usage sites. If we wanted k not to be visible in the kind of T1, then one comment on the thread proposed data T1' @k (a :: k) = C1' which would yield T1' :: forall (k :: Type). k -> Type C1' :: forall (k :: Type) (a :: k). T1' a I imagine we could combine the two, so that data T1'' @{k} (a :: k) = C1'' would yield T1'' :: forall (k :: Type). k -> Type C1'' :: forall {k :: Type} (a :: k). T1'' a Under this idea, there would be no way to get k to be *inferred* in the type's kind. A top-level kind signature (#54) would be necessary. Note that the extensions discussed here, with @, are *not* part of this proposal, but might be a future one.

-- 2) Can GHC add extra inferred parameters? (This examples assumes `PolyKinds`) data T2 {k} a = C2 -- C2 :: forall {k1::Type} {k::Type} (a :: k1). T2 {k1} {k} a (ambiguous?)

I get T2 :: forall {x :: Type} {y :: Type}. x -> y -> Type C2 :: forall {x :: Type} {y :: Type} {k :: x} (a :: y). T2 k a This is not an ambiguous type, because all the variables are determined by the (injective) result type. So, in answer to your question: yes.

-- 3) Can we infer non-kind types? data T3 {a} = C3 a -- C3 :: forall {a::Type}. a -> T3 {a}

I get T3 :: Type -> Type C3 :: forall {a :: Type}. a -> T3 a In answer to your question: yes.

-- 4) If `T3` is OK, how does "inferring" work in signatures? To make things concrete, would the following be accepted? f :: T3 f = C3 True -- A): not, because the signature is really: `forall {a}. T3 {a}`. -- B): yes, because we are going to infer that the missing type is `Bool`, so the signature becomes `T3 {Bool}`.

C) not, because T3 still has a visible argument, and therefore T3 has kind `Type -> Type`, which is inappropriate for a type signature.

-- 5) The proposal has a class, something like this: class C a {b} where meth1 :: a -> b

-- How do I write an instance for this class? -- A) instance C Int where meth1 x = x

-- B) instance C Int {Int} where meth1 x = x

I imagine the answer is A) is I see nothing about writing types like `{Int}`. If so, here are a couple of follow up questions about instances:

Neither. I would write instance C Int Int where meth1 x = x The braces in the type declaration affect only the term-level definitions therein, not the type definition, according to RULE.

-- Valid? instance C Int where meth1 x = [] -- instance is really `forall {a::Type}. C Int {[a]}` ?

instance C Int where meth1 x = return x --- error, instance is `C Int {m Int}`, but no `Monad` constraint. -- There doesn't seem to be a way to write the instance with the constraint?

These are not valid.

Sorry for the long e-mail, but I hope that these examples might bring some clarity to users of the proposed feature.

These questions are really helpful in poking at the squishy spots! Thanks. Richard

-Iavor

On Tue, May 1, 2018 at 3:55 AM Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: [Redirecting to the steering committee]

I argue for acceptance.

For me a compelling motivation is this: at the moment we can infer types and kinds that we cannot write down with an explicitly-quantified type signature. That seems all wrong to me: we should be able to write down any type you can infer. The proposal adds notation. It does not add semantics. We already have the distinction between “inferred” and “specified” type variables. You might not like it, but it’s there in GHC. If it wasn’t there already, I’d be happy to debate not adding it. If you want to argue for removing the distinction, that would certainly render the current proposal moot. But that would take a GHC proposal – and there are good reasons for the status quo! What is bad is to maintain the semantic distinction, but be unable to express it. That’s what we have right now, and it’s a bad thing.

What is the distinction between “specified” and “inferred”?

Specified. f :: forall a. blah, or f :: a -> a. You may give a visible type argument at a call of f, but you do not have to. Thus (f x) or (f @type x).

Inferred. f :: t a -> t a. The type of f is really g :: forall {k} (t :: k -> *) (a :: k). t a -> t a

Note that k does not appear at all in the signature; that’s why it is “inferred”. In GHC today you cannot supply an explicit kind argument for g, but you can supply explicit argument for t and a.

So by all means make the case for abolishing the distinction, to render the present proposal moot. But I think it’s unreasonably simply to reject on the grounds of “please think of something better”.

Simon

From: ghc-devs mailto:ghc-devs-bounces@haskell.org> On Behalf Of Iavor Diatchki Sent: 30 April 2018 17:12 To: ghc-devs@haskell.org mailto:ghc-devs@haskell.org Subject: Discussion on proposal #99: forall {k}

Hello,

As a shepherd for proposal #99, I'd like to kick off the discussion. The full proposal is available here: https://github.com/goldfirere/ghc-proposals/blob/explicit-specificity/propos... https://github.com/goldfirere/ghc-proposals/blob/explicit-specificity/propos...

Summary: allows programmers to write `forall {x}` instead of `forall x` in type signatures. The meaning of the braces is that this parameter cannot be instantiated with an explicit type application and will always be inferred. The motivation is to shorten explicit type applications by skipping parameters that are known to be inferable, the common example being omitting the kinds in signatures with poly kinds.

As I understand it, the main motivation for this proposals is to give programmers more flexibility when instantiating type variables, with a less noisy syntax. While the proposed solution might work in some situations, I am unconvinced that it is the best way to address the issue in general, for the following reasons:

1. It requires that programmers commit at declaration time about which arguments will be inferred, and which may be inferred or specified. While in some cases this may be an easy decision to make, in many cases this really is a decision which should be made at the use site of a function (e.g., I'd like to provide argument X, but would like GHC to infer argument Y).

2. It still requires that programmers instantiate arguments in a fixed order, which is sometimes dictated by the structure of the type itslef. Here is, for example, what the proposal suggests to do if you want to provide type before a kind:

typeRep4 :: forall {k} (a :: k) k'. (k ~ k', Typeable a) => TypeRep a

While technically this is not wrong, it is not exactly elegant.

I think that we should reject this proposal, and try to come up with a more comprehensive solution to the problem.

One alternative design is to allow programmers to instantiate type variables by name. This is much more flexible as it allows programmers to instantiate whichever variables they want, and in whatever order. We've been doing this in Cryptol for a long time, and it seems to work really well.

-Iavor

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

RULE. Braces used in type declarations affect only the types of terms declared within the declaration. The braces have no effect whatsoever on the kind of the type(s) declared I’m not very comfortable with this. The obvious alternative is to make them behave exactly the same. Why did you discard that? In any case this applies solely to H98 data type decls, and class decls. For GADT-style decls we give a complete standalone type sig for the constructor. In any case, I’ve lost track of the details here. Might you revise the proposal, incorporating * some of the motivations articulated on this thread (eg by me 😊) * some of the illustrative examples herein * what is not covered [I think stuff to do with data type decls?] Then we can take a fresh run at it. Simon From: Richard Eisenberg Sent: 02 May 2018 03:06 To: Iavor Diatchki Cc: Simon Peyton Jones ; ghc-steering-committee@haskell.org Subject: Re: [ghc-steering-committee] Discussion on proposal #99: forall {k} The proposal, as written, affects only type signatures and class declarations. It does not cover datatype declarations, though perhaps it should. This seems to be an oversight. A key problem with this notation in type declarations is that H98-syntax datatype and class declarations do two things: they create a new type and they also inform the types of term-level definitions. In the case of a datatype, the terms are the constructors; in the case of a class, the terms are the methods. Suppose we want to make term-level definitions suppress a certain variable but not to suppress this variable in the type definition? For example, perhaps we want data Proxy k (a :: k) = P, where Proxy :: forall k -> k -> Type, but P :: forall {k} (a :: k). Proxy k a. Note the different visibilities at the different levels. We can boil it down to one rule for these situations: RULE. Braces used in type declarations affect only the types of terms declared within the declaration. The braces have no effect whatsoever on the kind of the type(s) declared. With this in mind, I'll answer the questions below: On May 1, 2018, at 12:56 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote: -- 1) The "normal" case. I've written the types of the introduces names underneath, are they correct? data T1 {k} (a :: k) = C1 -- T1 :: forall {k::Type}. k -> Type -- C1 :: forall {k::Type} (a :: k). T1 {k} a I would say we get T1 :: forall (k :: Type) -> k -> Type -- T1 has *2* visible arguments C1 :: forall {k :: Type} (a :: k). T1 k a -- C1 has one inferred and one specified type argument -- Am I correct in assuming that while GHC could print the types like that, but users are not allowed to actually write those types (i.e., `T1 {k} (a::k)` is not a valid type). GHC will print braces only around inferred-variable binding sites, not usage sites. If we wanted k not to be visible in the kind of T1, then one comment on the thread proposed data T1' @k (a :: k) = C1' which would yield T1' :: forall (k :: Type). k -> Type C1' :: forall (k :: Type) (a :: k). T1' a I imagine we could combine the two, so that data T1'' @{k} (a :: k) = C1'' would yield T1'' :: forall (k :: Type). k -> Type C1'' :: forall {k :: Type} (a :: k). T1'' a Under this idea, there would be no way to get k to be *inferred* in the type's kind. A top-level kind signature (#54) would be necessary. Note that the extensions discussed here, with @, are *not* part of this proposal, but might be a future one. -- 2) Can GHC add extra inferred parameters? (This examples assumes `PolyKinds`) data T2 {k} a = C2 -- C2 :: forall {k1::Type} {k::Type} (a :: k1). T2 {k1} {k} a (ambiguous?) I get T2 :: forall {x :: Type} {y :: Type}. x -> y -> Type C2 :: forall {x :: Type} {y :: Type} {k :: x} (a :: y). T2 k a This is not an ambiguous type, because all the variables are determined by the (injective) result type. So, in answer to your question: yes. -- 3) Can we infer non-kind types? data T3 {a} = C3 a -- C3 :: forall {a::Type}. a -> T3 {a} I get T3 :: Type -> Type C3 :: forall {a :: Type}. a -> T3 a In answer to your question: yes. -- 4) If `T3` is OK, how does "inferring" work in signatures? To make things concrete, would the following be accepted? f :: T3 f = C3 True -- A): not, because the signature is really: `forall {a}. T3 {a}`. -- B): yes, because we are going to infer that the missing type is `Bool`, so the signature becomes `T3 {Bool}`. C) not, because T3 still has a visible argument, and therefore T3 has kind `Type -> Type`, which is inappropriate for a type signature. -- 5) The proposal has a class, something like this: class C a {b} where meth1 :: a -> b -- How do I write an instance for this class? -- A) instance C Int where meth1 x = x -- B) instance C Int {Int} where meth1 x = x I imagine the answer is A) is I see nothing about writing types like `{Int}`. If so, here are a couple of follow up questions about instances: Neither. I would write instance C Int Int where meth1 x = x The braces in the type declaration affect only the term-level definitions therein, not the type definition, according to RULE. -- Valid? instance C Int where meth1 x = [] -- instance is really `forall {a::Type}. C Int {[a]}` ? instance C Int where meth1 x = return x --- error, instance is `C Int {m Int}`, but no `Monad` constraint. -- There doesn't seem to be a way to write the instance with the constraint? These are not valid. Sorry for the long e-mail, but I hope that these examples might bring some clarity to users of the proposed feature. These questions are really helpful in poking at the squishy spots! Thanks. Richard -Iavor On Tue, May 1, 2018 at 3:55 AM Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: [Redirecting to the steering committee] I argue for acceptance. * For me a compelling motivation is this: at the moment we can infer types and kinds that we cannot write down with an explicitly-quantified type signature. That seems all wrong to me: we should be able to write down any type you can infer. * The proposal adds notation. It does not add semantics. We already have the distinction between “inferred” and “specified” type variables. You might not like it, but it’s there in GHC. * If it wasn’t there already, I’d be happy to debate not adding it. * If you want to argue for removing the distinction, that would certainly render the current proposal moot. But that would take a GHC proposal – and there are good reasons for the status quo! * What is bad is to maintain the semantic distinction, but be unable to express it. That’s what we have right now, and it’s a bad thing. What is the distinction between “specified” and “inferred”? * Specified. f :: forall a. blah, or f :: a -> a. You may give a visible type argument at a call of f, but you do not have to. Thus (f x) or (f @type x). * Inferred. f :: t a -> t a. The type of f is really g :: forall {k} (t :: k -> *) (a :: k). t a -> t a Note that k does not appear at all in the signature; that’s why it is “inferred”. In GHC today you cannot supply an explicit kind argument for g, but you can supply explicit argument for t and a. So by all means make the case for abolishing the distinction, to render the present proposal moot. But I think it’s unreasonably simply to reject on the grounds of “please think of something better”. Simon From: ghc-devs mailto:ghc-devs-bounces@haskell.org> On Behalf Of Iavor Diatchki Sent: 30 April 2018 17:12 To: ghc-devs@haskell.orgmailto:ghc-devs@haskell.org Subject: Discussion on proposal #99: forall {k} Hello, As a shepherd for proposal #99, I'd like to kick off the discussion. The full proposal is available here: https://github.com/goldfirere/ghc-proposals/blob/explicit-specificity/propos...https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fexplicit-specificity%2Fproposals%2F0000-explicit-specificity.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C91b5ba6ae508426a711b08d5afd13277%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608235390001323&sdata=2tYpwTwlWtp73a1pkWEIhIOQFnWwLufJWSDKwRkqB8g%3D&reserved=0 Summary: allows programmers to write `forall {x}` instead of `forall x` in type signatures. The meaning of the braces is that this parameter cannot be instantiated with an explicit type application and will always be inferred. The motivation is to shorten explicit type applications by skipping parameters that are known to be inferable, the common example being omitting the kinds in signatures with poly kinds. As I understand it, the main motivation for this proposals is to give programmers more flexibility when instantiating type variables, with a less noisy syntax. While the proposed solution might work in some situations, I am unconvinced that it is the best way to address the issue in general, for the following reasons: 1. It requires that programmers commit at declaration time about which arguments will be inferred, and which may be inferred or specified. While in some cases this may be an easy decision to make, in many cases this really is a decision which should be made at the use site of a function (e.g., I'd like to provide argument X, but would like GHC to infer argument Y). 2. It still requires that programmers instantiate arguments in a fixed order, which is sometimes dictated by the structure of the type itslef. Here is, for example, what the proposal suggests to do if you want to provide type before a kind: typeRep4 :: forall {k} (a :: k) k'. (k ~ k', Typeable a) => TypeRep a While technically this is not wrong, it is not exactly elegant. I think that we should reject this proposal, and try to come up with a more comprehensive solution to the problem. One alternative design is to allow programmers to instantiate type variables by name. This is much more flexible as it allows programmers to instantiate whichever variables they want, and in whatever order. We've been doing this in Cryptol for a long time, and it seems to work really well. -Iavor _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

OK -- I could agree with forbidding braces on `data` (given that the GADT-syntax alternative exists), but what about `class`? And then if we allow it on `class`, it seems a bit silly not to do the analogous thing on `data`. (Note that the proposal currently describes the same scheme as I have described in this email thread, but only about `class`.) Richard

On May 2, 2018, at 9:48 AM, Joachim Breitner wrote:

Hi,

Am Dienstag, den 01.05.2018, 22:05 -0400 schrieb Richard Eisenberg:

...

We can boil it down to one rule for these situations: RULE. Braces used in type declarations affect only the types of terms declared within the declaration. The braces have no effect whatsoever on the kind of the type(s) declared.

With this in mind, I'll answer the questions below:

...

On May 1, 2018, at 12:56 PM, Iavor Diatchki wrote:

-- 1) The "normal" case. I've written the types of the introduces names underneath, are they correct? data T1 {k} (a :: k) = C1 -- T1 :: forall {k::Type}. k -> Type -- C1 :: forall {k::Type} (a :: k). T1 {k} a

I would say we get

T1 :: forall (k :: Type) -> k -> Type -- T1 has *2* visible arguments C1 :: forall {k :: Type} (a :: k). T1 k a -- C1 has one inferred and one specified type argument

I think this is highly confusing. The {k} is on T1, but it does not affect T1, but rather something else?

What is wrong with “if you want to have different specificity on the tycon and the datacon, use GADTSyntax”?

Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/ _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Joachim, you are always a fount of interesting ideas.

On May 2, 2018, at 2:51 PM, Joachim Breitner wrote:

class C k (a : k) where meth :: a meth :: forall {k} a. C k a -> k -> Constraint

I think this is brilliant. But not only for this proposal! Imagine this: class Num a where fromInteger :: Integer -> a fromInteger :: Integer -> forall a. Num a => a If we do that, then #129 is essentially solved, at no further cost to anyone. (Note that in all Haskell98-style code, no one will ever be able to notice the changed type of fromInteger.) This approach also allows for the possibility of reordering quantified type variables for Haskell98-style constructors, if anyone should want to do it. And it allows for updated types (including quantified variable ordering, etc.) for record selectors. And it allows (maybe?) for giving good types to GADT record selectors: data X a where Foo :: { bar :: Int } -> X Int Quux :: { bar :: Bool } -> X Bool bar :: X a -> a GHC currently rejects the declaration for X, but it could be accepted if only we could specify the correct type of bar. And now we can. I don't particularly want to cook up the typing rules here, but I don't think I'm totally crazy. GADT record selectors aside, the rule for these could be that the top-level type signature must be equivalent w.r.t. the subtype relation with the original type signature. That is, if the new signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy enough to check for. The implementation would probably do a little worker/wrapper stunt.

class C k (a : k) where meth :: a specificity meth inferred specified

This is also quite interesting. Syntax for role annotations started out very terse, and written inline with datatype declarations. Over time, we recognized that it was more ergonomic to separate them from the declarations. One reason for this was to ease the transition period and requisite CPP clutter. I still prefer your first suggestion here more because it seems to have greater applicability.

(The rambliness of this mail is an indication that the proposal does not immediately resonates as the obvious right and best solution with me…)

I agree, and so I'm pleased with this debate. Richard

Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/ _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Hello, based on the discussion so far, it seems that #99 in its current form might not be exactly what we want, so I'd say that we should reject it for the moment. Overall, I agree that it would be nice to come up with a consistent notation for things that are currently happening in GHC but we can't write, so perhaps we could revisit this with a revised proposal at a later time? -Iavor On Sat, May 5, 2018 at 8:48 PM Joachim Breitner wrote:

Hi,

Am Mittwoch, den 02.05.2018, 16:10 -0400 schrieb Richard Eisenberg:

...

Joachim, you are always a fount of interesting ideas.

...

On May 2, 2018, at 2:51 PM, Joachim Breitner wrote:

class C k (a : k) where meth :: a meth :: forall {k} a. C k a -> k -> Constraint

I think this is brilliant. But not only for this proposal! Imagine this:

class Num a where fromInteger :: Integer -> a

fromInteger :: Integer -> forall a. Num a => a

If we do that, then #129 is essentially solved, at no further cost to anyone. (Note that in all Haskell98-style code, no one will ever be able to notice the changed type of fromInteger.)

This approach also allows for the possibility of reordering quantified type variables for Haskell98-style constructors, if anyone should want to do it.

And it allows for updated types (including quantified variable ordering, etc.) for record selectors.

And it allows (maybe?) for giving good types to GADT record selectors:

data X a where Foo :: { bar :: Int } -> X Int Quux :: { bar :: Bool } -> X Bool bar :: X a -> a

GHC currently rejects the declaration for X, but it could be accepted if only we could specify the correct type of bar. And now we can. I don't particularly want to cook up the typing rules here, but I don't think I'm totally crazy.

GADT record selectors aside, the rule for these could be that the top-level type signature must be equivalent w.r.t. the subtype relation with the original type signature. That is, if the new signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy enough to check for. The implementation would probably do a little worker/wrapper stunt.

I smell a new proposal… what does this mean for #99? Will you want to revise it?

Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/ _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

I’m keen to get #99 into GHC in some form. My motivation (which could be a fourth bullet in the proposal) is that it should be possible for a programmer to write a fully-explicit type signature for anything GHC can infer. But currently we can’t. For typeRep1 GHC infers the signature shown for typeRep3; but we can’t write it down. based on the discussion so far, it seems that #99 in its current form might not be exactly what we want Can you summarise the reasons it might not be exactly what we want? Simon From: ghc-steering-committee On Behalf Of Richard Eisenberg Sent: 24 May 2018 21:17 To: Iavor Diatchki Cc: ghc-steering-committee@haskell.org; Joachim Breitner Subject: Re: [ghc-steering-committee] Discussion on proposal #99: forall {k} I do plan on turning Joachim's recent suggestion into a separate proposal, and then to modify #99. But the modification would remove only the bit about classes, not the feature overall. I don't have time to do this now, though -- will do next week. Richard On May 24, 2018, at 1:54 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote: Hello, based on the discussion so far, it seems that #99 in its current form might not be exactly what we want, so I'd say that we should reject it for the moment. Overall, I agree that it would be nice to come up with a consistent notation for things that are currently happening in GHC but we can't write, so perhaps we could revisit this with a revised proposal at a later time? -Iavor On Sat, May 5, 2018 at 8:48 PM Joachim Breitner mailto:mail@joachim-breitner.de> wrote: Hi, Am Mittwoch, den 02.05.2018, 16:10 -0400 schrieb Richard Eisenberg:

Joachim, you are always a fount of interesting ideas.

...

On May 2, 2018, at 2:51 PM, Joachim Breitner wrote:

class C k (a : k) where meth :: a meth :: forall {k} a. C k a -> k -> Constraint

I think this is brilliant. But not only for this proposal! Imagine this:

class Num a where fromInteger :: Integer -> a

fromInteger :: Integer -> forall a. Num a => a

If we do that, then #129 is essentially solved, at no further cost to anyone. (Note that in all Haskell98-style code, no one will ever be able to notice the changed type of fromInteger.)

This approach also allows for the possibility of reordering quantified type variables for Haskell98-style constructors, if anyone should want to do it.

And it allows for updated types (including quantified variable ordering, etc.) for record selectors.

And it allows (maybe?) for giving good types to GADT record selectors:

data X a where Foo :: { bar :: Int } -> X Int Quux :: { bar :: Bool } -> X Bool bar :: X a -> a

GHC currently rejects the declaration for X, but it could be accepted if only we could specify the correct type of bar. And now we can. I don't particularly want to cook up the typing rules here, but I don't think I'm totally crazy.

GADT record selectors aside, the rule for these could be that the top-level type signature must be equivalent w.r.t. the subtype relation with the original type signature. That is, if the new signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy enough to check for. The implementation would probably do a little worker/wrapper stunt.

I smell a new proposal… what does this mean for #99? Will you want to revise it? Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.demailto:mail@joachim-breitner.de http://www.joachim-breitner.de/https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Ca43c362fd18e4163aeba08d5c1b34be2%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636627898179266033&sdata=1cwPEVKXCcP3DuCHXOFuA%2BbEBniRLjcKI%2BAZji5vR4Q%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

I have posted the new proposal, at https://github.com/ghc-proposals/ghc-proposals/pull/148 https://github.com/ghc-proposals/ghc-proposals/pull/148 I've also updated #99 to clarify where the new syntax is allowed. For Iavor's examples:

data T1 a = C1 a

type T1 :: Type -> Type C1 :: forall a. a -> T1 a

data T2 (a :: k) = C2 { f2 :: Proxy a }

type T2 :: forall k. k -> Type C2 :: forall k (a :: k). Proxy a -> T2 a f2 :: forall k (a :: k). T2 a -> Proxy a

data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a

type T3 :: forall {k}. k -> Type C3 :: forall k (a :: k). Proxy a -> T3 a

data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a

type T4 :: forall {k}. k -> Type C4 :: forall {k} (a :: k). Proxy a -> T3 a

data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a

Rejected, as k is used dependently but is not lexically dependent. (This is no change.) It we have

data T5 k (a :: k) where C5 :: forall k (a :: k). Proxy a -> T5 k a

we would get type T5 :: forall k -> k -> Type C5 :: forall k (a :: k). Proxy a -> T5 k a

data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a

Rejected, like T6. If we revise to:

data T6 k (a :: k) where C6 :: forall {k} (a::k). Proxy a -> T6 k a

we get type T6 :: forall k -> k -> Type C6 :: forall {k} (a::k). Proxy a -> T6 k a I've updated the proposal itself to include these examples. Does this help to clarify? Richard

On May 25, 2018, at 1:56 PM, Iavor Diatchki wrote:

Hello,

well, I thought that Richard was going to write a new proposal based on the feedback here, but it sounds like he is planning to revise #99, and then write a separate new one. I guess we should discuss the proposal again once the changes are in. I would encourage Richard to add some text and examples to clarify exactly what's in the proposal and what's not, and how things are supposed to work. Here are some examples, for which it would be illuminating (to me) to see the types/kinds of all names introduced.

data T1 a = C1 a data T2 (a :: k) = C2 { f2 :: Proxy a } data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a

-Iavor

On Fri, May 25, 2018 at 2:02 AM Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: I’m keen to get #99 into GHC in some form.

My motivation (which could be a fourth bullet in the proposal) is that it should be possible for a programmer to write a fully-explicit type signature for anything GHC can infer. But currently we can’t. For typeRep1 GHC infers the signature shown for typeRep3; but we can’t write it down.

based on the discussion so far, it seems that #99 in its current form might not be exactly what we want

Can you summarise the reasons it might not be exactly what we want?

Simon

From: ghc-steering-committee mailto:ghc-steering-committee-bounces@haskell.org> On Behalf Of Richard Eisenberg Sent: 24 May 2018 21:17 To: Iavor Diatchki mailto:iavor.diatchki@gmail.com> Cc: ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org; Joachim Breitner mailto:mail@joachim-breitner.de> Subject: Re: [ghc-steering-committee] Discussion on proposal #99: forall {k}

I do plan on turning Joachim's recent suggestion into a separate proposal, and then to modify #99. But the modification would remove only the bit about classes, not the feature overall. I don't have time to do this now, though -- will do next week.

Richard

On May 24, 2018, at 1:54 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote:

Hello,

based on the discussion so far, it seems that #99 in its current form might not be exactly what we want, so I'd say that we should reject it for the moment. Overall, I agree that it would be nice to come up with a consistent notation for things that are currently happening in GHC but we can't write, so perhaps we could revisit this with a revised proposal at a later time?

-Iavor

On Sat, May 5, 2018 at 8:48 PM Joachim Breitner mailto:mail@joachim-breitner.de> wrote:

Hi,

Am Mittwoch, den 02.05.2018, 16:10 -0400 schrieb Richard Eisenberg:

...

Joachim, you are always a fount of interesting ideas.

...

On May 2, 2018, at 2:51 PM, Joachim Breitner wrote:

class C k (a : k) where meth :: a meth :: forall {k} a. C k a -> k -> Constraint

I think this is brilliant. But not only for this proposal! Imagine this:

class Num a where fromInteger :: Integer -> a

fromInteger :: Integer -> forall a. Num a => a

If we do that, then #129 is essentially solved, at no further cost to anyone. (Note that in all Haskell98-style code, no one will ever be able to notice the changed type of fromInteger.)

This approach also allows for the possibility of reordering quantified type variables for Haskell98-style constructors, if anyone should want to do it.

And it allows for updated types (including quantified variable ordering, etc.) for record selectors.

And it allows (maybe?) for giving good types to GADT record selectors:

data X a where Foo :: { bar :: Int } -> X Int Quux :: { bar :: Bool } -> X Bool bar :: X a -> a

GHC currently rejects the declaration for X, but it could be accepted if only we could specify the correct type of bar. And now we can. I don't particularly want to cook up the typing rules here, but I don't think I'm totally crazy.

GADT record selectors aside, the rule for these could be that the top-level type signature must be equivalent w.r.t. the subtype relation with the original type signature. That is, if the new signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy enough to check for. The implementation would probably do a little worker/wrapper stunt.

I smell a new proposal… what does this mean for #99? Will you want to revise it?

Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de mailto:mail@joachim-breitner.de http://www.joachim-breitner.de/ https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Ca43c362fd18e4163aeba08d5c1b34be2%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636627898179266033&sdata=1cwPEVKXCcP3DuCHXOFuA%2BbEBniRLjcKI%2BAZji5vR4Q%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

But we morally *do* have explicit kind application. See accepted proposal https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0015-ty... https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0015-ty... So the only reason that we don't have it is that GHC hasn't caught up to its specification. (I have a student working on this now.) The reason that T2 and T3 are different here is that T2 mentions the k in the type declaration, while T3 mentions it only in the constructor declaration. Richard

On Jun 26, 2018, at 6:52 PM, Iavor Diatchki wrote:

Hello, thanks for the revisions---I read through the new version, and I think I almost understand the plan. I would say that for this proposal it makes more sense to just deal with explicit specificities at the value level, and never have the curly braces in type constructors. Since we don't have an explicit kind application at the type level (e.g., we can't write `Proxy @Type`), I don't think it really makes sense to add the braces to type constructors. If we ever implemented THAT feature, then we can discuss which declarations should have explicit and which should have implicit parameters. In the current set of examples, I find it odd that `T2` does not have braces, but `T3` does.

-Iavor

On Wed, Jun 20, 2018 at 2:15 PM Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote: I have posted the new proposal, at https://github.com/ghc-proposals/ghc-proposals/pull/148 https://github.com/ghc-proposals/ghc-proposals/pull/148

I've also updated #99 to clarify where the new syntax is allowed.

For Iavor's examples:

...

data T1 a = C1 a

type T1 :: Type -> Type C1 :: forall a. a -> T1 a

...

data T2 (a :: k) = C2 { f2 :: Proxy a }

type T2 :: forall k. k -> Type C2 :: forall k (a :: k). Proxy a -> T2 a f2 :: forall k (a :: k). T2 a -> Proxy a

...

data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a

type T3 :: forall {k}. k -> Type C3 :: forall k (a :: k). Proxy a -> T3 a

...

data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a

type T4 :: forall {k}. k -> Type C4 :: forall {k} (a :: k). Proxy a -> T3 a

...

data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a

Rejected, as k is used dependently but is not lexically dependent. (This is no change.) It we have

...

data T5 k (a :: k) where C5 :: forall k (a :: k). Proxy a -> T5 k a

we would get

type T5 :: forall k -> k -> Type C5 :: forall k (a :: k). Proxy a -> T5 k a

...

data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a

Rejected, like T6. If we revise to:

...

data T6 k (a :: k) where C6 :: forall {k} (a::k). Proxy a -> T6 k a

we get

type T6 :: forall k -> k -> Type C6 :: forall {k} (a::k). Proxy a -> T6 k a

I've updated the proposal itself to include these examples.

Does this help to clarify?

Richard

...

On May 25, 2018, at 1:56 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote:

Hello,

well, I thought that Richard was going to write a new proposal based on the feedback here, but it sounds like he is planning to revise #99, and then write a separate new one. I guess we should discuss the proposal again once the changes are in. I would encourage Richard to add some text and examples to clarify exactly what's in the proposal and what's not, and how things are supposed to work. Here are some examples, for which it would be illuminating (to me) to see the types/kinds of all names introduced.

data T1 a = C1 a data T2 (a :: k) = C2 { f2 :: Proxy a } data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a

-Iavor

On Fri, May 25, 2018 at 2:02 AM Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: I’m keen to get #99 into GHC in some form.

My motivation (which could be a fourth bullet in the proposal) is that it should be possible for a programmer to write a fully-explicit type signature for anything GHC can infer. But currently we can’t. For typeRep1 GHC infers the signature shown for typeRep3; but we can’t write it down.

based on the discussion so far, it seems that #99 in its current form might not be exactly what we want

Can you summarise the reasons it might not be exactly what we want?

Simon

From: ghc-steering-committee mailto:ghc-steering-committee-bounces@haskell.org> On Behalf Of Richard Eisenberg Sent: 24 May 2018 21:17 To: Iavor Diatchki mailto:iavor.diatchki@gmail.com> Cc: ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org; Joachim Breitner mailto:mail@joachim-breitner.de> Subject: Re: [ghc-steering-committee] Discussion on proposal #99: forall {k}

I do plan on turning Joachim's recent suggestion into a separate proposal, and then to modify #99. But the modification would remove only the bit about classes, not the feature overall. I don't have time to do this now, though -- will do next week.

Richard

On May 24, 2018, at 1:54 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote:

Hello,

based on the discussion so far, it seems that #99 in its current form might not be exactly what we want, so I'd say that we should reject it for the moment. Overall, I agree that it would be nice to come up with a consistent notation for things that are currently happening in GHC but we can't write, so perhaps we could revisit this with a revised proposal at a later time?

-Iavor

On Sat, May 5, 2018 at 8:48 PM Joachim Breitner mailto:mail@joachim-breitner.de> wrote:

Hi,

Am Mittwoch, den 02.05.2018, 16:10 -0400 schrieb Richard Eisenberg:

...

Joachim, you are always a fount of interesting ideas.

...

On May 2, 2018, at 2:51 PM, Joachim Breitner wrote:

class C k (a : k) where meth :: a meth :: forall {k} a. C k a -> k -> Constraint

I think this is brilliant. But not only for this proposal! Imagine this:

class Num a where fromInteger :: Integer -> a

fromInteger :: Integer -> forall a. Num a => a

If we do that, then #129 is essentially solved, at no further cost to anyone. (Note that in all Haskell98-style code, no one will ever be able to notice the changed type of fromInteger.)

This approach also allows for the possibility of reordering quantified type variables for Haskell98-style constructors, if anyone should want to do it.

And it allows for updated types (including quantified variable ordering, etc.) for record selectors.

And it allows (maybe?) for giving good types to GADT record selectors:

data X a where Foo :: { bar :: Int } -> X Int Quux :: { bar :: Bool } -> X Bool bar :: X a -> a

GHC currently rejects the declaration for X, but it could be accepted if only we could specify the correct type of bar. And now we can. I don't particularly want to cook up the typing rules here, but I don't think I'm totally crazy.

GADT record selectors aside, the rule for these could be that the top-level type signature must be equivalent w.r.t. the subtype relation with the original type signature. That is, if the new signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy enough to check for. The implementation would probably do a little worker/wrapper stunt.

I smell a new proposal… what does this mean for #99? Will you want to revise it?

Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de mailto:mail@joachim-breitner.de http://www.joachim-breitner.de/ https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Ca43c362fd18e4163aeba08d5c1b34be2%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636627898179266033&sdata=1cwPEVKXCcP3DuCHXOFuA%2BbEBniRLjcKI%2BAZji5vR4Q%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Joachim, One thing I occasionally find tricky is this: what proposals exist, in what state? One way to find out is to start here https://github.com/ghc-proposals/ghc-proposals and use the links for “accepted”, “dormant” etc. But * You have to look at several different lists, one by one. * There isn’t a ‘rejected’ list Worse, the numbering seems to change. IN Richard’s link below, it looks as if 0015-type-level-type-applcations is #15. But it isn’t. It actually appears in the list of accepted proposals as #80. That’s very confusing. I really thought the number was unique. It’s be great to have a single comprehensive list, with a unique ID, that says for each proposal what its status is. Is that possible? Clearly I (still) don’t really understand the pull-request model well enough, which is a bit embarrassing given how universal it has become. (Side question: does anyone have a favourite tutorial?) Simon From: Richard Eisenberg Sent: 28 June 2018 05:45 To: Iavor Diatchki Cc: Simon Peyton Jones ; ghc-steering-committee@haskell.org; Joachim Breitner Subject: Re: [ghc-steering-committee] Discussion on proposal #99: forall {k} But we morally *do* have explicit kind application. See accepted proposal https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0015-ty...https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0015-type-level-type-applications.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C15fcb1b642114e05f1a808d5dcb1e5ca%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636657578984502957&sdata=%2B7wS%2F75AielivG1KfFAzGPXKSS5aHOtEVwy9Q6WyYLU%3D&reserved=0 So the only reason that we don't have it is that GHC hasn't caught up to its specification. (I have a student working on this now.) The reason that T2 and T3 are different here is that T2 mentions the k in the type declaration, while T3 mentions it only in the constructor declaration. Richard On Jun 26, 2018, at 6:52 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote: Hello, thanks for the revisions---I read through the new version, and I think I almost understand the plan. I would say that for this proposal it makes more sense to just deal with explicit specificities at the value level, and never have the curly braces in type constructors. Since we don't have an explicit kind application at the type level (e.g., we can't write `Proxy @Type`), I don't think it really makes sense to add the braces to type constructors. If we ever implemented THAT feature, then we can discuss which declarations should have explicit and which should have implicit parameters. In the current set of examples, I find it odd that `T2` does not have braces, but `T3` does. -Iavor On Wed, Jun 20, 2018 at 2:15 PM Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote: I have posted the new proposal, at https://github.com/ghc-proposals/ghc-proposals/pull/148https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F148&data=02%7C01%7Csimonpj%40microsoft.com%7C15fcb1b642114e05f1a808d5dcb1e5ca%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636657578984502957&sdata=RQ4V%2FWdRz009o6sieAUpx7wQ6RCqWydsQGbENvHFZfM%3D&reserved=0 I've also updated #99 to clarify where the new syntax is allowed. For Iavor's examples: data T1 a = C1 a type T1 :: Type -> Type C1 :: forall a. a -> T1 a data T2 (a :: k) = C2 { f2 :: Proxy a } type T2 :: forall k. k -> Type C2 :: forall k (a :: k). Proxy a -> T2 a f2 :: forall k (a :: k). T2 a -> Proxy a data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a type T3 :: forall {k}. k -> Type C3 :: forall k (a :: k). Proxy a -> T3 a data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a type T4 :: forall {k}. k -> Type C4 :: forall {k} (a :: k). Proxy a -> T3 a data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a Rejected, as k is used dependently but is not lexically dependent. (This is no change.) It we have

data T5 k (a :: k) where C5 :: forall k (a :: k). Proxy a -> T5 k a

we would get type T5 :: forall k -> k -> Type C5 :: forall k (a :: k). Proxy a -> T5 k a data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a Rejected, like T6. If we revise to:

data T6 k (a :: k) where C6 :: forall {k} (a::k). Proxy a -> T6 k a

we get type T6 :: forall k -> k -> Type C6 :: forall {k} (a::k). Proxy a -> T6 k a I've updated the proposal itself to include these examples. Does this help to clarify? Richard On May 25, 2018, at 1:56 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote: Hello, well, I thought that Richard was going to write a new proposal based on the feedback here, but it sounds like he is planning to revise #99, and then write a separate new one. I guess we should discuss the proposal again once the changes are in. I would encourage Richard to add some text and examples to clarify exactly what's in the proposal and what's not, and how things are supposed to work. Here are some examples, for which it would be illuminating (to me) to see the types/kinds of all names introduced. data T1 a = C1 a data T2 (a :: k) = C2 { f2 :: Proxy a } data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a -Iavor On Fri, May 25, 2018 at 2:02 AM Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: I’m keen to get #99 into GHC in some form. My motivation (which could be a fourth bullet in the proposal) is that it should be possible for a programmer to write a fully-explicit type signature for anything GHC can infer. But currently we can’t. For typeRep1 GHC infers the signature shown for typeRep3; but we can’t write it down. based on the discussion so far, it seems that #99 in its current form might not be exactly what we want Can you summarise the reasons it might not be exactly what we want? Simon From: ghc-steering-committee mailto:ghc-steering-committee-bounces@haskell.org> On Behalf Of Richard Eisenberg Sent: 24 May 2018 21:17 To: Iavor Diatchki mailto:iavor.diatchki@gmail.com> Cc: ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org; Joachim Breitner mailto:mail@joachim-breitner.de> Subject: Re: [ghc-steering-committee] Discussion on proposal #99: forall {k} I do plan on turning Joachim's recent suggestion into a separate proposal, and then to modify #99. But the modification would remove only the bit about classes, not the feature overall. I don't have time to do this now, though -- will do next week. Richard On May 24, 2018, at 1:54 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote: Hello, based on the discussion so far, it seems that #99 in its current form might not be exactly what we want, so I'd say that we should reject it for the moment. Overall, I agree that it would be nice to come up with a consistent notation for things that are currently happening in GHC but we can't write, so perhaps we could revisit this with a revised proposal at a later time? -Iavor On Sat, May 5, 2018 at 8:48 PM Joachim Breitner mailto:mail@joachim-breitner.de> wrote: Hi, Am Mittwoch, den 02.05.2018, 16:10 -0400 schrieb Richard Eisenberg:

Joachim, you are always a fount of interesting ideas.

...

On May 2, 2018, at 2:51 PM, Joachim Breitner wrote:

class C k (a : k) where meth :: a meth :: forall {k} a. C k a -> k -> Constraint

I think this is brilliant. But not only for this proposal! Imagine this:

class Num a where fromInteger :: Integer -> a

fromInteger :: Integer -> forall a. Num a => a

If we do that, then #129 is essentially solved, at no further cost to anyone. (Note that in all Haskell98-style code, no one will ever be able to notice the changed type of fromInteger.)

This approach also allows for the possibility of reordering quantified type variables for Haskell98-style constructors, if anyone should want to do it.

And it allows for updated types (including quantified variable ordering, etc.) for record selectors.

And it allows (maybe?) for giving good types to GADT record selectors:

data X a where Foo :: { bar :: Int } -> X Int Quux :: { bar :: Bool } -> X Bool bar :: X a -> a

GHC currently rejects the declaration for X, but it could be accepted if only we could specify the correct type of bar. And now we can. I don't particularly want to cook up the typing rules here, but I don't think I'm totally crazy.

GADT record selectors aside, the rule for these could be that the top-level type signature must be equivalent w.r.t. the subtype relation with the original type signature. That is, if the new signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy enough to check for. The implementation would probably do a little worker/wrapper stunt.

I smell a new proposal… what does this mean for #99? Will you want to revise it? Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.demailto:mail@joachim-breitner.de http://www.joachim-breitner.de/https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Ca43c362fd18e4163aeba08d5c1b34be2%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636627898179266033&sdata=1cwPEVKXCcP3DuCHXOFuA%2BbEBniRLjcKI%2BAZji5vR4Q%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

I am supportive of accepting the proposal, but I think that we should address the point raised by Joachim on the the git-hub thread first ( https://github.com/ghc-proposals/ghc-proposals/pull/99#issuecomment-40106097...). It really is not quite clear if the specificity is a property of the type itself, or the thing that has that type. On Thu, Jun 28, 2018 at 1:07 AM Simon Peyton Jones wrote:

I’m keen on this proposal. I am very keen to be able to express in a type or kind signature everything needful to use the value (or type constructor). The proposal gives an example at the term level. It’d be strengthened by an example at the type level. Eg

type T1 :: forall {k}. (k->Type) -> k -> Type

data T1 f a = MkT (f a)

type T2 :: forall k. (k->Type) -> k -> Type

data T2 f (a::k) = MkT2 (f a)

Here T1 has an inferred kind variable, mentioned nowhere in the declaration. The kind signature (which I have written as if it were code, which is the subject of a separate proposal) is inferred as shown.

T2 mentions k, so its kind signature looks a bit different.

What’s the difference? It’s exactly in explicit kind application. You can write (T1 @Type Maybe Int), but T2 can’t have that explicit kind argument.

The whole business of Required/Specified/Inferred is more complicated than I like, but if we have it (which we do right now) we should allow the programmer to specify exactly what they mean.

(An alternative is to abolish the Specified/Inferred distinction, but that carries significant costs of its own and no one is proposing it.)

Let’s accept!

Simon

*From:* Richard Eisenberg *Sent:* 28 June 2018 05:45 *To:* Iavor Diatchki *Cc:* Simon Peyton Jones ; ghc-steering-committee@haskell.org; Joachim Breitner < mail@joachim-breitner.de>

*Subject:* Re: [ghc-steering-committee] Discussion on proposal #99: forall {k}

But we morally *do* have explicit kind application. See accepted proposal https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0015-ty... https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0015-type-level-type-applications.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C15fcb1b642114e05f1a808d5dcb1e5ca%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636657578984502957&sdata=%2B7wS%2F75AielivG1KfFAzGPXKSS5aHOtEVwy9Q6WyYLU%3D&reserved=0 So the only reason that we don't have it is that GHC hasn't caught up to its specification. (I have a student working on this now.)

The reason that T2 and T3 are different here is that T2 mentions the k in the type declaration, while T3 mentions it only in the constructor declaration.

Richard

On Jun 26, 2018, at 6:52 PM, Iavor Diatchki wrote:

Hello,

thanks for the revisions---I read through the new version, and I think I almost understand the plan. I would say that for this proposal it makes more sense to just deal with explicit specificities at the value level, and never have the curly braces in type constructors. Since we don't have an explicit kind application at the type level (e.g., we can't write `Proxy @Type`), I don't think it really makes sense to add the braces to type constructors. If we ever implemented THAT feature, then we can discuss which declarations should have explicit and which should have implicit parameters. In the current set of examples, I find it odd that `T2` does not have braces, but `T3` does.

-Iavor

On Wed, Jun 20, 2018 at 2:15 PM Richard Eisenberg wrote:

I have posted the new proposal, at https://github.com/ghc-proposals/ghc-proposals/pull/148 https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F148&data=02%7C01%7Csimonpj%40microsoft.com%7C15fcb1b642114e05f1a808d5dcb1e5ca%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636657578984502957&sdata=RQ4V%2FWdRz009o6sieAUpx7wQ6RCqWydsQGbENvHFZfM%3D&reserved=0

I've also updated #99 to clarify where the new syntax is allowed.

For Iavor's examples:

data T1 a = C1 a

type T1 :: Type -> Type

C1 :: forall a. a -> T1 a

data T2 (a :: k) = C2 { f2 :: Proxy a }

type T2 :: forall k. k -> Type

C2 :: forall k (a :: k). Proxy a -> T2 a

f2 :: forall k (a :: k). T2 a -> Proxy a

data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a

type T3 :: forall {k}. k -> Type

C3 :: forall k (a :: k). Proxy a -> T3 a

data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a

type T4 :: forall {k}. k -> Type

C4 :: forall {k} (a :: k). Proxy a -> T3 a

data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a

Rejected, as k is used dependently but is not lexically dependent. (This is no change.) It we have

...

data T5 k (a :: k) where C5 :: forall k (a :: k). Proxy a -> T5 k a

we would get

type T5 :: forall k -> k -> Type

C5 :: forall k (a :: k). Proxy a -> T5 k a

data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a

Rejected, like T6. If we revise to:

...

data T6 k (a :: k) where C6 :: forall {k} (a::k). Proxy a -> T6 k a

we get

type T6 :: forall k -> k -> Type

C6 :: forall {k} (a::k). Proxy a -> T6 k a

I've updated the proposal itself to include these examples.

Does this help to clarify?

Richard

On May 25, 2018, at 1:56 PM, Iavor Diatchki wrote:

Hello,

well, I thought that Richard was going to write a new proposal based on the feedback here, but it sounds like he is planning to revise #99, and then write a separate new one. I guess we should discuss the proposal again once the changes are in. I would encourage Richard to add some text and examples to clarify exactly what's in the proposal and what's not, and how things are supposed to work. Here are some examples, for which it would be illuminating (to me) to see the types/kinds of all names introduced.

data T1 a = C1 a

data T2 (a :: k) = C2 { f2 :: Proxy a }

data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a

data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a

data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a

data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a

-Iavor

On Fri, May 25, 2018 at 2:02 AM Simon Peyton Jones wrote:

I’m keen to get #99 into GHC in some form.

My motivation (which could be a fourth bullet in the proposal) is that it should be possible for a programmer to write a fully-explicit type signature for anything GHC can infer. But currently we can’t. For typeRep1 GHC infers the signature shown for typeRep3; but we can’t write it down.

based on the discussion so far, it seems that #99 in its current form might not be exactly what we want

Can you summarise the reasons it might not be exactly what we want?

Simon

*From:* ghc-steering-committee *On Behalf Of *Richard Eisenberg *Sent:* 24 May 2018 21:17 *To:* Iavor Diatchki *Cc:* ghc-steering-committee@haskell.org; Joachim Breitner < mail@joachim-breitner.de> *Subject:* Re: [ghc-steering-committee] Discussion on proposal #99: forall {k}

I do plan on turning Joachim's recent suggestion into a separate proposal, and then to modify #99. But the modification would remove only the bit about classes, not the feature overall. I don't have time to do this now, though -- will do next week.

Richard

On May 24, 2018, at 1:54 PM, Iavor Diatchki wrote:

Hello,

based on the discussion so far, it seems that #99 in its current form might not be exactly what we want, so I'd say that we should reject it for the moment. Overall, I agree that it would be nice to come up with a consistent notation for things that are currently happening in GHC but we can't write, so perhaps we could revisit this with a revised proposal at a later time?

-Iavor

On Sat, May 5, 2018 at 8:48 PM Joachim Breitner wrote:

Hi,

Am Mittwoch, den 02.05.2018, 16:10 -0400 schrieb Richard Eisenberg:

...

Joachim, you are always a fount of interesting ideas.

...

On May 2, 2018, at 2:51 PM, Joachim Breitner wrote:

class C k (a : k) where meth :: a meth :: forall {k} a. C k a -> k -> Constraint

I think this is brilliant. But not only for this proposal! Imagine this:

class Num a where fromInteger :: Integer -> a

fromInteger :: Integer -> forall a. Num a => a

If we do that, then #129 is essentially solved, at no further cost to anyone. (Note that in all Haskell98-style code, no one will ever be able to notice the changed type of fromInteger.)

This approach also allows for the possibility of reordering quantified type variables for Haskell98-style constructors, if anyone should want to do it.

And it allows for updated types (including quantified variable ordering, etc.) for record selectors.

And it allows (maybe?) for giving good types to GADT record selectors:

data X a where Foo :: { bar :: Int } -> X Int Quux :: { bar :: Bool } -> X Bool bar :: X a -> a

GHC currently rejects the declaration for X, but it could be accepted if only we could specify the correct type of bar. And now we can. I don't particularly want to cook up the typing rules here, but I don't think I'm totally crazy.

GADT record selectors aside, the rule for these could be that the top-level type signature must be equivalent w.r.t. the subtype relation with the original type signature. That is, if the new signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy enough to check for. The implementation would probably do a little worker/wrapper stunt.

I smell a new proposal… what does this mean for #99? Will you want to revise it?

Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/ https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Ca43c362fd18e4163aeba08d5c1b34be2%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636627898179266033&sdata=1cwPEVKXCcP3DuCHXOFuA%2BbEBniRLjcKI%2BAZji5vR4Q%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee