One can imagine a kind of "dependent with" type.
(x : S) & T x
lets you choose at runtime between a "raw" S and a "cooked" T whose type depends on what the S used to be. Both components may be *contemplated* but only one may exist at run time.
Conversation
Isn't this the dependent intersection type that's used in Cedille?
2
2
It does kind of remind me as well of that ‘dependent intersection’ thing that the NuPRL folks were using to describe dependent records… is that what Cedille uses? Only this ‘dependent with’ type has the constraint that you can only look at one component at runtime. 🤔
2
1