Conversation

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

4

1

9

Brendan Zabarauskas

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

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

Brendan Zabarauskas

Yeah, I was thinking something like that. Like a DAG or something in your types.

1

1

Brendan Zabarauskas

Or maybe not a DAG if you wanted something like insaneley dependent types 🙃

1

Brendan Zabarauskas

I wonder if using something like contextual type theory could make things easier, but I dunno.

1

1

1

I've been looking at Nanevski/Pientka recently (for metavariables), is that what you mean

1

1

Brendan Zabarauskas

Replying to

and

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!

8:46 AM · Jan 28, 2020Twitter Web App

Replying to

and

i'm talking about the latter, but i think i should look at the former too haha