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.
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
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
Like, unless there are dependencies between them? { tag : Type, value : Con tag } sort of sigma type thing? It would be neat to be order-agnostic everywhere else…
2
1
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
Show replies