> A (data) type is a set, and a value is an element in that set.
Nope, a type is not a set. Type theories are separate formal systems designed to be (among other things) computationally aware alternatives to set theory, and they are defined by "terms", "types" and "rewrite rules". The whole point of a dependent type theory is to be able to encode things like sets and propositions in the same formal system.
The rest of your comment is wildly off based on this misunderstanding.
What the GP was probably referring to is the persepctive of dependent types from the lambda cube, where you have three different extensions to simply typed lambda calculus's regular functions from value to value:
1. Parametric polymorphism, which are functions from type to value
2. Type operators, which are functions from type to type
3. Dependent types which are fubnction from *value to type*
Since dependent types allows functions from value to type, it kinda erases the artificial barrier between type-level and value-level. In reality it doesn't really erase it, somuch as replace it with an infinte hierarchy of levels to avoid Girrard's paradox.
Nope, a type is not a set. Type theories are separate formal systems designed to be (among other things) computationally aware alternatives to set theory, and they are defined by "terms", "types" and "rewrite rules". The whole point of a dependent type theory is to be able to encode things like sets and propositions in the same formal system.
The rest of your comment is wildly off based on this misunderstanding.
What the GP was probably referring to is the persepctive of dependent types from the lambda cube, where you have three different extensions to simply typed lambda calculus's regular functions from value to value:
Since dependent types allows functions from value to type, it kinda erases the artificial barrier between type-level and value-level. In reality it doesn't really erase it, somuch as replace it with an infinte hierarchy of levels to avoid Girrard's paradox.