Purescript Records and Row Type kind

Hi,
I’m really knew to functional programming and have only done minimal research into category and type theory as most of it completely goes over my head. However Rows confuse me. So i kinda just want to state some things and please correct me if I’m wrong.

  1. a kind is a type of types sort of
  2. So the kind of Record is Row Type -> Type where Row Type takes a type of kind Type and makes a kind of Row Type. but how does the Record type constructor take multiple Row Types. or is a Row the comna separated lists of types.

The purescript markdown document still confuses me. Thanks

1 Like

Note that this is specific to the upcoming 0.14 release (if you are reading documentation in master).

The Record type constructor does not take multiple Row Types. Record takes a single type-argument with the kind Row Type. (foo :: Bar, ...) is type-level-literal syntax for constructing a type with the kind Row Type, similar to how [ 1, 2, ... ] syntax at the value-level-literal syntax for constructing a value of type Array Int.

In 0.14, the Row constructor is polymorphic, in the same way that Array can be polymorphic. At the value level, you can do ["foo"] :: Array String or [true] :: Array Boolean, and at the type level you can do (foo :: "Foo") :: Row Symbol or (foo :: Array) :: Row (Type -> Type) to construct a row where the members have a different kind than Type.

Value-level things always have kind Type. This does not necessarily mean they have a run-time representation. That is, anything that exists at runtime is of kind Type, but not everything that has kind Type necessarily exists at runtime. Since Record takes a type argument with the kind Row Type, that means it is indexed by a row of labels to types that are potentially inhabited at runtime.

2 Likes