Kinds and Do-Syntax

Kinds-and-do-syntax.md

Kinds

In PureScript there are types of different kinds. Kinds are types for types. For example Int has kind Type, and we write it as Int :: Type. You can ask for the kind of a type in purs psci

> :k Int
Type

Type constructors take types to other types. For example Array (which still needs another type to form a type a value could have, like Array Int):

> :k Array
Type -> Type

> :k Array Int
Type

The feature that enables PureScript's records is row types. Rows have their own kind:

> :k (hi :: Int, wow :: Array String)
# Type

(notice that I'm using parens not braces, so this is just a row type, no record)

The # is the kind of rows, and it's a kind constructor. It needs another kind to form a full kind, which is why we can't have rows with types of different kinds:

> :k (hi :: Int, wow :: Array)

  Could not match kind

    Type -> Type

  with kind

    Type

Now let's turn to records. The curly brace syntax in PureScript is syntactic sugar for applying the Record constructor to a row type, meaning that:

{ hi :: Int, wow :: Array Int }

expands to:

Record (hi :: Int, wow :: Array Int)

Now what's the kind of Record?

:k Record
# Type -> Type

It's a type constructor of kind "Row of Types to Type"!

The kind of Monad

When you are using do-syntax you are using syntactic sugar for the Bind typeclass, which is usually used in combination with an Applicative, which then forms a Monad.

Now the Monad type class is defined for types of kind Type -> Type. See https://pursuit.purescript.org/packages/purescript-prelude/4.1.1/docs/Control.Monad#t:Monad

It doesn't really say it anywhere explicitly (because the inference works it out), but if you check out the functions that are defined over all monads, you can see that the m parameter is usually applied to another type argument, thus Type -> Type.

Do-syntax

In do-syntax the compiler expects every line that starts at the indentation level directly after do to have type: m a, where m is the Monad that has been picked for the do-block. For example:

hiho = do
  Console.log "hi"
  x <- readLine
  Console.log x

The type of Console.log "hi" is: Effect Unit, and the compiler will follow these steps to figure out what's the relevant Monad here.

1. Unit is the a in m a, so strip it off.
2. Effect is our Monad
3. done.

The compiler will now check that every subsequent line also has type Effect a for some a. (Btw if you run into errors with the Discard typeclass, that happens if that a is not Unit and you're still discarding it.)

Now what happens if I put a record literal on its own line?

hiho = do
  Console.log "hi"
  { hello: 1 }
  
  Could not match type

    Record

  with type

    Effect

Oops.

When the compiler tried to apply the same transformation to Record (hello :: Int), it stripped off the (hello :: Int) part and was left with Record. When it now tries to match the remaining Record with Effect it returns an error, because these two types can not be made equal.