[ChadNauseam]

I like ChatGPT’s answer better than yours. Rust’s cost generics and C++ aren’t dependent types in any sense. And saying “the type of one variable can depend on the value of another” is vague but a good intuition pump.

Since I guess we’re doing dependent types explanations I’ll give it a go. Dependent types extend a type system with two new type thingies: 2-tuples where the type of the second element depends on the value of the first, and functions where the type of the function’s return value depends on the value that was passed to it.

[howenterprisey]

Ha! Looks like I was wrong and confusing refinement types with dependent types: https://cs.stackexchange.com/a/21733 (unless of course this person is also confidently wrong, heh)

> Dependent types are types which depend on values in any way. A classic example is "the type of vectors of length n", where n is a value. Refinement types, as you say in the question, consist of all values of a given type which satisfy a given predicate. E.g. the type of positive numbers. These concepts aren't particularly related (that I know of). Of course, you can also reasonably have dependent refinement types, like "type of all numbers greater than n".