I also observe that the go-to example of why depen...

# language-proposals

[mikehearn]

I also observe that the go-to example of why dependent types are useful is always Vector<N>, but usually I don't want to specify exactly how many elements a list has in the type, but being able to express non-emptyness (wish English had a short word for this) would have been concretely useful.

[pdvrieze]

I'd rather like such advanced type system. Perhaps value types will get us part of the way. At the same time these kinds of types can create all kinds of complexity (baffles weaker programmers).

My ideal solution for the size, or stream (and other) problem is the notion of a type having a compile time state. Methods could state their effect on the state and put requirements on the state (an undefined state must be possible as well).

It is possible to simulate compile time state with interfaces that expose only parts of the API on their return value, but it is very unsatisfactory (it requires setting the value (and type) on the containing variables).