The Hardest Problem in Type Theory - Computerphile 

I'd say the one place where I got quite lost and had to rewatch was the introduction of reflexivity, but the problem is that, if I was Sean, I wouldn't know what to ask other than "I didn't get it... can you explain that again?" :P

You can include me in that...

​@@NuclearCraftMod You know how natural numbers are defined by induction? You have two ways to make natural numbers: - The first is `zero : ℕ` - The second is `succ : ℕ → ℕ` (so for any `n : ℕ`, we have `succ n : ℕ`. Think of `succ n` as `n + 1`, but keeping in mind we haven't defined addition yet). And you also have the rules that all naturals are defined like that ("no junk") and no natural is represented in two different ways by `zero` and `succ` ("no confusion"). This is how we define *inductive types*, using the motto "no junk, no confusion". This motto ensures that to define a function `ℕ → α`, we only need to define it on `zero` and on `succ`. This is called the "elimination rule" (as opposed to the "introduction rules" `zero` and `succ n`). And when you think about it, this is *exactly* your usual induction! Defining something for `zero` is the base case, and defining something for `succ` is the induction hypothesis. Well, equality is defined as an inductive type as well, but with only one introduction rule: - `refl : a = a` In turn, the elimination rule is simpler than for naturals. It says "To prove that a = b implies some property P(a, b), it suffices to prove P(a, a)". In the video example, if you take P = sym, you get "To prove that a = b implies b = a, it suffices to prove a = a". And `a = a` is true by `refl`, so we're done.

@@yaeldillies Thanks a lot for the extra info regarding inductive types, as that does help better appreciate the form of the arguments :) However, really it was the fact that there is only that one introductory definition of equality that I didn’t understand - I just accepted it for the sake of the rest of the video. It’s not as easy for me to see how ‘refl’ is “enough” in the same way ‘zero’ and ‘succ’ are for the naturals, whether defining all equality terms, defining functions or writing proofs.

@@NuclearCraftMod Note that the constructors (here, just refl) should only handle the cases where our property (equality) holds. In any case where your equality relates something other than values of a type directly, such as "a + b = b + a", that's either because it hasn't yet been reduced to canonical form, or it contains free variables (most commonly they're bound outside with a forall). Now, once you actually substitute something for these variables and reduce fully, the only case that needs handling is that a value is equal to itself. Does that help?

The whole of society is constructed on just such a house of cards, where almost every single one is a presumption or underestimation or overestimation.

I agree.

I'd like that, too, but explained a bit better.

Canonical, jawohl!

rofl

😭😭😭

Perhaps he is proving an inverted shirt is still a shirt. Or he knows this is the side with fewer stains.🙃

He is just proving that the generic type for “t-shirt” can still represent the category of all t-shirts, be it folded, rotated or inverted!

I have a shirt of the same kind of which the normal side is the reverse and it raises question but it's a nice shirt

he's ascended beyond the material realm

Look up isomophism of algebraic data types if you want to know how more "complex" types can be "encoded" differently just like booleans as integers

What is the name of this language? Could you please share the link here?

@@theb1z0n Essence. It's not public unfortunately, it may not be public for many more years.

I knew I was already lost when the title said "type theory"

I suspect that I am lost prior to clicking on the video, but the optimist in me cannot be thwarted.

I was trying to click on something about food probably and I’m just wandering around here now

Oh, you are cruel. I read the author's preface to the 20th anniversary edition of GED and now feel that this strange loop is falling into the abyss. I may never be the same.

I’ve almost purchased this many times - now I’m convinced I need to read it - thanks :)

That is a brilliant book. It is work of genius. But it is also extremely witty and entertaining. It covers deep, difficult subjects, but explains them superbly at a level anyone can get into, if they are prepared to put in the effort. It is a big book, but that is mainly because every idea is explained in more than one way. He comes at everything from multiple different angles until you feel it all fit together.

