First you have to solve the not so nice name clash of GHC...Type [1] and Data.Kind.Type [2] The former is all over the GHC code base, the latter is needed for (most) kind signatures, as * is not an option. - Oleg [1]: https://downloads.haskell.org/ghc/latest/docs/html/libraries/ghc-9.0.1/GHC-T... [2]: https://hackage.haskell.org/package/base-4.15.0.0/docs/Data-Kind.html#t:Type On 18.5.2021 21.18, Hécate wrote:

After reading this proposal, I agree that StandaloneKindSignatures ought to be encouraged in the codebases, and I vote that we mention them in the coding style¹.

Cheers, Hécate

——— ¹ https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/coding-style

Cheers, Hécate.

Le 18/05/2021 à 19:58, Baldur Blöndal a écrit :

...

Discussion to permit use of StandaloneKindSignatures in the GHC coding style guide. I believe it increases the clarity of the code, especially as we move to fancier kinds.

It is the only way we have for giving full signatures to type synonyms, type classes, type families and others. An example:

     type Cat :: Type -> Type      type Cat ob = ob -> ob -> Type

     type  Category :: forall ob. Cat ob -> Constraint      class Category cat where        id :: cat a a ..

     type Proxy :: forall k. k -> Type      data Proxy a = Proxy

     type Some :: forall k. (k -> Type) -> Type      data Some f where        Some :: f ex -> Some f

     -- | The regular function type      type (->) :: forall {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}. TYPE1 rep1 -> TYPE rep2 -> Type      type (->) = FUN 'Many

This is in line with function definitions that are always given a top-level, standalone type signature (1) and not like we currently define type families/synonyms (2) by annotating each argument or not at all. Using -XStandaloneKindSignatures (3) matches (1)

     -- (1)      curry :: ((a, b) -> c) -> (a -> b -> c)      curry f  x y = f (x, y)

     -- (2)      type Curry (f :: (a, b) -> c) (x :: a) (y :: b) =  f '(x, y) :: c

     -- (3)      type Curry :: ((a, b) -> c) -> (a -> b -> c)      type Curry f x y = f '(x, y)

It covers an edgecase that `KindSignatures` don't. The only way for deriving to reference datatype arguments is if they are quantified by the declaration head -- `newtype Bin a ..`. StandaloneKindSignatures allows us to still provide a full signature. We could write `newtype Bin a :: Type -> Type` without it but not `newtype Bin :: Type -> Type -> Type`

     type    Bin :: Type -> Type -> Type      newtype Bin a b = Bin (a -> a -> b)        deriving (Functor, Applicative)        via (->) a `Compose` (->) a

Let me know what you think _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Le 18/05/2021 à 20:41, Richard Eisenberg a écrit :

On the other hand, I'm in support of encouraging the use of a standalone kind signature for type declarations where at least one parameter of the datatype does not have kind Type. In fact, I'd be in support of mandating (such as we can) such a standalone kind signature in our style guide. The cases where at least one parameter of a datatype does not have kind Type are the places we need the extra information. This is indeed quite reasonable. I will follow you on that point.

-- Hécate ✨ 🐦: @TechnoEmpress IRC: Uniaika WWW: https://glitchbra.in RUN: BSD

Silly question: when will stand alone kind sigs speed up type checking phase of compilation? Cause that would be an interesting argument in favor :) On Fri, May 21, 2021 at 2:11 AM Baldur Blöndal wrote:

...

encouraging the use of a standalone signature for type declarations where at least one parameter of the datatype does not have kind Type.

So Dict, Eq both get a sig but Fix and Either do not?

type Dict :: Constraint -> Type type Eq :: Type -> Constraint type Fix :: (Type -> Type) -> Type

It's sensible to exclude tired tropes like `Type` and `Type -> Type` but higher-order functors (like Fix) warrant a signature.

