7 ms·

Relation Between Type Theory, Category Theory and Logic

177 points by rndn 11y ago

deleted 11y ago
[deleted]
HOLYCOWBATMAN 11y ago
https://www.youtube.com/watch?v=Ccoj5lhLmSQ https://www.youtube.com/watch?v=Ccoj5lhLmSQ
- dang 11y ago
  Please don't post unsubstantive comments to Hacker News.
noblethrasher 11y ago
Also, see some of Robert Harper's lectures on the same subject: https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_Ync...
AdieuToLogic 11y ago
Something I looked for on this very intriguing site was a reconciliation in my mind between dependent types and higher kinded types. This has been a nagging question since the announcement of Scala moving to the DOT calculus[1]. While this page[2] helped a bit, doing more research unveiled an example put out by Runar here[3]. Has anyone else considered a reasonable method for addressing what higher-kinded types provide currently in a DOT calculus, especially as it pertains to "matching" the type parameters in a higher-kinded type? 1 - http://lampwww.epfl.ch/~amin/dot/fool.pdf http://lampwww.epfl.ch/~amin/dot/fool.pdf 2 - http://ncatlab.org/nlab/show/dependent+type+theory http://ncatlab.org/nlab/show/dependent+type+theory 3 - https://gist.github.com/runarorama/33986541f0f1ddf4a3c7 https://gist.github.com/runarorama/33986541f0f1ddf4a3c7
- deleted 11y ago
  [deleted]
- mafribe 11y ago
  reconciliation in my mind between dependent types and higher kinded types. They are orthogonal concepts. This is made very clear in Barendregt's λ-cube [1]. Orthogonal here means that a typing system might be higher-kinded without allowing type-dependency, or it might allow type-dependency without having higher-kinds. An example of the latter is LF, the Logical Framework of Harper et al. Haskell, or at least some forms of Haskell are an example of the former. Higher-kinded types simply allow functions and function application at the type level which can take functions as arguments and can return functions. For example (lambda x.x => bool) and (lambda xy. x => y) are functions at the type level. An example of a dependent type is List(2+4)[bool], of lists of length 6 carrying booleans. Here (2+4) is a program. This parameterisation happens without having type-functions. [1] https://en.wikipedia.org/wiki/Lambda_cube https://en.wikipedia.org/wiki/Lambda_cube
szany 11y ago
See also Bob Harper's blog for a more leisurely exposition: https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...
- joe_the_user 11y ago
  "Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof!" The thing I never understood about statements of this sort is that in my understanding of model theory, Godel's theorem and so-forth, a proof is a rare thing. Most of the true statements in a given model don't have proofs. Any consistent proof system admits an uncountable sets of independent theorems and so-forth.
  - szany 11y ago
    Most true statements are uninteresting.
    - joe_the_user 11y ago
      Indeed but so are most programs.
  - mafribe 11y ago
    While Goedel's first incompleteness theorem indeed shows that there will always be true statements that don't follow from a given set of (computable) axioms, this is almost never a problem in practise. It is hard to find natural examples of such statements. Almost every mathematical statement (or its negation) you or I can come up with is a consequence of the axioms of ZFC set theory, or whatever other foundation you prefer.
    - joe_the_user 11y ago
      It doesn't follow in normal mathematical practice I think because mathematicians want natural, sane axioms that lead to human understandable models. Computing already starts out much messier in its activities. Determining what will happen when a large system gets input is tricky. I'm not sure what could proved about the operations of a "deep neural net" for example.
