Purescript Records and Row Type kind

Help
,
#1

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
#2

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