This is an interesting post on /r/dependent_types that talks about expressing row polymorphism using groupoids in cubical type-theory - not sure I understand much of it but it seems intriguing! 😅
Conversation
Replying to
I've wondered in the past if you could have 'dependent rows' - ie. where entries in the row can have dependencies between them. A potential use case would be row-polymorphic modules, or for metaprogramming with modules. 🤔
2
2