Type theory

For the discussion of math. Duh.

Moderators: gmalivuk, Moderators General, Prelates

polymer
Posts: 125
Joined: Mon Feb 04, 2008 7:14 am UTC

Type theory

Postby polymer » Fri Aug 15, 2014 1:40 am UTC

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?

User avatar
z4lis
Posts: 767
Joined: Mon Mar 03, 2008 10:59 pm UTC

Re: Type theory

Postby z4lis » Sun Aug 17, 2014 10:53 pm UTC

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.

polymer
Posts: 125
Joined: Mon Feb 04, 2008 7:14 am UTC

Re: Type theory

Postby polymer » Tue Aug 19, 2014 5:57 am UTC

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. :)

gibsonferna
Posts: 1
Joined: Tue Oct 28, 2014 1:57 am UTC

Re: Type theory

Postby gibsonferna » Thu Oct 30, 2014 2:31 am UTC

I don't think it's difficult as long as you are intelligent enough to understand and you to read the book thoroughly. 8-)

polymer
Posts: 125
Joined: Mon Feb 04, 2008 7:14 am UTC

Re: Type theory

Postby polymer » Sat Nov 01, 2014 10:46 pm UTC

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.

User avatar
Tillian
NotNotNotTillian
Posts: 71
Joined: Sat May 16, 2009 2:47 pm UTC
Location: Set₁

Re: Type theory

Postby Tillian » Sun Nov 23, 2014 9:54 am UTC

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 honest-to-God 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
heuristically_alone wrote:Tillian you are always in every single one of dreams,
usually driving an ice cream truck.
NOTE: This is not me. That's another guy.


Return to “Mathematics”

Who is online

Users browsing this forum: No registered users and 13 guests