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 :(
Replying to
I have some rules that my coworker wrote for records that I can just use but the problem here is extensibility 😞
2
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Show replies
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