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)
Also I think the labels should somehow be namespaced, not like type-level strings - like, they should work well in a modular way in 'the large'. Perhaps along the lines of how Clojure does it, but I dunno.
2
I guess that could work! One issue though is how partial application might work, but perhaps there could be special rules for that.
1
Show replies