41–50 of 51 posts
what about categorial semantics? hahaha!!!
Walk away now. Type Theory derailed my PhD studies. Seduced by constructivism, Curry-Howard, Martin-Löf and especially Girard's Proofs and Types, I wasted two years and subsequently abandoned my postgraduate studies. It's comp. sci. flavoured esoteric nonsense.
Earlier quoted context omitted.
So where did Java generics come from, then? Or pretty much anything in Scala? Or Rust or C++11 lambdas or Swift? It's all pretty much exactly the same as done in academic type theory for decades.
It really isn't. Take a good long look at Java generics and ask yourself if they really came straight out of type theory research. They didn't, that's why they're so botched, and why Odersky wanted a do-over with Scala :] More seriously, Scala and Rust are the only things in your list that would actually claim to be influenced by academia. I'm sure Apple is not going for the type theorists with Swift, despite having…
At any rate, C++, Scala, Rust, Java.. these are not languages that take type theory very seriously, and probably couldn't. It's certainly true that the popular imperative languages don't take TT seriously.
But so what? The comment was about general purpose languages, and type theory is demonstrably of use in implementing them. Just because most mainstream languages don't use type theory doesn't make that not true. It just means most mainstream languages do not make use of everything they could.
Oh well. Their loss.
Good list, I'd also recommend http://www.cs.cmu.edu/~rwh/plbook/book.pdf for something designed for newcomers to the field
What's Type Theory and how's it different from Set Theory and Category Theory?
I want to disagree a little bit with chas here and just say that type theory as we know it today emerged out of a different, post-computer tradition than old-school Russellian type theory. Modern type theory comes arguably from Martin-Löf and the FP domain. As for what is type theory vs. set theory vs. category theory, I'd put it this way: type theory is a flavor of proof theory built on computational justification o…
I am interested to hear about practical application of type theory and how it helped solve real world software and hardware problem better.
http://www.cs.cmu.edu/~rwh/plbook/book.pdf
Harper's thesis is that type theory is the backbone for language design. When you read his book you see him elaborate this and show how it applies to understanding and designing practical languages that work right.
Earlier quoted context omitted.
I want to disagree a little bit with chas here and just say that type theory as we know it today emerged out of a different, post-computer tradition than old-school Russellian type theory. Modern type theory comes arguably from Martin-Löf and the FP domain. As for what is type theory vs. set theory vs. category theory, I'd put it this way: type theory is a flavor of proof theory built on computational justification o…
This is what I don't get... _Why_ is 'type' theory _a logic_? A type is an enumeration of values (terms), right? What's that got to do with truth values and how they may be manipulated? I've read some of the papers/texts you posted in that tremendously helpful summary (thanks by the way!) and talking about type theory always segues into talking about logic. If you could explain that _one_ thing I'd be so happy. To me…
1:
My first answer is, because of the nature of what a logic is. Logics are systems for reasoning about some problem domain, or put it another way, logics are ways of convincing yourself that you're justified in believing a judgment (`A is true`, `B is a proposition`, `C is tasty`).
What this means is that, to have a proof `M` which proves a judgment `J`, is to have some piece of data which you can look at. So all proofs are some kind of data, in the same way that all novels and all movies are some kind of data.
A harder question is why all data is a kind of proof and that's more subtle. Some people actually want to say they're not, proofs are just a special kind of data, while others want to just say to loosen the notion of proof and proposition. I don't think there's a good answer for this direction.
2:
My second answer is, it turns out they couldn't be anything else! Consider the inference rule (written in natural English):
if you know
A is true
and you know
B is true
then you can conclude
A&B is true
Now consider this description of how to make pairs:
if you have
M of type A
and you have
N of type B
then you can make
(M,N) of type A*B
Now I ask you, what are you doing when "proving A&B" if not taking two things (two smaller proofs of `A` and `B`) and sticking them together to form a new piece of data (the proof of `A&B`)? I would argue you're not doing ANYTHING different. The act of proving a conjunction is just the same as the act of making a pair!
Now do this for other logical connectives:
proving a disjunction is just the same as giving an element of a tagged union
proving an implication is just the same as giving a function
proving the trivial proposition is just giving a 0-length tuple
proving the absurd proposition (which is impossible)
is just giving a void-type value (which is impossible)
----
Now, I should say, this connection does not mean that all logics are type theories! Type theory has a very specific view of how inference rules are justified, by appeal to certain principles which turn out to be computational in nature.
Why these principles should be so powerful as computational principles, I don't know. It's a mystery. Maybe God is a type theorist? ;p
I am interested to hear about practical application of type theory and how it helped solve real world software and hardware problem better.
The more common practical uses are:
1) If you're using a statically typed language, knowing some basic TT will let you understand the hows and whys of its type system. This is especially true of static langs that have richer type systems, like Haskell.
2) Rich type systems actually help you program! a lot of people complain that type systems merely complain when you mess up -- which is helpful, because you now know you've messed, but not completely helpful because it feels like the types don't help you. The truth is,, this is mostly true only of BAD type systems.
A GOOD type system can guide you to the right answer by making the number of possible programs very tiny. Instead of infinitely many programs, there might just be one or two.
A GOOD type system can guide you to the right answer by making it possible for the computer to write parts of the program for you because the types make it obvious what the options are at any moment program construction.
For specific examples, you'd have to look around. I don't have any offhand (nor am I trying to convince you to learn TT!). Conal Elliot and Edward Kmett no doubt have plenty of good examples, or could tell you who does.
Earlier quoted context omitted.
Walk away now. Type Theory derailed my PhD studies. Seduced by constructivism, Curry-Howard, Martin-Löf and especially Girard's Proofs and Types, I wasted two years and subsequently abandoned my postgraduate studies. It's comp. sci. flavoured esoteric nonsense.
is there anything in the world that is non-nonsense? so it is better to study pure-nonsense, just because it is pure
I am interested to hear about practical application of type theory and how it helped solve real world software and hardware problem better.
Aside from PFPL, which is oriented towards implementors of programming languages, type theory has practical uses in the act of programming itself. That is to say, with an adequate type theory, you can at a minimum use it to help you construct proofs that your programs do what you want them to do. But that's doable with any meta-system for certified programming, TT is just one particular meta-system that has some nice…