is there anyone working on type-level records (dependent row types?), things like this silly example, or am I just badly reinventing something
list : List Nat { max = 5 }
list = [1, 4, 5]
here List has kind
(a : Type) -> { max : a } -> Type
Conversation
That seems doable with just regular dependent types. What I really want is dependent row types! With nice swap rules so you don't have to worry about the order of the fields so much.
2
5
isn't a general value belonging to a dependent record type of this nature "just" a bunch of records that you can get by toposorting the labels?
1
Yeah, I think so! Things might become harder if you want operations for row extension, field lookup, etc.
1
This is whI was thinking that maybe contextual type theory might help
Quote Tweet
Replying to @brendanzab @rob_rix and @mrkgrnao
I wonder if using something like contextual type theory could make things easier, but I dunno.