I don't know what you're trying to say. The point I am trying to refute is "the whole type-level and value-level is a false dichotomy", and the existence of dep

I don't know what you're trying to say. The point I am trying to refute is "the whole type-level and value-level is a false dichotomy", and the existence of dependent types do not support that claim, they only provide a narrow domain where the distinction is blurred. > Randomness is about computational purity, which is nearly orthogonal to the expressiveness of your type system. If types and values are to be considered identical, then random types should be just as useful as random values. They are not. That alone should indicate that values and types have a well-motivated distinction. Additionally, dependent types offer no additional capabilities, only convenience. Having a type defined in terms of a value communicates nothing more to a compiler than would a functionally equivalent assertion, though it would certainly be easier to use and work with in some situations. I'm not trying to say anything about dependent types here. I'm trying to say that the goal of producing a language which makes no distinction between type and value is neither useful nor possible.