When I was a kid, like 11-12 years, my dad show me this book because I know i loved math, and expected i will ony read the dialogues , which are interesting enough by themself. But i ventured in the classic parts and discovered the TNT. It truly changed me and enlighted me, because at this age I was the kid that provid the answer without the reasoning, considering it futile. This showed me the beauty of proofs.

I would say hofstadters book is a primer for people who haven’t done many proofs. An even better book is Peter smiths An Introduction to Godels theorems.

Yeah it's a bit obscure. As someone who studied cs and understands all the basics here (group theory, isomorphisms,..) I didn't quite get the explanation, haven't had a lesson on type theory. Guess I need to read up on it this on my own. But very interesting topic nonetheless.

What is the university that you studied it in?

@@theb1z0n University of Turin in Italy, the course was called Formal methods for computer science

His channel has more in-depth content!

can be used ... what?

I'm not so sure these things are so clear cut -- you could say that Python is statically typed, too. It's just that every variable refers to a PyObject. What types do (from a type theory point of view) is specify the interface/API for a variable. Python gives you an interface where different methods of the PyObject get called in different situations. There's a related concept called a subtype, which consists of all those things with a specific type that satisfy some given property. PyObjects have a very rich interface, so there are many interesting subtypes in Python, for example by subclassing or duck typing. I think what makes typing "dynamic" is when a program checks whether something is in a given subtype at runtime. Unlike what Prof. Thorsten said, which is that everything can have at most one type, things can be in multiple different subtypes. Python objects can have a length, have arithmetic operations, be iterable, among many others subtypes. Even Haskell has dynamic subtype checking. For example, there is the subtype of nonempty lists, and the head function is only defined for this subtype. If you give it an empty list, the Haskell runtime will stop your program. Some type theories (like the one in Lean) let you turn subtypes into bona fide types that are statically checked, though when you have an object satisfying a subtype you have to supply a proof that you can do the "cast." Languages like Java have an extremely weak version of static subtyping in the form of interfaces. If I'm trying to say anything, it's that there is always some amount of dynamic subtyping in a program, no matter the type system, and it's interesting to find nice ways to express those subtypes statically. This can be difficult, though, since more elaborate subtypes can require that part of your program be a real mathematical proof. Sometimes you can get around this by having functions return some kind of Optional value, returning None for inputs that aren't part of the subtype.

I think in this case nominal typing vs structural typing is also an interesting duality to consider. Set theory deals with unions, subsets, etc. And so does structural typing, you can have types unify based on their structure alone. Nominal typing works more like type theory in the sense that types never share element because every element is sort of inherently tagged with its name (hence "nominal")

@@emiflake A sort of strange thing in type theory like the ones in Coq, Agda, and Lean, which all appear to have nominal typing, is that there must be types that share elements -- this is referred to as the failure of type constructors being injective. There are "too many types" for there to be enough tags to go around, so to speak. This is OK though, because statically you determine types based on how things are constructed in source code. At runtime, though, this means there is necessarily some type erasure (like in the Java generics sense). There's another level to this, which is that types have associated constructors that are used to create elements of that type. You could say the subtype of things created with a particular constructor is nominal because elements are essentially tagged with how they were constructed. An interesting way to implement structural typing is to add in a system that tries to automatically insert reasonable coercion functions when types fail to unify (this can be used in other situations, too, like when using a natural number where an integer is expected). I'm not sure if that does everything you'd want for structural typing, though.

Some level of ambiguity also exists in "statically typed", too. One can argue that C is not statically typed, in the same way that you argue C is not strongly typed: you can subvert the type system via casting, it just has to be done explicitly, unlike in, say, PHP, where types are expressly dynamic by design. The ambiguity in the use of the term "strong typing", and the nature of the term "static typing", is not relevant in type theory. Such ambiguity or ability to subvert static typic only exists in real, practical programs, such as in the example you give (e.g. casting pointers and datatypes at the potentially arbitrary whims of the programmer in C). It comes from the fact that real programs deal with actual binary data, instances of types in real programs are ultimately always realised as a binary encoding of whatever abstract thing they represent, and thus one can "translate" freely between different types by re-interpreting the underlying binary encoding. To give a simple example, one can "translate" between signed integers and unsigned integers by e.g. doing int x = -7; void* p = (void*)(&x); unsigned int y = *(unsigned int*)p; printf("%d", y); // prints '4294967289', assuming `int` is 4 bytes/32 bits But type theory is more abstract than this. In pure type theory, there is no notion of translating/re-interpreting an instance of one type as an instance of another. This is why we have tailor-made languages and apps like Agda and Coq which are specifically designed for applications of type theory and for performing computer-assisted proofs. The likes of Agda are not only statically typed like C, but they are _completely, definitively_ statically typed, unlike C, in the sense that there is _absolutely no way_ to subvert the type system; casting between types is not a feature.

