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
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
This Tweet is from a suspended account. Learn more
Replying to
Yeah, it seems hard. Really wish it was easier to program with ‘graphs’ of terms and types. Where nodes may or may not have dependencies between them.
Replying to
Dunno if contextual type theory is at all helpful here? Need to get around to reading the Cocon paper at some stage! arxiv.org/abs/1901.03378