Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
@TheMatten let's take this to another topic.
The system how it is implemented in purescript does have some formal definition with a paper by Leijen, but there are several issues the biggest being that Core's type system is dependently typed, has kind polymorphism and is not the toy type system that Leijen uses.
In my thesis I developed the idea further, combining it with type indexed rows by meijer to create rows that are polykinded in the key and the value.
I just have the issue of embedding these in the complex foundation that is System FC these days (after TypeInType, ie kind equalities)