@@JivanPal but you're just describing strong typing. Static typing means there's type checking done at compile time, dynamic typing means done at runtime (languages can also do both or neither). Strong typing means you can't do "bad things" with types, and is somewhat ambiguous across languages because different languages define "bad things" differently, and define the bar for whether the language is strong as a whole differently: does it need to be completely, provably strong in all situations? Is there an exception for "unsafe" tagged code? Writing to /proc/self/mem? The programmer doing things the language hasn't defined?

but... can you prove it?

no

Proof and models are the bread and butter of mathematics

@@LKRaider and if you eat nothing but bread and butter for every meal you wouldnt be very healthy

Proofs are nothing but programs. Theorems are nothing but types. Simplification of proofs is nothing but evaluation (running) of programs. Type Theory is the grand unified theory of computation and can be a solid basis for all of mathematics*.

It's oe of the key artifacts / show elements of Computerphile. I wonder where they get those.

@@hrclful probably by raiding the university museum archives! j/k

Yes that’s the plan. There is already one video on Agda on the channel now and another one being prepared.

@@ThorstenAltenkirch awesome! Glad to hear!

There's something similar that's used to find people lost at sea. It's based on Bayesian updating.

The Univalence principle, in combination with this work by Martin, can be used to rebuild the whole foundation of mathematics!

Sorry Muhammad. If you have some time you can listen to my lectures which are linked in the comments. Also I am always happy to answer questions.

@@ThorstenAltenkirch Thanks a lot for reply. It was just on a lighter note. I have seen your channel. Will watch your videos.

Don't get too carried away with functors and monads in such languages! In the likes of C++, you can almost always implement things more simply/cleanly by using e.g. `null` in place of `std::optional.empty` to indicate an error state, thereby removing a layer of encapsulation.

@@JivanPal lol

@@jawad9757 double lol

@@JivanPal by using null pointers, you get rid of all of the safety afforded by optional types

A decidable proposition is the same as a Boolean and equality of Booleans is trivial. Maybe this helps?

It makes it more difficult to put errors in empty files because you actually have to think about your domains. You can't to things like 1/0*8+'Batman'. But it makes your code easier to read, which makes it easier to maintain. With functional programming, the code often looks declarative rather than procedural. DSLs are _supposed_ to be declarative. But as my example above shows, untyped functional programming has no guarantee that the code does what you expect. As much as Matlab scripters hate it: Strict type checking is your friend.

@you- tube Programming is a fundamentally inhuman activity: There are no "happy accidents", you have to be diligent, consider all that can go wrong, and the feedback is mostly being shown your mistakes. And yet, programmers say that it is the most fun you can have with your clothes on (clothes not mandatory). As Shannon Garrity once observed: Programmers are not human.

