I wanted to investigate the relevance of mathematics for understanding type systems in programming languages. However when I tried to read some basic information, I found I was investing more energy learning a formalism different from set theory to solve the same problems I've already solved in set theory.
Can anyone give some really cool applications of Type theory? Like a solution to a problem which would've stumped me had I not know type theory? In particular, can anyone mention applications of type theory for problems in analysis?
Type theory
Moderators: gmalivuk, Moderators General, Prelates
Re: Type theory
You might try looking at what's been done with homotopy type theory. I spent a little time looking through it and had basically the same conclusion you had  it's a bunch of new formalism that doesn't help me understand anything better than I already did. But it's been several months and I haven't been keeping up with developments, so maybe some cool stuff has come out.
What they (mathematicians) define as interesting depends on their particular field of study; mathematical anaylsts find pain and extreme confusion interesting, whereas geometers are interested in beauty.
Re: Type theory
You know I found a free book online about homotopy type theory, skimmed some chapters and tried to read a discussion on real numbers in depth. I found the discussion more difficult to understand then plain English, while not introducing any new analysis ideas. I figured that maybe I just haven't read the book thoroughly enough, but before doing that I might ask for some motivating applications.
Because of this, It's funny you mentioned homotopy type theory.
Because of this, It's funny you mentioned homotopy type theory.

 Posts: 1
 Joined: Tue Oct 28, 2014 1:57 am UTC
Re: Type theory
I don't think it's difficult as long as you are intelligent enough to understand and you to read the book thoroughly.
Re: Type theory
I said more difficult, not impossible, or even hard.
There is more to mathematics then rigor, and that's all the book felt like to me.
I was curious if the Rigor bought anything, and if so, whether I found the conclusions interesting.
There is more to mathematics then rigor, and that's all the book felt like to me.
I was curious if the Rigor bought anything, and if so, whether I found the conclusions interesting.
Re: Type theory
polymer wrote:Like a solution to a problem which would've stumped me had I not know type theory? In particular, can anyone mention applications of type theory for problems in analysis?
Not necessarily unsolved problems, but the thing about constructivist systems (such as ML type theory) is that everything is explicit. If you, for example, prove in such a system that an object t exists, then you simultaneously construct an honesttoGod algorithm for actually finding t. Often, if you have a constructive proof (in the informal sense) you can find such an algorithm by just inspecting the proof, and the formal proof will likely follow the same structure, so the formalism doesn't really help you.
However, there are ways to mechanically translate certain classical proofs to this formalism, which would reveal some algorithmic content that you might not have seen otherwise. Some people have used a system which is in a certain sense a basic type theory to formulate and prove some convergence results from analysis (of the form ∀ε∃δ...) which then lets you "unwind" the proof (as they call it) in order to find explicit bounds δ for every ε even though the classical proof you started with (seemingly) doesn't contain that information. This in turn might help prove other results (which call for such explicit bounds) that you might not otherwise have been able to. Check out [U. Kohlenbach (2008). Applied Proof Theory: Proof Interpretation and their Use in Mathematics] if you are interested in that.
Another point of ML type theory (and more recently Homotopy type theory) is to show that most of mathematics can in fact be done without certain principles and machinery (such as the law of excluded middle and set theory) to which some people have historically raised some philosophical concerns. So regardless of whether (homotopy) type theory gives you new mathematical results (which it might; I haven't been keeping up), it should be remarkable that it works at all, and even allows you to show much of the same things as in the regular mathematical practice.
xkcd forum gamers' Discord chat: https://discord.gg/Q7QM5sH
NOTE: This is not me. That's another guy.heuristically_alone wrote:Tillian you are always in every single one of dreams,
usually driving an ice cream truck.
Who is online
Users browsing this forum: No registered users and 7 guests