Propositions as Types - Computerphile

Mathematics once again meets Computer Science as Professor Altenkirch continues to discuss Type Theory

Thanks to Lily the dog!

This video was filmed and edited by Sean Riley.

[ThePritt]

My unpopular opinion: His videos are the best on computerphile.

[lovealien]

Eigentlich gut verständlich, aber er verwendet mächtig viele Anglizismen.

[lierdakil]

Finally a video on Curry-Howard equivalence! A nice, simple way to introduce it to boot. This was a bit of a mind-blower when I first stumbled upon it and really understood what it meant (being reasonably competent in both mathematics and programming at that point). One minor nitpick, you could've probably named the thing to make it easier to google for.

[erinc.]

About Vladimir Voevodsky's work there's an excellent article from Quanta Magazine written in May 2015. It's about replacing the foundation of maths (set theory) by univalent foundations (type theory), and how then that helps to automate maths proofs.

[daxvena]

Wow, it's so weird seeing this video after discovering these concepts on my own a few months ago for a project that I have been working on. What I discovered is that predicate logic, algebra and type theory all have a very similar structure:

not ⊂ incrementation ⊂ option type (nullable value)
xor ⊂ addition ⊂ sum type (enum + union)
and ⊂ multiplication ⊂ product type (structs/tuples/cons cell)
implication ⊂ exponentiation ⊂ function type

false ⊃ 0 ⊃ bottom type ("exception")
true ⊃ 1 ⊃ unit type ("void")
true ⊃ ...
true ⊃ ∞/variable ⊃ top type (untyped variable)

From this I also discovered:
- Predicate logic is a restriction of algebra, where every operation is performed modulo 2.
- Algebra is a restriction of type theory, where every operation is performed on the number of possible states each type describes.
- Type theory doesn't need inverse functions like in algebra (decrement, subtraction, division, root, logarithm) because it is completely constructive.

I've tried imagining what hyper-operations after exponentiation would mean, but I couldn't think of anything useful other than that it may be related to mapping lower dimension types to higher dimension types (point => line => circle => sphere => ... n-sphere).

[kwanghoonchoi]

I love a scene interrupted by a cute puppy. Totally unexpected in propositions as types!!


8:10

[Yotanido]

Some good stuff on computerphile lately. You should probably link to the paper, though.

Also, if anyone wants to actually play around with this: Take a look at Agda or Coq. Those are languages specifically made to do this.
Some other functional languages like Haskell and Idris can also do this, but especially in Haskell, it's a bit of effort.

[Cody]

I don’t see the problem with his voice, its not hard to understand what he saying.

[AlexBerg]

This is a hugely important idea in programming. Great introduction to the idea here! Thanks!

[krasserkalle]

Best video from this guy on computerphile so far

[IwoIwanov]

This is just fascinating. Top content right here on Computerphile. Thanks for this.

[Kalernor]

I didn't fully understand, but this area seems very interesting to me. I am a cs student generally interested in areas relating to mathematical logic so these seems like a perfect fit for me. I will be reading more into this.

[ntmg]

Awesome video. Thanks to all people which makes this type of content possible :)

[matthewkriebel]

I'm just digging that classic LaserJet with the IrDA interface.

[MusicThatILike]

I worked with a language in university, coq, that allows one to write provably correct programs. The syntax being shown is very similar, I wouldn't be surprised if professor Altenkirch is one of the individuals working on it.

[AhmadKhan-porl]

I’m confused at minute 15:03 where he’s explaining why the Law of Excluded Middle does not hold in this isomorphism. He says we must decide if all predicates are either true or all predicates are false, but aren’t we showing that all predicates are either true/false? As in the prime number example given, where for some Natural Numbers its going to be true, while for others it will be false. Does anyone have an explanation?

[brantwedel]

What I got out of it: If something is not provable it is not classically computable therefore use a mathematical logic that represents the idea of computability for computer science applications?

[ibic]

At 9:00, I believe he's talking about some people call the `left` and `right` functions as `inl` and `inr`.

[coachsteve.]

Very well explained! Here is a simple Haskell implementation.

{-# LANGUAGE TypeOperators #-}

type P = Bool
type Q = Bool
type R = Bool

type a × b = (a, b)
type a + b = Either a b

f :: P × (Q + R) -> (P × Q) + (P × R)
f (x, Left y) = Left (x, y)
f (x, Right z) = Right (x, z)

[SSJHF]

One thing I have noticed from the comments in this video, is that everyone is from a different background.

Some are programmers, some are mathematicians, some are logicians and some have no background in the things you covered.