No, Martin-Löf type theory doesn't have inheritance. Technically speaking, the type of prime natural numbers is not a sub-type of the natural numbers. The prime numbers type is modelled as a so-called Sigma type, also called a dependent pair type, that is a type containing pairs, where the type of the second entry may depend on the value of the first one. In the case of prime numbers, the first entry is the natural number to be a prime. The second entry is a proof (as explained in the video, that is a program) that in one way or another proves that the number is in fact prime. If the number is not a prime, no such proof can exist, and therefore, there is no pair containing it. One can prove that all possible proofs of prime-ness _of the same number(!)_ are equal. So the second entry of a such a pair provides no information beyond its existence. And that is what justifies talking about primes being a sub-type of the naturals in some textbooks. So, technically, there are no sub-types, but practically, there are. Another kind of de-facto sub-types is inclusion functions. If there's an injection function _inc_ that maps Nat to Int preserving everything interesting like operations and such, formally correct, it would be a monomorphism, we can look at Nat as if it were a sub-type of Int. Even programming languages are often smart enough to figure out where to insert the injection function: if z : Int and n : Nat, then z-n actually is z-inc(n) as minus is only available for Int. Then there's the type _Type,_ the Universe that “contains” the types. It is itself a type and it's objects are, well, types. So 1 : Nat, and Nat : Type. But Type cannot be of type Type, that would lead to inconsistencies. So instead of having one Universe, type theory requires an infinite hierarchy of Types, usually labelled Type0, Type1 and so on, where Nat : Type0 and Type0 : Type1 and Type1 : Type2 and so on. As far as I know - and please do _not_ take my word alone for it, those Universes are cumulative, so Nat : Type1, too. So smaller Universes are truly sub-types of larger Universes. Inheritance as in C# and Java isn't something commonly found in dependent type theories. That's a very different branch of type theory. Unfortunately, they're named similarly, but don't have too much in common.

I think sun typing is a notational convention. There is an embedding for example from natural numbers to integers and whenever you need an integer but only have a natural number you insert it automatically. However organising these embedding a effectively is certainly a non-trivial task. However it shouldn’t be at the core of a type system but in a component we call elaboration.

@@ThorstenAltenkirch Yes. There's also an embedding from the primes as defined in my comment above to the naturals: just take the first entry of the pair.

"Speak softly but make a severe dent in type theory" - Theodore Roosevelt

would you say this is not your .... type of thing?

Yes, I feel your pain.

if there is a chair on the left side, AND...

Or use a mirror!

When he said there are multiple ways representations of equality within types, I also thought of that as well as Turing's theorem about computation. Basically there are multiple ways computer programs can be represented while producing the same output, under what aspects are such two program considered 'equal' or 'identical'? All these theorems Goedel and Turing are at least related to or affecting each other. On a wider scale you can apply this to scientific theories as well. Consider two scientists coming up with an equal theory, but either use a completely different language or vocabulary to represent the same thought, even use different ways or methods of proof. Who gets credited for the discovery? Its always mind blowing how much uncertainty arises when asking questions about 'equality' or 'identity'...

Yeah. I was screaming that question to my screen during the video 😂 In particular: What does it mean for a program to prove something. Or programs to be considered "equal".

Check out Agda which is also used in the Type Theory lectures which are linked in the description.

Also Idris language

🍎 != 🍊

Yes, indeed. Because you cannot observe so much from a mere type. If you add more structure then you can distinguish more. E.g. not all groups with a fixed number of element are the same.

@@ThorstenAltenkirch does it mean only bijective groups are provably equal then?

@@LKRaider no why? I mean ok a commutative group will not be equal to a non-commutative group but certainly two non-commutative groups can be isomorphic and hence equal.

There's a link in the description

IMO the best way to learn it is to learn a language like Haskell that leans on types heavily.

@@empathogen75 Dependent types are key to type theory, which Haskell doesn't have; or, more precisely, Haskell built up a very complicated non-dependent type system, then recently started to add dependent types, resulting in a big confusing tangle of features. Dependent types are actually much simpler than Haskell (e.g. there's no distinction between terms and types!). Hence I'd recommend Agda or Idris for this sort of thing, rather than Haskell.

J programming language.

(How) are category theory and type related?

The same as two programs being equal.

Or... Type Theory.

It is called univalent foundations.

Yeah, subtitles would be of help, even more so for non-native english speakers.

p, q, a, b ... erm yes, I heard of those...

Nah. That's just a continuation type.

In Agda, you can prove it by default, too, because it has the K axiom (vaguely similar to J from the video, but lets you prove UIP). But you can add the flag --without-K, and then you can't prove UIP anymore.

