I've been thinking about how 'First Class Types' feels like a much better name for 'Dependent Types' than 'Dependent Types'.
The fact that we can treat types as first-class objects seems of primary value, and the fact that they types arise as outputs of functions sometimes seems secondary.
The fact that we can treat types as first-class objects seems of primary value, and the fact that they types arise as outputs of functions sometimes seems secondary.
Comments
Relevant: https://en.wikipedia.org/wiki/Reification_(computer_science)