3 ms·

Can you explain to me in what sense the Java and C++ typing systems are logics? Because I don't see it.

by mafribe 10y ago

dvt 10y ago
Any typing system that has at least two types (functional and non-functional) is a logic. In fact, modus ponens follows axiomatically via →elimination: Let α → H be a functional type where α is a Person type, and H is a boolean type. Γ ⊢ α → H Γ ⊢ α --------------------- (→e) Γ ⊢ H What this means is that you can have a function isAtHome(x) which takes a Person and returns a boolean. This schema itself is a logic insofar that it follows the same rules as the proposition A → B where A is true: A → B A ∴ B (I wrote a simple and short paper[1] about typing λ-calculus in the context of Frege's concept horse paradox a few years ago.) [1] http://dvt.name/logic/horse2.pdf http://dvt.name/logic/horse2.pdf
- mafribe 10y ago
  It's not enough for a formalism to exhibit modus ponens to be a logic. It also needs to be consistent.
  - dvt 10y ago
    There are many paraconsistent logics out there[1]. There are also many "trivial" logics out there[1] (which exhibit the Principle of Explosion). The former are useful, the latter not so much. All them of them are logics. Consistency is not a requirement; it's simply a property a system may or may not have. [1] http://plato.stanford.edu/entries/logic-paraconsistent/ http://plato.stanford.edu/entries/logic-paraconsistent/
    - mafribe 10y ago
      C++ and Java are not even paraconsistent: every type is inhabited.
- chriswarbo 10y ago
  Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules. I was struggling to think of a concrete example less trivial than function application, but I suppose my difficulty just shows how terrible these systems are when viewed as logics (but they're still logics!)
  - dvt 10y ago
    > Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules. Yep, exactly. Why I think it's hard to think of a more concrete example is because any type theory (like vanilla λ-calculus) is not deductive. Let me clarify: once you add types to λ-calculus, it (amazingly) becomes deductive! But the type theory itself is not deductive (because types are not tractable, among other reasons).

Can you explain to me in what sense the Java and C++ typing systems are logics? Because I don't see it.

by mafribe 10y ago

Can you explain to me in what sense the Java and C++ typing systems are logics? Because I don't see it.

dvt 10y ago

Any typing system that has at least two types (functional and non-functional) is a logic. In fact, modus ponens follows axiomatically via →elimination: Let α → H be a functional type where α is a Person type, and H is a boolean type. Γ ⊢ α → H Γ ⊢ α --------------------- (→e) Γ ⊢ H What this means is that you can have a function isAtHome(x) which takes a Person and returns a boolean. This schema itself is a logic insofar that it follows the same rules as the proposition A → B where A is true: A → B A ∴ B (I wrote a simple and short paper[1] about typing λ-calculus in the context of Frege's concept horse paradox a few years ago.) [1] http://dvt.name/logic/horse2.pdf http://dvt.name/logic/horse2.pdf

mafribe 10y ago
It's not enough for a formalism to exhibit modus ponens to be a logic. It also needs to be consistent.
- dvt 10y ago
  There are many paraconsistent logics out there[1]. There are also many "trivial" logics out there[1] (which exhibit the Principle of Explosion). The former are useful, the latter not so much. All them of them are logics. Consistency is not a requirement; it's simply a property a system may or may not have. [1] http://plato.stanford.edu/entries/logic-paraconsistent/ http://plato.stanford.edu/entries/logic-paraconsistent/
  - mafribe 10y ago
    C++ and Java are not even paraconsistent: every type is inhabited.
chriswarbo 10y ago
Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules. I was struggling to think of a concrete example less trivial than function application, but I suppose my difficulty just shows how terrible these systems are when viewed as logics (but they're still logics!)
- dvt 10y ago
  > Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules. Yep, exactly. Why I think it's hard to think of a more concrete example is because any type theory (like vanilla λ-calculus) is not deductive. Let me clarify: once you add types to λ-calculus, it (amazingly) becomes deductive! But the type theory itself is not deductive (because types are not tractable, among other reasons).