7 ms·

Under HoTT's take on propositions as “types where any two inhabitants are equal”, “types as propositions” is even less general than “types as sets”. As I state

Under HoTT's take on propositions as “types where any two inhabitants are equal”, “types as propositions” is even less general than “types as sets”. As I stated in a comment on that gist, what types denote varies from one type system to another: https://gist.github.com/garybernhardt/122909856b570c5c457a6cd674795a9c?#gistcomment-1856634 https://gist.github.com/garybernhardt/122909856b570c5c457a6c...

naasking 10y ago
No one except mathematicians and type theorists are using HoTT, where every programmer in existence is using first-order and sometimes second-order logic. I think it should be obvious which is more appropriate if this is supposed to be an introduction. The idea that types express propositions in first- or second-order logic about a program one is writing is sufficiently general for every programmer to understand the proper scope of type checking. Types-as-sets is simply false as an introductory concept.
- catnaroek 10y ago
  > No one except mathematicians and type theorists are using HoTT, Right. > where every programmer in existence is using first-order and sometimes second-order logic. I'm not so sure about this one. Perhaps by “programmer” you mean “every Haskell programmer”? Even then I'm still not sure. Are you counting “let's approximate `forall x. P(x)` with the large but finite conjunction `P(a) /\ P(b) /\ P(c) ...`” as “using first-order logic”?
  - naasking 10y ago
    I mean pretty much every programmer, even C programmers. Simple business logic is rife with such propositions. Note that I didn't say they use first-order logic to encode invariants in types or anything, but they obviously use it everyday to write programs Haskell programmers also use higher order logic, which is also common now in Java and C#.
    - catnaroek 10y ago
      > Note that I didn't say they use first-order logic to encode invariants in types or anything, but they obviously use it everyday to write programs I wasn't talking about types either. Most programmers I've talked to simply can't use formal logic.
      - naasking 10y ago
        Hmm, I don't think you're being very charitable. That these programmers can write working programs suggest they sufficiently understand disjunction, conjunction, negation, conditionals and quantification. Perhaps they have trouble abstracting the semantics from their preferred language and/or syntax, but that doesn't mean they don't grasp their meaning.
        catnaroek 10y ago
        I offer this thread as evidence: https://news.ycombinator.com/item?id=12342583 https://news.ycombinator.com/item?id=12342583
        naasking 10y ago
        That's definitely not being charitable. Subtyping has some pretty subtle interaction with other typing features, which is why it's still being studied more than 20 years after Cardelli's "Subtyping Recursive Types". The pernicious conflation of subtyping and subclassing in common OO programming languages just compounds the confusion.
        eli_gottlieb 10y ago
        Hey, it's not the fault of the programming masses that some evil motherfucker conflated implementation extension (inheritance) and subtyping. Subtyping = "A <: B, therefore I can start with an A, forget the details irrelevant to B, and just use it as a B." Inheritance = "A inherits B, if I try to actually use it as a B, it promises to work. However, it might actually blow up in my face, because it was keeping its extra details secret from me and promising they wouldn't blow up."

naasking 10y ago

No one except mathematicians and type theorists are using HoTT, where every programmer in existence is using first-order and sometimes second-order logic. I think it should be obvious which is more appropriate if this is supposed to be an introduction. The idea that types express propositions in first- or second-order logic about a program one is writing is sufficiently general for every programmer to understand the proper scope of type checking. Types-as-sets is simply false as an introductory concept.

catnaroek 10y ago
> No one except mathematicians and type theorists are using HoTT, Right. > where every programmer in existence is using first-order and sometimes second-order logic. I'm not so sure about this one. Perhaps by “programmer” you mean “every Haskell programmer”? Even then I'm still not sure. Are you counting “let's approximate `forall x. P(x)` with the large but finite conjunction `P(a) /\ P(b) /\ P(c) ...`” as “using first-order logic”?
- naasking 10y ago
  I mean pretty much every programmer, even C programmers. Simple business logic is rife with such propositions. Note that I didn't say they use first-order logic to encode invariants in types or anything, but they obviously use it everyday to write programs Haskell programmers also use higher order logic, which is also common now in Java and C#.
  - catnaroek 10y ago
    > Note that I didn't say they use first-order logic to encode invariants in types or anything, but they obviously use it everyday to write programs I wasn't talking about types either. Most programmers I've talked to simply can't use formal logic.
    - naasking 10y ago
      Hmm, I don't think you're being very charitable. That these programmers can write working programs suggest they sufficiently understand disjunction, conjunction, negation, conditionals and quantification. Perhaps they have trouble abstracting the semantics from their preferred language and/or syntax, but that doesn't mean they don't grasp their meaning.
      - catnaroek 10y ago
        I offer this thread as evidence: https://news.ycombinator.com/item?id=12342583 https://news.ycombinator.com/item?id=12342583
        naasking 10y ago
        That's definitely not being charitable. Subtyping has some pretty subtle interaction with other typing features, which is why it's still being studied more than 20 years after Cardelli's "Subtyping Recursive Types". The pernicious conflation of subtyping and subclassing in common OO programming languages just compounds the confusion.
        eli_gottlieb 10y ago
        Hey, it's not the fault of the programming masses that some evil motherfucker conflated implementation extension (inheritance) and subtyping. Subtyping = "A <: B, therefore I can start with an A, forget the details irrelevant to B, and just use it as a B." Inheritance = "A inherits B, if I try to actually use it as a B, it promises to work. However, it might actually blow up in my face, because it was keeping its extra details secret from me and promising they wouldn't blow up."