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
I also want named arguments too, using these rows. Where the following applications are equivalent (not sure about the syntax though):
List (elem = Int) (max = 5)
List (elem = Int, max = 5)
List (max = 5) (elem = Int)
List (max = 5, elem = Int)
2
why not List {elem = Int, max = 5} ?
1
I guess that could work! One issue though is how partial application might work, but perhaps there could be special rules for that.
1
Don't worry! {...} is also a type, and its kind is *.
In fact, row types are very close to tuple types.
1
Ahhh, I thought it was a record there. was using `()` like in purescript to distinguish it as a 'row'. Are you not distinguishing rows at the kind level? Ie. `{...} : Type` as opposed to `{...} : Row`?
You thought it was a record value, while I thought it was a record type. As we have {max=5}, it's already dependent type, so yours might be more flexible..