Add a section on `StandaloneKindSignatures` to the code style guide
Clarification and motivation
We don't have a style guide for using StandaloneKindSignatures
, which occasionally leads to short-lived arguments in reviews. Perhaps it's about time we decided on something for the sake of consistency.
Standalone signatures are strictly more useful if the type in question is polykinded, unless the kind variable is used in the definition (see below).
For mono-kinded types, they're arguably still more readable than inline kind signatures, but that may depend on the context.
There is, however, an unfortunate quirk: kind variables bound in the standalone type signature do not scope over the definition. Hence, it's not always possible to eschew in-line kind signatures in the definition, even in the presence of the standalone kind signature.
Here's a concrete proposal:
A section ### Kind signatures
is added at the end of ## General guidelines
section with the following content:
- You MUST add a standalone kind signature for poly-kinded types.
- You SHOULD add a standalone kind signature for poly-kinded type classes.
- You SHOULD mark kind variables inferred in the type class signature, if the class has methods, i.e.
type MyClass :: forall {k}. ...
. - You SHOULD add a standalone kind signature for mono-kinded types, unless the kind signature is trivial, i.e. has the form
Type
,Type -> Type
,Type -> Type -> Type
, etc. - You MAY use in-line kind signatures for mono-kinded datatypes and type families.
- You MAY eschew kind signatures for newtypes and simple type synonyms.
- You NEED NOT add a standalone kind signature for a
data
ornewtype
declaration using GADT syntax, if it includes its own kind signature (i.e.data Foo :: ... -> Type where
) - You SHOULD use standalone kind signature with declarations using GADT syntax if the parameters can be given names that reveal information beyond their kinds.
Remember that the kind variables bound by an outermost forall in a standalone kind signature scope only over the kind in that signature, not over the corresponding declaration, hence
class C (a :: k) where
m :: Proxy k -> Proxy a -> String
is NOT equvialent to
type C :: forall k. k -> Constraint
class C a where
m :: Proxy k -> Proxy a -> String
Examples:
type SizedList :: Nat -> Type -> Type
type SizedList n a = SizedList' (ToPeano n) a
-- preferred, SHOULD add standalone kind signature for nontrivial mono-kinded types
---
type SizedList n a = SizedList' (ToPeano n) a
-- acceptable, MAY eschew kind signatures for simple type synonyms
---
type SizedList (n :: Nat) a = SizedList' (ToPeano n) a
-- acceptable, MAY use in-line kind signatures for mono-kinded type families
type family RequireLongerThan' (l :: [k]) (a :: Nat) :: Constraint where
-- NOT acceptable, MUST add a standalone kind signature for poly-kinded types
---
type RequireLongerThan' :: [k] -> Nat -> Constraint
type family RequireLongerThan' l a where
-- required, MUST add a standalone kind signatures for poly-kinded types
data FieldAlias (alias :: k) (p :: FieldRefTag) = FieldAlias (Proxy alias)
-- NOT acceptable, MUST add a standalone kind signature for poly-kinded types
---
type FieldAlias :: k -> FieldRefTag -> Type
data FieldAlias alias p = FieldAlias (Proxy alias)
-- required, MUST add a standalone kind signature for poly-kinded types
class ReifyList (c :: k -> Constraint) (l :: [k]) where
reifyList :: (forall a. c a => Proxy a -> r) -> [r]
-- acceptable, but SHOULD add a standalone kind signature for poly-kinded type classes
---
type ReifyList :: forall {k}. (k -> Constraint) -> [k] -> Constraint
class ReifyList c l where
-- note kind signatures are not required in the definition because k is unused
reifyList :: (forall a. c a => Proxy a -> r) -> [r]
-- preferred, SHOULD add a standalone kind signature for poly-kinded type classes,
-- SHOULD mark kind variables _inferred_ in the type class signature.
newtype FieldConstructor st field =
FieldConstructor (Instr (ToTs' st) (ToT field ': ToTs' st))
-- acceptable, MAY eschew kind signatures for newtypes and simple type synonyms.
---
type FieldConstructor :: [k] -> Type -> Type
newtype FieldConstructor st field =
FieldConstructor (Instr (ToTs' st) (ToT field ': ToTs' st))
-- preferred, MUST add a standalone kind signature for poly-kinded types.
---
newtype FieldConstructor (st :: [k]) (field :: Type) =
FieldConstructor (Instr (ToTs' st) (ToT field ': ToTs' st))
-- NOT acceptable, MUST add a standalone kind signature for poly-kinded types.
data KnownList :: [k] -> Type where
-- acceptable, NEED NOT add a standalone kind signature for a
-- `data` or `newtype` declaration using GADT syntax, if it
-- includes its own kind signature
---
type Append :: [k] -> [k] -> [k] -> Type
data Append beginning middle end where
-- acceptable, SHOULD use standalone kind signature with
-- declarations using GADT syntax if the parameters can be
-- given names that reveal information beyond their kinds.
---
data KnownList (xs :: [k]) :: Type where
-- NOT acceptable, MUST add a standalone kind signature for
-- poly-kinded types, and no exceptions apply.
Acceptance criteria
- The exact wording is decided.
-
code-style.md
is updated accordingly.