wait, we don’t have “standard” results on extensible records/row types for dependently-type languages? is Morris and McKinna 2019 our best guess so far?
Conversation
There's Randy Pollack's "Dependently Typed Records in Type Theory", which is kind of similar, and implemented in Agda here:
- agda.github.io/agda-stdlib/RE
- agda.github.io/agda-stdlib/Da
It's a bit goofy, but I kind of love it anyway.
1
Not sure if it supports the kind extensibility you want though, and it's implemented using datatypes, as opposed to being built-in, so looks kind of clunky, and is probably annoying to use in practice compared to natively supported row+record types :(
2
I also have always wanted to know if there is such thing as dependent extensible variants, and dependent extensible effects (other things that can use rows), but I have not idea what those would mean