Coding style: Using StandaloneKindSignatures in GHC

[Oleg Grenrus]

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-Tc-Utils-TcType.html#t:Type
[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 at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>