Many systems can have UIP as an axiom (or something equivalent, like K). That was quite popular, since it made some proofs easier (hence why Agda has this, and apparently Idris too). There was no reason *not* to have UIP; until univalence came along, which is incompatible with UIP. That's when people started using the '--without-K' option in Agda :)

I wonder if that design choice comes down to the difficulty of efficiently implementing higher inductive types. Most well-known types in programming are plain inductive types which are easy to implement (little more than a discriminated union), and uip does hold for these kinds of types.

Doesn't UIP contradict Rice's lemma?

Prolog can run functions backwards (more precisely, it defines relations rather than functions, and uses search to find values related to the ones we give, whether that's an "input" or an "output"). For multi-argument functions, currying can be useful. There are also languages like Racket, which allow multiple return values; that might be useful :)

@@chriswarburton4296 hmm neato!

Not much to do with multiple arguments, they're just a single tuple argument. The real problem is you need to handle expressions that aren't injective, for example x / 4 where x is an integer will result in the same value for 4 different possible values for x. And that's an easy one.

@@SimonBuchanNz Yep. Prolog (and related systems, like Kanren) handle this by returning multiple values (or a set/stream of values, if you prefer). I know Prolog's resolution algorithm relies on first-order logic, and wouldn't work in a higher-order logic like type theory. For example, in type theory we cannot ask 'does value V have type T?' (unlike set theory, where 'is element of' is a predicate which can be true or false). Instead, we would have to make an encoding of type theory, perform our search using that encoded form, then 'decode' the result back to a normal type theory value. This latter 'decoding' step is a challenge, since it would either introduce inconsistency, or incompleteness. Fascinating idea though!

@@chriswarburton4296 do you have more details of that encoding/decoding of type theory?

Equality should identify objects that behave the same way. You need groupoids to handle this sort of equality for types.

I did Kerninformatik (core informatics) for 4 Semesters....also had no idea.... Learned it all later in my second try ! turns out there is nothing to calculate, it's all about defining things or recognizing how things fit into defnitions....

Since proofs are programs it reduces to the question wether two programs are equal.

Category and Type Theory work very well together. Groupoids are categories where every morphism is an isomorphism. However to model types properly you need higher categories: types are weak infinity-1 groupoids.

@@ThorstenAltenkirch thanks 😊

No

@@roman-fo2sk Which is a type of theory.

Are you familiar with the types in programming languages? It is like that, except as an alternative foundation (or, family of foundations) of math. You talk about types, and terms that belong to types, and how, given some terms of some types, how you can construct some other terms of other types (or of the same types), and things like that.

Indeed, sorry for not saying more due to lack of time. We like to identify objects which behave the same even though they are defied differently. This is important both in Mathematics and in Computer Science. The equality in the groupoid model gives you this.

@@ThorstenAltenkirch thank you for your specifying. The sense of the video now became more clear

The thing is that, the equality mentioned here is named "propositional equality", which is like "equal for what we care about". If You Say "two things are equal if there is a bijection between them" then sure enough, there is a proof that N and Z are equal. But they are NOT equal if You take bijections that respect adition for example. The set of real numbers and the Interval (0, 1) are equal in terms of topological properties. But they are NOT equal as metric spaces. One is bounded and the other isn't

It’s just theory stuff, but the properties of operations like commutativity and associativity might be useful to know if you want to define operations on types you have made. E.g say you have a type for a stack of chairs, you could define an operation of syntax x

He deals with propositional logic which has a certain syntax that he uses so you’d need to know that for the video. This isn’t programming at this point.

Basically it’s relying on computer science theory so if you haven’t studied it will be gibberish

I also don’t think it’s explained too well and his hand gets in the way

Type theory is deep in figuring out whether the people who specified a programming language did a good job. It's not a tool like a hammer, but rather something like a training method for people who inspect hammer factories. A proof that an implementation of JavaScript doesn't have any optimizations that introduce security vulnerabilities could be in type theory, for example.

Type theory