3 ms·

From the examples: > 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 means “𝗍𝗋𝗎𝖾+2 has type 𝖨𝗇𝗍”, which makes even less sense, as the expression 𝗍𝗋𝗎𝖾+2 is nonsense and does not h

• edgyquant 3y ago
  Isn’t this language specific? For instance in C doesn’t true map to 1, thus true+1=2
  • Tainnor 3y ago
    The runtime values don't matter to type theory, only the types of expressions.
• dreamcompiler 3y ago
  Even though 'True + 2' doesn't throw an error in Python or C, it's still stupid because it makes the semantics of the language hard to reason about, in order to give programmers a little syntactic sugar.
  • anttihaapala 3y ago
    This is for backward-compatibility reasons. The comparison operators in Python produced 1 or 0 before boolean was a thing, and programs existed that exploited this, i.e. you can do something like `(a < b) - (a > b)` in a sorting algorithm. Same thing in C, or even more so, as the comparison operators produce an `int` instead of a `bool`.
  • logicchains 3y ago
    >Even though 'True + 2' doesn't throw an error in Python or C, it's still stupid because it makes the semantics of the language hard to reason about It's consistent. If we add a 64 bit integer and a 32 bit integer, we'd expect to get a 64 bit integer as the result. Same with if we add a 64 bit integer and a 4 bit integer. So why shouldn't it also apply if we add a 64 bit integer and a 1 bit integer? Mathematically, bool is a 1-bit integer with fancy names for 1 and 0.
    • dreamcompiler 3y ago
      Because booleans are not 1-bit integers. They're not integers at all. The only thing computers represent directly are ones and zeros. 1 and 0 are not integers either; they're just high or low voltage levels on wires. The fact that we label them "1" and "0" is just for convenience; it doesn't make them integers. Even addition itself is an abstraction. As far as the CPU is concerned, addition is just a multi-bit XOR operation coupled with some AND operations. We abstract sets of 1s and 0s to mean numbers, pointers, characters, booleans, symbols, arrays, structures, etc. and we abstract operations on them as well. If we don't make our abstractions explicit, we cannot reason about what results to expect from a computer's operations, nor can we enlist computers to help us with that reasoning process. By your argument I might as well add integers to strings or arrays or structures -- they're all just bits after all. We might as well not have types at all and just let the programmer keep track of all operations manually. That's assembler programming and it's extremely bug-prone and it doesn't scale.
      • account42 3y ago
        The ring ({false,true},xor,and) is isomorphic to ℤ₂ aka the 1-bit integers. Deal with it.
• Tainnor 3y ago
  If you think that True + 2 makes sense, you can just define your own judgments that allow it (*). Logic, and the theory behind type systems, don't care about your axioms and inference rules, they just let you reason about them, and their interactions. (*) Something like |- True : Bool |- True : Int or, if you only want to allow it in certain expressions |- x : Int ----------- |- True + x: Int etc.