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.

Comments