Xcelerate 11y ago
Can someone give me an absolute layman explanation to homotopy type theory (and why it's so interesting)? I'm hearing about it everywhere, but most of the introductions to the subject assume the reader is already familiar with either type theory or category theory.
- j2kun 11y ago
  I'll try to keep it short and skip the details of the mathematical framework itself. Back in the early 1900's there was a school of mathematical logic that denied a certain axiom called the law of the excluded middle, that !!p <=> p. They said that if you used this axiom (roughly) your proof was not "constructive," whereas if you avoided it your proof was "constructive." They went as far as to deny all math that was not constructive (which I think is silly). Their ideas faded out of popularity among mainstream mathematicians, but their goal was to rewrite the foundations of all mathematics using only constructive proofs, and to their credit they got pretty damn far in certain subjects like real analysis (calculus). Today, their ideas are seeing a resurgence in the homotopy type theorists (HTTs). Their goal is also to rewrite all of mathematics in a constructive way, but now they have the hindsight of these great tools like category theory and homology and computers and all these great things developed in the mid to late 20th century. So they are working on building this framework and seeing what it can prove. The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive) and one of their main selling points is that their work will eventually lead to "computer assisted mathematics," not in the sense of Stephen Wolfram but rather in the sense that a computer will check your proofs as you prove them and find stupid mistakes. I personally am not all that excited about HTT, due to what I see as misguided hype around it. My preferred way to view it is as logicians studying a really fascinating new logical system and seeing how far they can push it. Saying things like "I deny all mathematics that's not constructive" and "computers will start doing our proofs for us," makes me cringe. But it is what it is :)
  - mafribe 11y ago
    j2kun's characterisation of HoTT is misleading. Their goal is also to rewrite all of mathematics in a constructive way, This is not the goal of HoTT, and also not possible as some mathematics is intrinsically non-constructive. HoTT allows non-constructive reasoning, see section 3.4 "Classical vs. intuitionistic logic" of the HoTT book http://homotopytypetheory.org/book/ http://homotopytypetheory.org/book/. You can say that HoTT derives non-constructive mathematics on top of constructive foundations. The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive) No. Whether a proof can be logically checked by a computer has nothing to do with whether it is constructive or not. A proof is just a syntactic object. It's just as easy to check if a proof step uses excluded middle or double negation as it is to check whether it uses a construtive principle like /\-introduction. There are many proof assitants that work with classical logic, e.g. Mizar, HOL, HOL light, Isabelle/HOL ... All of SAT-solving works classically. The novelty of HoTT, and only extension over intensional Martin-Loef type-theory, is the univalence axiom.