Caveat: The kind of type synonyms, type families and data families is not necessarily determined by counting the syntactic arguments of X like for a `data' declaration as Y could be a type, a functor, a bifunctor..

type X = Y _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

On Fri, May 21, 2021 at 2:11 AM Baldur Blöndal wrote:

...

encouraging the use of a standalone signature for type declarations where at least one parameter of the datatype does not have kind Type.

So Dict, Eq both get a sig but Fix and Either do not?

type Dict :: Constraint -> Type type Eq :: Type -> Constraint type Fix :: (Type -> Type) -> Type

That's not how I understand Richard's criteria. Dict and Fix have non-Type parameters (Dict has a Constraint parameter, and Fix has a (Type -> Type) parameter. On the other hand, Eq and Either have only Types as parameters. This seems to match my intuition about when a kind signature might be helpful, as well as yours as far as I can tell from what you wrote. That's not to say I am advocating any kind of rule. As I'm not really involved in GHC development, I refrain from having any opinion. I just think you may have misread Richard's suggestion.

I’m good with those rules. Simon From: ghc-devs On Behalf Of Richard Eisenberg Sent: 21 May 2021 21:21 To: Chris Smith Cc: GHC developers Subject: Re: Coding style: Using StandaloneKindSignatures in GHC I agree with Chris here. Let me expand upon my counter-proposal: * A datatype declaration gets a standalone kind signature whenever at least one of its type arguments has a kind other than Type. * A class declaration gets a standalone kind signature whenever at least one of its type arguments has a kind other than Type.(*) * A closed type family always gets a standalone kind signature. * A type synonym gets a standalone kind signature whenever either at least one of its arguments has a kind other than Type or its result has a kind other than Type. (*) The class rule has an exception: if a class has a superclass constraint using Monad, Functor, Applicative, Foldable, or Traversable (or some other class whose name textually includes one of those names, such as MonadIO), we understand that the constrained variable must have kind Type -> Type. If that type variable is the only one without kind Type -> Type, then the standalone kind signature is optional. In cases other than those covered above, the standalone kind signature is optional, at the discretion of the programmer. This suggests that Dict gets a signature, Eq does not, Fix does, and Either does not. Richard On May 21, 2021, at 12:37 PM, Chris Smith mailto:cdsmith@gmail.com> wrote: On Fri, May 21, 2021 at 2:11 AM Baldur Blöndal mailto:baldurpet@gmail.com> wrote:

encouraging the use of a standalone signature for type declarations where at least one parameter of the datatype does not have kind Type.

So Dict, Eq both get a sig but Fix and Either do not? type Dict :: Constraint -> Type type Eq :: Type -> Constraint type Fix :: (Type -> Type) -> Type That's not how I understand Richard's criteria. Dict and Fix have non-Type parameters (Dict has a Constraint parameter, and Fix has a (Type -> Type) parameter. On the other hand, Eq and Either have only Types as parameters. This seems to match my intuition about when a kind signature might be helpful, as well as yours as far as I can tell from what you wrote. That's not to say I am advocating any kind of rule. As I'm not really involved in GHC development, I refrain from having any opinion. I just think you may have misread Richard's suggestion.

The CLC owns base, with final say coming down to listed maintainers. Though in practise, it ends up being a collective opinion of the CLC + GHC HQ that drives decisions, rather than one person. On Mon, May 24, 2021, 15:28 Oleg Grenrus wrote:

To clarify, are you suggesting guidelines for GHC **and** base-library?

I'm puzzled about ownership of base. Who have a final word about it? ghc-devs, libraries@haskell.org, CLC, chessai alone, whoever is first?

- Oleg On 21.5.2021 23.21, Richard Eisenberg wrote:

I agree with Chris here.

Let me expand upon my counter-proposal:

* A datatype declaration gets a standalone kind signature whenever at least one of its type arguments has a kind other than Type. * A class declaration gets a standalone kind signature whenever at least one of its type arguments has a kind other than Type.(*) * A closed type family always gets a standalone kind signature. * A type synonym gets a standalone kind signature whenever either at least one of its arguments has a kind other than Type or its result has a kind other than Type.

(*) The class rule has an exception: if a class has a superclass constraint using Monad, Functor, Applicative, Foldable, or Traversable (or some other class whose name textually includes one of those names, such as MonadIO), we understand that the constrained variable must have kind Type -> Type. If that type variable is the only one without kind Type -> Type, then the standalone kind signature is optional.

In cases other than those covered above, the standalone kind signature is optional, at the discretion of the programmer.

This suggests that Dict gets a signature, Eq does not, Fix does, and Either does not.

Richard

On May 21, 2021, at 12:37 PM, Chris Smith wrote:

On Fri, May 21, 2021 at 2:11 AM Baldur Blöndal wrote:

...

...

encouraging the use of a standalone signature for type declarations where at least one parameter of the datatype does not have kind Type.

So Dict, Eq both get a sig but Fix and Either do not?

type Dict :: Constraint -> Type type Eq :: Type -> Constraint type Fix :: (Type -> Type) -> Type

That's not how I understand Richard's criteria. Dict and Fix have non-Type parameters (Dict has a Constraint parameter, and Fix has a (Type -> Type) parameter. On the other hand, Eq and Either have only Types as parameters. This seems to match my intuition about when a kind signature might be helpful, as well as yours as far as I can tell from what you wrote.

That's not to say I am advocating any kind of rule. As I'm not really involved in GHC development, I refrain from having any opinion. I just think you may have misread Richard's suggestion.

_______________________________________________ ghc-devs mailing listghc-devs@haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

I'm all for "encourage" but not keen on "require". Simon | -----Original Message----- | From: ghc-devs On Behalf Of Hécate | Sent: 18 May 2021 19:18 | To: ghc-devs@haskell.org | Subject: Re: Coding style: Using StandaloneKindSignatures in GHC | | After reading this proposal, I agree that StandaloneKindSignatures ought | to be encouraged in the codebases, and I vote that we mention them in the | coding style¹. | | Cheers, | Hécate | | ——— | ¹ | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab. | haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fcommentary%2Fcoding- | style&data=04%7C01%7Csimonpj%40microsoft.com%7C526d76f0fe6f4bfad5b208 | d91a297bd3%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63756958777303339 | 3%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1 | haWwiLCJXVCI6Mn0%3D%7C3000&sdata=xUV24DTEWYImjevJtWxK1hAB6QI0gX9dqvXm | 81jLOPo%3D&reserved=0 | | Cheers, | Hécate. | | Le 18/05/2021 à 19:58, Baldur Blöndal a écrit : | > Discussion to permit use of StandaloneKindSignatures in the GHC coding | > style guide. I believe it increases the clarity of the code, | > especially as we move to fancier kinds. | > | > It is the only way we have for giving full signatures to type | > synonyms, type classes, type families and others. An example: | > | > type Cat :: Type -> Type | > type Cat ob = ob -> ob -> Type | > | > type Category :: forall ob. Cat ob -> Constraint | > class Category cat where | > id :: cat a a .. | > | > type Proxy :: forall k. k -> Type | > data Proxy a = Proxy | > | > type Some :: forall k. (k -> Type) -> Type | > data Some f where | > Some :: f ex -> Some f | > | > -- | The regular function type | > type (->) :: forall {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}. | > TYPE1 rep1 -> TYPE rep2 -> Type | > type (->) = FUN 'Many | > | > This is in line with function definitions that are always given a | > top-level, standalone type signature (1) and not like we currently | > define type families/synonyms (2) by annotating each argument or not | > at all. Using -XStandaloneKindSignatures (3) matches (1) | > | > -- (1) | > curry :: ((a, b) -> c) -> (a -> b -> c) | > curry f x y = f (x, y) | > | > -- (2) | > type Curry (f :: (a, b) -> c) (x :: a) (y :: b) = f '(x, y) :: c | > | > -- (3) | > type Curry :: ((a, b) -> c) -> (a -> b -> c) | > type Curry f x y = f '(x, y) | > | > It covers an edgecase that `KindSignatures` don't. The only way for | > deriving to reference datatype arguments is if they are quantified by | > the declaration head -- `newtype Bin a ..`. StandaloneKindSignatures | > allows us to still provide a full signature. We could write `newtype | > Bin a :: Type -> Type` without it but not `newtype Bin :: Type -> Type | > -> Type` | > | > type Bin :: Type -> Type -> Type | > newtype Bin a b = Bin (a -> a -> b) | > deriving (Functor, Applicative) | > via (->) a `Compose` (->) a | > | > Let me know what you think | > _______________________________________________ | > ghc-devs mailing list | > ghc-devs@haskell.org | > https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail. | > haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=04%7C01 | > %7Csimonpj%40microsoft.com%7C526d76f0fe6f4bfad5b208d91a297bd3%7C72f988 | > bf86f141af91ab2d7cd011db47%7C1%7C0%7C637569587773033393%7CUnknown%7CTW | > FpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6 | > Mn0%3D%7C3000&sdata=Dc5Xbl2YJ%2BWmstt2z289UAzX9s%2BWJ5RuH84V2AbxJY | > c%3D&reserved=0 | | -- | Hécate ✨ | 🐦: @TechnoEmpress | IRC: Uniaika | WWW: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fglitchb | ra.in%2F&data=04%7C01%7Csimonpj%40microsoft.com%7C526d76f0fe6f4bfad5b | 208d91a297bd3%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63756958777304 | 3386%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6 | Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=KqNL0D9zC%2FiOORPEUqChk%2FTUxkekq | vxyZuyokFjcxMI%3D&reserved=0 | RUN: BSD | | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.has | kell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc- | devs&data=04%7C01%7Csimonpj%40microsoft.com%7C526d76f0fe6f4bfad5b208d | 91a297bd3%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637569587773043386 | %7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1h | aWwiLCJXVCI6Mn0%3D%7C3000&sdata=yuGMW58YP7Grt4TrjtL5dahu0vSOP%2BYmV9I | zxLvrRxI%3D&reserved=0