The Hardest Problem in Type Theory - Computerphile
ฝัง
- เผยแพร่เมื่อ 29 ก.ค. 2021
- Equality sounds a straightforward idea, but there are subtle problems in theoretical computer science. Professor Thorsten Altenkirch explains how his late friend Martin Hofmann solved one of the biggest problems.
More of Thorsten on Type Theory: bit.ly/C_Thor_playlist
Thorsten's paper dedicated to Martin: bit.ly/C_Thor_Paper
/ computerphile
/ computer_phile
This video was filmed and edited by Sean Riley.
Computer Science at the University of Nottingham: bit.ly/nottscomputer
Computerphile is a sister project to Brady Haran's Numberphile. More at www.bradyharan.com
![LISA - ROCKSTAR (Official Music Video) REACTION [SHE'S BACK!]](http://i.ytimg.com/vi/QBxE30vavMQ/mqdefault.jpg)
RIP Martin Hoffmann :( Very sad story.
He was my professor, so it hit us students hard.
you know the camera guy is lost when he hasn't said a word for 20 min straight!
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?
You made me cry the first two seconds. He was supposed to be my bachelor's thesis advisor, but went missing before we got started. Such a loss for the world.
I'll never go hiking alone.
"people at the time when this was a problem said, oh yeah it's easy, we can do it and then went away and said oh hang on it doesn't work" so many problems are underestimated like this.
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.
Please, enable automatic subtitles. Non English speakers have a hard time understanding this man accent, and subtitles help a lot.
6:37 Iconic: "… because I am a computer scientist, ja." 🤘
Canonical, jawohl!
Loved this! More Type Theory please!
I agree.
I'd like that, too, but explained a bit better.
“If I replace both with refl, so I have to prove that relf is equal to refl then i refl”
rofl
When one knows the depth that this professor knows, it is irrelevant which side goes outside on your tee-shirt.
😭😭😭
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
Prof T always has amazing explanations. RIP M Hofmann. Will be happy to see more about type theory on here.
I think I was following along right up until the Professor started talking.
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
I've been working on a programming language where equality of types etc are necessary (for example, are two state machines equal even if they are encoded differently), and this video was very beneficial to my research. When you mentioned how a simple boolean can be encoded in different ways, it made me feel like there is information about what I'm looking for already out there and that I'm not in some obscure dead zone that hasn't been entered before.
(edit: I probably phrased this comment very badly haha)
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 studied the intuitionist Martin-Löf type theory in a course this year, it's really interesting but so obscure argument that few know.
I would like other videos about this topic
So sorry for Martin Hoffmann.
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
interesting way to frame problems, as a programmer I'm used to thinking in the context of math or object related sets, but this looks like an interesting means of standardizing a mixture of the two to kind of more directly reason about it, and specifically a more direct means of incorporating logic through proofs
When it comes to understanding formal systems and the limitations of proofs you can't do much better than "Gödel, Escher, Bach: An Eternal Golden Braid" by Douglas R. Hofstadter. Everyone interested in math, computers, science, or philosophy should read this classic (or at least as much of it as you can before the binding disintegrates). It will change how you see everything and inculcates a true appreciation for the challenges we face in obtaining that elusive thing we call "truth."
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.
Computerphile videos with Thorsten Altenkirch from 2017 make me seriously interested in homotopy type theory and type theory in general. So I want more videos about this subject on this channel.
PS. I still try to crack syntax of type theory.
His channel has more in-depth content!
This is the type of presentation that motivates the viewer to want to learn more. Excellent Professor Altenkirch!
This provides some context to homotopy type theory since fundamental groupoids can be used
can be used ... what?
I know that I'm kind of nitpicking, but I really wanted to say something; "strong typing" is not a well-defined term, and Professor Torsten probably should've used the term "static typing" instead.
Static typing is when variables have set types, dynamic typing is when they don't. These are both well-defined and understood terms.
Strong typing and weak typing have no real definitions, for instance I'd argue C is weakly typed because you can bypass the type system entirely with void pointers, while I could say Python is strongly typed because while its types are dynamic, they're strictly adhered to and nothing gets implicitly converted to another type.
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?
I actually think this is the best video you've ever done. Prof Thorsten described it perfectly in a very easy to understand manner.
but... can you prove it?
Doing Math with numbers? easy. Doing math with letters? okay. Doing math with symbols? hard. Doing maths with mathematical proofs? Blowing my mind ^^*
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 clicked for me, thanks for the explanation
Looks like Professor Altenkirch has lost a lot of weight! Good for him!
This solution is beautiful, I love it!
A buddy of mine did a project on mathematically modelling where lost hikers would be likely to go over time. For a second I thought it was heading that direction.
There's something similar that's used to find people lost at sea. It's based on Bayesian updating.
I like how he didnt forget to return control after the sad story
Great video! I also like how Thorsten used continuous form paper during his explanation.
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
I tried to follow this, but I think my expression after it is...what?
I would love a few videos breaking this all down step by step. Fingers crossed!!
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!
Understood about 1% of it. Loved it!
The only thing I learned is that Prof. Martin was a brave genius because he worked on something which I could not understand the heck about it ...
Edit: And that something is related to types ...
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.
More like this please. I am a software engineer, not a computer scientist, so it is nice to see some of the theoretical underpinnings (I was blown away when I discovered monads and even more blown away when I found C++17 supported them - std::optional is the Maybe monad and now I use it all the time for operations that can fail like DB lookups etc.)
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
Thanks awesome video
I know a bit more about this but am still mesmerized by Hedberg's theorem. Why do identity proofs become unique when your Type is discrete?
A decidable proposition is the same as a Boolean and equality of Booleans is trivial. Maybe this helps?
Great video, but I couldn't really grasp the importance/impact of the solution to this problem. Like, what are consequences of this?
The Univalence principle, in combination with this work by Martin, can be used to rebuild the whole foundation of mathematics!
Awesome!
On a side note, Per Martin-Löf's type theory can actually be programmed. Maybe that was the goal from the 80'ties when they sought a real programmable logic (without cuts etc)? And, in a way, that would solve programming as "what" rather than "how". It would also make programs more of proofs than sequences of instructions. But for an ordinary programmer, programming in type theory is hard. Much harder than one would like it to be.
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.
Sadly this passes way above my head, and I can feel how this part of CS is Not My Kind Of Thing. Happy to see the dress code of professors to be spreading around though!
"Speak softly but make a severe dent in type theory" - Theodore Roosevelt
would you say this is not your .... type of thing?
Pro tip for the cameraman: if someone is right handed, film from the left side.
if there is a chair on the left side, AND...
Or use a mirror!
My favourite! nice explanation, very Interesting Topic
also
9:00 computer lagging a little
RIP Martin. Great tribute to him, and video guys.
"I just wanted to understand types, now I'm learning about ∞-groupoids, (∞,1)-categories of (∞,1)-toposes, n-homotopies, n-truncation, higher Isbell duality...
Where did my life go so wrong..?"
Yes, I feel your pain.
"Thorsten's just this guy, you know".
How do you write the programs? What do they look like?
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
''You see I Start with zero, because I'm a computer scientist'' xD
I wish there were subs
Does anyone have a MOOC or textbook they would recommend to learn more type theory?
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 type theory opens a new way of doing math. Really love it. This new math could have a cool name like: Mathoid or Algomath or Quantumath.
Or... Type Theory.
It is called univalent foundations.
Loving the inside out shirt.
what does it imply to proof statements about proofs themselves?
Getting huge Godel's Incompleteness Theorem vibes halfway through this video. Are the concepts connected?
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'...
I really struggled to get what this was about. I feel like maybe too much was lost in "not trying to give too much detail about [XYZ]..." Maybe I have just missed some videos that would give background info but this one really lost me.
Please add captions !
The hardest problem: time travel in type theory
Nah. That's just a continuation type.
I really tried but there are a number of places where I just cannot parse the sounds I'm hearing into sensible sentences. Can't tell if it's the topic that's confusing or just missing information cause I'm bad at parsing unclear vocalizations (though likely some of both). But please make correct subtitles if you can. :)
Yeah, subtitles would be of help, even more so for non-native english speakers.
What does it mean for to proofs to be equal? Only that they prove the same thing?
I have no idea what I'm watching but I love it. If I get the chance to take type theory I'll make sure to get some basics then come back to this.
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....
So, your type theory doesn't have inheritance? It was stated that once an entity was typed that it wouldn't be of another type... In C#, my string is still an "Object" type...
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.
Interestingly in Idris you can prove uniqueness of equality proofs.
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?
RIP Martin Hofmann
Wait, so does this mean that ANY type that has the same finite number of elements or has a 'countably infinite' number of elements is the same type?
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.
Any time I’m starting to feel smart, I watch something like this. Problem solved.
If only this video had captions...
Wish I understood this better
Doesn't it means we should try to define:
Relative Equality of types
Maybe we need a set of relative equalities, containing the 1 to 1 projection as the tool for a specific relative equality.
I guess we move from discussion of the equality property of the set, to the projection quality of the set.
I know what most of these words mean on their own...
p, q, a, b ... erm yes, I heard of those...
What does it mean for two proofs to be equal?
The same as two programs being equal.
NIce
Are you saying that we should only compare apples to apples and there are more than one apple around?
🍎 != 🍊
it would be so much easier if functions/statements could be executed backwards to be absolutely sure that there's a 1 to 1 correspondence between types. It seems like there's a chance that if 2 different functions are used, it may result in a completely different type. If functions/statements use multiple arguments, it's then impossible to have the original arguments when run forwards then backwards, we may only obtain a range of valid arguments in which the original arguments can be found...
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?
If only the camera was to the left of professor so he wouldn't obstruct what he was writing with his hand.
R. I. P. Martin Hofmann
I am always confused when somebody elaborates on whether one proof is equal to another proof.
Since proofs are programs it reduces to the question wether two programs are equal.
How does this relate to category theory? 🤔
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 😊
RIP.
So im just seeing this video 2 weeks after it launched. Of the 2 mio suns, you haven't even gotten 70k views. I was aware that TH-cam was suppressing independent news but is this now also affecting informational videos?
Hmm. I approximately followed until the ending - it’s not clear to me what the significance of this result is.
Equality should identify objects that behave the same way. You need groupoids to handle this sort of equality for types.
What is type theory
@@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.
RIP Martin Hoffman.
his shirt though
The Caps Lock.
The Hardest Button to Button: uh oh!
Is the shirt inside out?
No
Would love if video had captions 🙁 It's too hard for me to understand what's being said at times
o'course they are the same as they are infinitely countable, and they are also the same as Rationals
this is a level of abstraction that I'm not comfortable with
they had us in the first half ain't gonna lie
He looks like Bradd Pitt lol...
SUBTITLES
Germo just like me
what is he talking about
Type theory
I have trouble following the video after an intro like that.... yeah, some people are just too brave
is it just me smelling the black marker?
I know some of these words..
Type Theory :
So What's your Type?
Brunette ...
hello torsten, I think you did a good job at introducing type theory and presenting that problem. Martin Hofmann 1965 - 2018.
/cse-student, gothenburg
IM STRAIGHT SLEEPINK!!! 35yr young here.
But... those are different kinds of equality? You cannot prove ℕ = ℤ, because they are different (irreducible) symbols. You cannot find an a such that refl a : ℕ = ℤ. Now, bijection is a totally valid and useful notion of equality, but it is not the same as the basic refl-only kind.
That said, I'm sure I'm misunderstanding something. I've been dabbling in Type Theory for maybe a year; he has been actively involved in research for much longer.
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
everything seems to be clear, but in fact I did not understand anything (the deep meaning of this whole video), especially what is the practical application of this all, even if it was possible to prove it
P.S. Maybe we just need a lot of good examples?
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
So 3 is of type natural and not of integer type? Since it cannot have more than one type...
Isn’t that basically a typed version of rice-Shapiro?