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
Yeah, I was thinking something like that. Like a DAG or something in your types.
1
1
Or maybe not a DAG if you wanted something like insaneley dependent types 🙃
1
I wonder if using something like contextual type theory could make things easier, but I dunno.
I've been looking at Nanevski/Pientka recently (for metavariables), is that what you mean
1
1
You mean "A Modal Foundation for Meta-Variables" from 2003? I think there are a few interesting papers by those peeps (and Pfenning) - recommended "Contextual Modal Type Theory" to me recently for example!
1
Show replies