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 have some rules that my coworker wrote for records that I can just use but the problem here is extensibility 😞
2
Replying to
IIRC think the Pollack paper has some rules but they might not be compatible with your stuff… I don't think they are row based, but I think they are extensible.