4 ms·

They fact that they can be conflated doesn't mean that they should.

by Retra 8y ago

gnulinux 8y ago
No, they really should be since (1) it gives more guarantees about your program in compile-time and (2) lets you express more assumptions about your program to your compiler (3) for free.
- Retra 8y ago
  Perhaps you should instead produce a counter-example, because as far as I can tell nothing you've said is actually true.
  - andrewflnr 8y ago
    Their (3) is the only debatable point (aside from the inherent subjectivity of statements involving the word "should", which applies equally to you), since dependently typed languages tend to put a lot of the burden of proof onto the programmer. The other points are practically true by definition.
    - Retra 8y ago
      If types and values were identical, there would be no need for a runtime in any program, and that is simply not possible. There are many things which can only be modeled as values and not as types. (Randomness, for instance.) Dependently typed languages allow a little bit of value-level feedback into the type system, but they certainly do not eliminate the distinction. And certainly none of this is free. Indirection has costs, and trying to model the entire behavior of a program in a compile-time system is going have costs. Some of those costs will push solvable problems into an unsolvable state, and then things break down. (For another example of this: software can try to emulate hardware, but there are things that hardware can do that software cannot and vice versa, so it wouldn't make sense to say they are identical.) >The other points are practically true by definition. "More guarantees" and "more assumptions" are not definable terms. You can't count the number of theorems that need to be true for some model to be accurate.
      - andrewflnr 8y ago
        You seem to be operating from an overly narrow perspective. Type theories were invented for mathematical logic and only co-opted for programming later. It doesn't make sense to try to prove things about type systems by referring to a runtime. The rest of your objections show similar misunderstandings of the question. While I said myself a dependent type system is not free, its costs have nothing to do with "indirection", whether you mean type system complication or pointer chasing (the latter is more likely to be reduced). Randomness is about computational purity, which is nearly orthogonal to the expressiveness of your type system. I'm not completely sure what you're trying to say about hardware, not I'm pretty sure it's a red herring, at least from the theoretical perspective relevant to characterizing dependent types. The Wikipedia article on dependent types is a pretty decent survey: https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
        kazinator 8y ago
        "Dependent types were created to deepen the connection between programming and logic. {clarification needed}"
        Retra 8y ago
        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.

They fact that they can be conflated doesn't mean that they should.

by Retra 8y ago

They fact that they can be conflated doesn't mean that they should.

No, they really should be since (1) it gives more guarantees about your program in compile-time and (2) lets you express more assumptions about your program to your compiler (3) for free.

Retra 8y ago
Perhaps you should instead produce a counter-example, because as far as I can tell nothing you've said is actually true.
- andrewflnr 8y ago
  Their (3) is the only debatable point (aside from the inherent subjectivity of statements involving the word "should", which applies equally to you), since dependently typed languages tend to put a lot of the burden of proof onto the programmer. The other points are practically true by definition.
  - Retra 8y ago
    If types and values were identical, there would be no need for a runtime in any program, and that is simply not possible. There are many things which can only be modeled as values and not as types. (Randomness, for instance.) Dependently typed languages allow a little bit of value-level feedback into the type system, but they certainly do not eliminate the distinction. And certainly none of this is free. Indirection has costs, and trying to model the entire behavior of a program in a compile-time system is going have costs. Some of those costs will push solvable problems into an unsolvable state, and then things break down. (For another example of this: software can try to emulate hardware, but there are things that hardware can do that software cannot and vice versa, so it wouldn't make sense to say they are identical.) >The other points are practically true by definition. "More guarantees" and "more assumptions" are not definable terms. You can't count the number of theorems that need to be true for some model to be accurate.
    - andrewflnr 8y ago
      You seem to be operating from an overly narrow perspective. Type theories were invented for mathematical logic and only co-opted for programming later. It doesn't make sense to try to prove things about type systems by referring to a runtime. The rest of your objections show similar misunderstandings of the question. While I said myself a dependent type system is not free, its costs have nothing to do with "indirection", whether you mean type system complication or pointer chasing (the latter is more likely to be reduced). Randomness is about computational purity, which is nearly orthogonal to the expressiveness of your type system. I'm not completely sure what you're trying to say about hardware, not I'm pretty sure it's a red herring, at least from the theoretical perspective relevant to characterizing dependent types. The Wikipedia article on dependent types is a pretty decent survey: https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type
      - kazinator 8y ago
        "Dependent types were created to deepen the connection between programming and logic. {clarification needed}"
      - Retra 8y ago
        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.