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.
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.
2