Relation Between Type Theory, Category Theory and Logic
1–10 of 77 posts
Re: Relation Between Type Theory, Category Theory and Logic
#2[deleted]
Re: Relation Between Type Theory, Category Theory and Logic
#3Re: Relation Between Type Theory, Category Theory and Logic
#4Also, see some of Robert Harper's lectures on the same subject: https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_Ync...
Re: Relation Between Type Theory, Category Theory and Logic
#5Something 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
Re: Relation Between Type Theory, Category Theory and Logic
#6Something 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 provi…
[deleted]
Re: Relation Between Type Theory, Category Theory and Logic
#7See also Bob Harper's blog for a more leisurely exposition:
https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...
Re: Relation Between Type Theory, Category Theory and Logic
#8Can 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.
Re: Relation Between Type Theory, Category Theory and Logic
#9Can 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.
Re: Relation Between Type Theory, Category Theory and Logic
#10See also Bob Harper's blog for a more leisurely exposition: https://existentialtype.wordpress.com/2011/03/27/the-holy-tr...
"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.