When to use kind annotation?

Chat
#1

Why is a kind annotation suggested for V1 and V3, but not V2?

-- Suggests annotation:
-- type V1 :: forall k. (k -> Type) -> Type
type V1 c =
  { foo :: forall a. c a -> c a
  }

-- No annotation suggested
type V2 c =
  { foo :: forall a. c a -> c a
  , bar :: forall a. c a -> a
  }

-- Suggests annotation:
-- type V3 :: forall k. (k -> Type) -> Type
type V3 c =
  { foo :: forall a. c a -> c a
  , bar :: forall a. c a -> Int
  }

https://try.ps.ai/?gist=23e3fed95ffaec15bd9eb93737f6aa19

This is the compiler warning:

The inferred kind for the type declaration V1 contains polymorphic kinds.
Consider adding a top-level kind signature as a form of documentation.

1 Like
Why does `:kind` in the REPL throw error for `data T a f = T (a f)`?
#2

It warns whenever it infers a polymorphic kind. V2 does not suggest anything because the signature of bar fixes a :: Type since (->) :: Type -> Type -> Type. In the others, a is otherwise unconstrained and can be generalized. For example, c could be Record and a :: Row Type.

4 Likes
#3

Thanks for the explanation. I realized I had a few gaps in understanding. Here are some additional notes I made while reasoning through what’s going on in case anyone else is similarly confused.

An arrow -> in a type signature is the Function data constructor, which has a “kind” signature of Type -> Type -> Type. Note that these kind signature arrows are different than type signature arrows. Only the former means Function.

So then if we look at V2's bar :: forall a. c a -> a, we can fill-in the following:

 Type   ->   Type   ->   Type
(c a)           a        Function (c a) a

Looking at the second Type, we see that a has kind Type.
Looking at the first Type, we see that c a has kind Type, and since a was earlier determined to have kind Type, then c must have kind Type -> Type. This kind signature is straightforward (no kind polymorphism), and so the compiler doesn’t nag us for annotation. But we could still include the kind annotation if we wanted to: type V2 :: (Type -> Type) -> Type.

In V1 or V3, we can’t nail down the kinds of any a to simply Type. These as could be a variety of things, such as Type -> Type, Type -> Type -> ... -> Type, Row Type, etc.
Since c must accept any of these kinds of a, we use a kind variable k to indicate this “kind polymorphism” and describe the kind of c as forall k. (k -> Type). The compiler wants us to annotate declarations involving polymorphic kinds.

2 Likes
#4

Thanks a lot for the exposition, @milesfrain (and @natefaubion for the previous explanation, which i now think i understand!)

1 Like
#5

I don’t know if this is accurate, or at least I’m not totally sure what you mean to convey. I’d think of it like:

  • PureScript is two “languages”: The term-level language and the type-level language.
  • The type-level language is used to express the constraints of the term-level language.
  • The same type-level language is also used to express the constraints of itself (the type-level language).
  • The term-level language has reducible computation (lambdas) and constructors, both of which are typed using Function a b or a -> b. That is, data Foo = Bar Int introduces a constructor Bar :: Int -> Foo, which is typed using ->, but this doesn’t “compute” anything. It’s just symbolic data.
  • The type-level language only has constructors (what we call type-constructors). These constructors are still typed using Function or ->.
2 Likes