The word for types depending on a value is dependent typing. Eg lists of size N, numbers in a range, are all what you call dependent types. Idris - cosmeticall

The word for types depending on a value is dependent typing. Eg lists of size N, numbers in a range, are all what you call dependent types. Idris - cosmetically looks like haskell, Lean and a bunch of other languages have this feature https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type