Anyone knows a paper on implementing row polymorphism for records (and variants) with type predicates? All the papers I've found are based on giving record rows a different kind, but that leads to annoying issues for me.

What I'm envisioning is, a type class `Record`, and then two types `EmptyRecord` and `RecordExtend label field tail` with rules `Record EmptyRecord` and `Record tail => Record (RecordExtend label field tail)`. Then whenever you need to enforce that something is a record (e.g. when constructing one or accessing a field) you just add a predicate on the type.

I'd love to see if anyone has attempted to formalise this idea though. The fact that I haven't found anything makes me wonder whether it might be unsound or bad.

#typetheory #rowpolymorphism #polymorphism #records #variants