4 ms·

In a world where cranks use Curry-Howard to justify their ridiculous beliefs, it is refreshing to see not just a correct application, but a well-formed and aest

In a world where cranks use Curry-Howard to justify their ridiculous beliefs, it is refreshing to see not just a correct application, but a well-formed and aesthetically pleasing presentation. Thank you for not trying to obfuscate the material.

throwaway_pdp09 7y ago
> where cranks use Curry-Howard to justify their ridiculous beliefs I'm not an abstract thinker so that correspondence is not interesting to me (open to being educated though if it is applicable to my daily work), but to what ridiculous beliefs do you refer? TIA
- ampdepolymerase 7y ago
  ��
  - TheAsprngHacker 7y ago
    Given that most (but not all) Lisps are untyped, I don't see what Lisp evangelism has to do with the Curry-Howard correspondence...
    - wglb 7y ago
      Which Lisp are you referring to? There are types all over CL.
      - TheAsprngHacker 7y ago
        Sorry, by "untyped" I meant "dynamically typed." CL does have a sophisticated type hierarchy, but to my knowledge, according to the standard, types are checked at runtime, right? In the type-theoretic sense, "type" refers to a statically known classification. Curry-Howard is the idea that static types are propositional formulas and expressions that have such types are their proofs. Under the Curry-Howard correspondence, a static typechecker analyzing your program is equivalent to a proof checker ensuring that your proof is valid. People tend to invoke Curry-Howard to praise ML- and Haskell-style algebraic types (according to Curry-Howard, sum types are disjunction, product types are conjunction, and function/exponential types are implication).
        wglb 7y ago
        types are checked at runtime, right? Not entirely. There are type errors that are caught at compilation time. A stark difference is that Lisp has the idea that type checking is done on values, not on symbols. If the compiler can deduce that a value is going to conflict in a given context, it will flag the error. And types are checked at run time as well.
- lidHanteyk 7y ago
  Curry-Howard-Lambek distills largely into a big table which relates type theory, category theory, formal logic, and metamathematics. This table is very precise, but high-dimensional, so that we can only take small limited slices of it. Nonetheless, the slices that we take are very formal. The important parts are well-known and published, say at [0] or [1]; extending beyond this is possible but requires care and effort. That said, once one groks the nature of the correspondence, then it becomes painfully obvious, to the point where folks who don't grok it seem block-headed. I don't really have a glossary or nosology of how people misuse this, but I'd say some wrong ideas include: * If a language has a type system, then it is usable for formal proofs, it is sound, and it is a language that ends the need for other languages. * Dependently-typed languages have values that are also types, so all values are types, and therefore dependent typing makes no sense. * Because my language uses higher-order logic instead of first-order logic, Turing's results don't limit my language's problem-solving abilities. * Because of my religious beliefs, type universes have a certain shape, and thus Cantor's results are incorrect. * The English language is far more powerful than any programming language. * All logic is really just intuitionistic logic. * All logic is really just linear logic. * Syntactic formalism must be wrong, because abstracta only exist in my mind. To repeat myself, all of these are wrong, despite some relatively large tribes of programmers believing them sincerely. [0] https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory https://ncatlab.org/nlab/show/relation+between+type+theory+a... [1] http://math.ucr.edu/home/baez/rosetta.pdf http://math.ucr.edu/home/baez/rosetta.pdf
  - danharaj 7y ago
    > * All logic is really just linear logic. Obviously it's all really just tensorial logic :^)
  - cscurmudgeon 7y ago
    Thank you! That list intersects with some of what has been troubling me too. You should write a blog post or paper expanding on these. Some of these beliefs are more dangerous than others. Especially: > * All logic is really just linear logic. and > * Because of my religious beliefs, type universes have a certain shape, and thus Cantor's results are incorrect.

throwaway_pdp09 7y ago

> where cranks use Curry-Howard to justify their ridiculous beliefs I'm not an abstract thinker so that correspondence is not interesting to me (open to being educated though if it is applicable to my daily work), but to what ridiculous beliefs do you refer? TIA

ampdepolymerase 7y ago
��
- TheAsprngHacker 7y ago
  Given that most (but not all) Lisps are untyped, I don't see what Lisp evangelism has to do with the Curry-Howard correspondence...
  - wglb 7y ago
    Which Lisp are you referring to? There are types all over CL.
    - TheAsprngHacker 7y ago
      Sorry, by "untyped" I meant "dynamically typed." CL does have a sophisticated type hierarchy, but to my knowledge, according to the standard, types are checked at runtime, right? In the type-theoretic sense, "type" refers to a statically known classification. Curry-Howard is the idea that static types are propositional formulas and expressions that have such types are their proofs. Under the Curry-Howard correspondence, a static typechecker analyzing your program is equivalent to a proof checker ensuring that your proof is valid. People tend to invoke Curry-Howard to praise ML- and Haskell-style algebraic types (according to Curry-Howard, sum types are disjunction, product types are conjunction, and function/exponential types are implication).
      - wglb 7y ago
        types are checked at runtime, right? Not entirely. There are type errors that are caught at compilation time. A stark difference is that Lisp has the idea that type checking is done on values, not on symbols. If the compiler can deduce that a value is going to conflict in a given context, it will flag the error. And types are checked at run time as well.
lidHanteyk 7y ago
Curry-Howard-Lambek distills largely into a big table which relates type theory, category theory, formal logic, and metamathematics. This table is very precise, but high-dimensional, so that we can only take small limited slices of it. Nonetheless, the slices that we take are very formal. The important parts are well-known and published, say at [0] or [1]; extending beyond this is possible but requires care and effort. That said, once one groks the nature of the correspondence, then it becomes painfully obvious, to the point where folks who don't grok it seem block-headed. I don't really have a glossary or nosology of how people misuse this, but I'd say some wrong ideas include: * If a language has a type system, then it is usable for formal proofs, it is sound, and it is a language that ends the need for other languages. * Dependently-typed languages have values that are also types, so all values are types, and therefore dependent typing makes no sense. * Because my language uses higher-order logic instead of first-order logic, Turing's results don't limit my language's problem-solving abilities. * Because of my religious beliefs, type universes have a certain shape, and thus Cantor's results are incorrect. * The English language is far more powerful than any programming language. * All logic is really just intuitionistic logic. * All logic is really just linear logic. * Syntactic formalism must be wrong, because abstracta only exist in my mind. To repeat myself, all of these are wrong, despite some relatively large tribes of programmers believing them sincerely. [0] https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory https://ncatlab.org/nlab/show/relation+between+type+theory+a... [1] http://math.ucr.edu/home/baez/rosetta.pdf http://math.ucr.edu/home/baez/rosetta.pdf
- danharaj 7y ago
  > * All logic is really just linear logic. Obviously it's all really just tensorial logic :^)
- cscurmudgeon 7y ago
  Thank you! That list intersects with some of what has been troubling me too. You should write a blog post or paper expanding on these. Some of these beliefs are more dangerous than others. Especially: > * All logic is really just linear logic. and > * Because of my religious beliefs, type universes have a certain shape, and thus Cantor's results are incorrect.