Xcelerate 11y ago
Can someone give me an absolute layman explanation to homotopy type theory (and why it's so interesting)? I'm hearing about it everywhere, but most of the introductions to the subject assume the reader is already already familiar with either type theory or category theory.

177 points by rndn 11y ago

deleted 11y ago

[deleted]

HOLYCOWBATMAN 11y ago

https://www.youtube.com/watch?v=Ccoj5lhLmSQ https://www.youtube.com/watch?v=Ccoj5lhLmSQ

dang 11y ago
Please don't post unsubstantive comments to Hacker News.

noblethrasher 11y ago

Also, see some of Robert Harper's lectures on the same subject: https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_Ync...

AdieuToLogic 11y ago

Something I looked for on this very intriguing site was a reconciliation in my mind between dependent types and higher kinded types. This has been a nagging question since the announcement of Scala moving to the DOT calculus[1]. While this page[2] helped a bit, doing more research unveiled an example put out by Runar here[3]. Has anyone else considered a reasonable method for addressing what higher-kinded types provide currently in a DOT calculus, especially as it pertains to "matching" the type parameters in a higher-kinded type? 1 - http://lampwww.epfl.ch/~amin/dot/fool.pdf http://lampwww.epfl.ch/~amin/dot/fool.pdf 2 - http://ncatlab.org/nlab/show/dependent+type+theory http://ncatlab.org/nlab/show/dependent+type+theory 3 - https://gist.github.com/runarorama/33986541f0f1ddf4a3c7 https://gist.github.com/runarorama/33986541f0f1ddf4a3c7

deleted 11y ago
[deleted]
mafribe 11y ago
reconciliation in my mind between dependent types and higher kinded types. They are orthogonal concepts. This is made very clear in Barendregt's λ-cube [1]. Orthogonal here means that a typing system might be higher-kinded without allowing type-dependency, or it might allow type-dependency without having higher-kinds. An example of the latter is LF, the Logical Framework of Harper et al. Haskell, or at least some forms of Haskell are an example of the former. Higher-kinded types simply allow functions and function application at the type level which can take functions as arguments and can return functions. For example (lambda x.x => bool) and (lambda xy. x => y) are functions at the type level. An example of a dependent type is List(2+4)[bool], of lists of length 6 carrying booleans. Here (2+4) is a program. This parameterisation happens without having type-functions. [1] https://en.wikipedia.org/wiki/Lambda_cube https://en.wikipedia.org/wiki/Lambda_cube

szany 11y ago

See also Bob Harper's blog for a more leisurely exposition: https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...

joe_the_user 11y ago
"Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof!" The thing I never understood about statements of this sort is that in my understanding of model theory, Godel's theorem and so-forth, a proof is a rare thing. Most of the true statements in a given model don't have proofs. Any consistent proof system admits an uncountable sets of independent theorems and so-forth.
- szany 11y ago
  Most true statements are uninteresting.
  - joe_the_user 11y ago
    Indeed but so are most programs.
- mafribe 11y ago
  While Goedel's first incompleteness theorem indeed shows that there will always be true statements that don't follow from a given set of (computable) axioms, this is almost never a problem in practise. It is hard to find natural examples of such statements. Almost every mathematical statement (or its negation) you or I can come up with is a consequence of the axioms of ZFC set theory, or whatever other foundation you prefer.
  - joe_the_user 11y ago
    It doesn't follow in normal mathematical practice I think because mathematicians want natural, sane axioms that lead to human understandable models. Computing already starts out much messier in its activities. Determining what will happen when a large system gets input is tricky. I'm not sure what could proved about the operations of a "deep neural net" for example.

Xcelerate 11y ago

Can someone give me an absolute layman explanation to homotopy type theory (and why it's so interesting)? I'm hearing about it everywhere, but most of the introductions to the subject assume the reader is already familiar with either type theory or category theory.

j2kun 11y ago
I'll try to keep it short and skip the details of the mathematical framework itself. Back in the early 1900's there was a school of mathematical logic that denied a certain axiom called the law of the excluded middle, that !!p <=> p. They said that if you used this axiom (roughly) your proof was not "constructive," whereas if you avoided it your proof was "constructive." They went as far as to deny all math that was not constructive (which I think is silly). Their ideas faded out of popularity among mainstream mathematicians, but their goal was to rewrite the foundations of all mathematics using only constructive proofs, and to their credit they got pretty damn far in certain subjects like real analysis (calculus). Today, their ideas are seeing a resurgence in the homotopy type theorists (HTTs). Their goal is also to rewrite all of mathematics in a constructive way, but now they have the hindsight of these great tools like category theory and homology and computers and all these great things developed in the mid to late 20th century. So they are working on building this framework and seeing what it can prove. The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive) and one of their main selling points is that their work will eventually lead to "computer assisted mathematics," not in the sense of Stephen Wolfram but rather in the sense that a computer will check your proofs as you prove them and find stupid mistakes. I personally am not all that excited about HTT, due to what I see as misguided hype around it. My preferred way to view it is as logicians studying a really fascinating new logical system and seeing how far they can push it. Saying things like "I deny all mathematics that's not constructive" and "computers will start doing our proofs for us," makes me cringe. But it is what it is :)
- mafribe 11y ago
  j2kun's characterisation of HoTT is misleading. Their goal is also to rewrite all of mathematics in a constructive way, This is not the goal of HoTT, and also not possible as some mathematics is intrinsically non-constructive. HoTT allows non-constructive reasoning, see section 3.4 "Classical vs. intuitionistic logic" of the HoTT book http://homotopytypetheory.org/book/ http://homotopytypetheory.org/book/. You can say that HoTT derives non-constructive mathematics on top of constructive foundations. The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive) No. Whether a proof can be logically checked by a computer has nothing to do with whether it is constructive or not. A proof is just a syntactic object. It's just as easy to check if a proof step uses excluded middle or double negation as it is to check whether it uses a construtive principle like /\-introduction. There are many proof assitants that work with classical logic, e.g. Mizar, HOL, HOL light, Isabelle/HOL ... All of SAT-solving works classically. The novelty of HoTT, and only extension over intensional Martin-Loef type-theory, is the univalence axiom.

Xcelerate 11y ago

Can someone give me an absolute layman explanation to homotopy type theory (and why it's so interesting)? I'm hearing about it everywhere, but most of the introductions to the subject assume the reader is already already familiar with either type theory or category theory.