Naïve Type Theory by Thorsten Altenkirch (University of Nottingham, UK)

Talk at: FOMUS 2016. For all Talks and more information, slides etc. see: fomus.weebly.com/
Naïve Type Theory by Thorsten Altenkirch (University of Nottingham, UK)
Abstract: In this course we introduce Type Theory (sometimes called "dependent type theory") as an informal language for mathematical constructions in Computer Science and other disciplines. By Type Theory we mean the constructive foundation of Mathematics whose development was started by Per Martin-Loef in the 1970ies based on the Curry-Howard equivalence of propositions and types. Because of this proximity to Computer Science, Type Theory has been the foundation of interactive theorem provers and programming languages such as NuPRL, Coq, Agda and Idris. While the calculi on which these systems are based are an important research topic, in this course we want to emphasise the "naive" use of Type Theory using just pen and paper. Indeed this is similar to the naive use of set theory which is usually applied informally without explicitly relating each constructions to the axioms of set theory (as in Halmos' book on "Naive Set Theory").
In this course we focus on the intuitive foundations of Type Theory and on basic constructions such as: universes, (dependent) function types, (dependent) products, inductive types and equality and their use in informal reasoning. If time permits we will also cover basic constructions from Homotopy Type Theory, such as the univalence axiom (isomorphism is equality), and some Higher Inductive Types (a generalisation of quotient types). A good reference for our course is chapter 1 of the book on Homotopy Type Theory (available here: homotopytypetheory.org/book/).
This workshop was organised with the generous support of the Association for Symbolic Logic (ASL), the Association of German Mathematicians (DMV), the Berlin Mathematical School (BMS), the Center of Interdisciplinary Research (ZiF), the Deutsche Vereinigung für Mathematische Logik und für Grundlagenforschung der Exakten Wissenschaften (DVMLG), the German Academic Merit Foundation (Stipendiaten machen Programm), the Fachbereich Grundlagen der Informatik of the German Informatics Society (GI) and the German Society for Analytic Philosophy (GAP).

[@neilbedwell7763]

Understanding with precision the samenesses and the differences (identities and deltas/differentials) between things was the motive for me finding my way to homotopy type theory. Stating the differences and samenesses (importantly the differences) on the *tools* of stating samenesses and differences is profoundly useful and helps people to become ambivalent to the tools that suit their needs best!

[@keithharbaugh2594]

01:55 Set theory ; 02:45 Type theory ; 03:38 What's the difference? ; 13:15 Intensional vs. extensional ; 16:22 What is a function? ;

[@neilbedwell7763]

🥳

[@mortenbrodersen8664]

Excellent talk. He covers a lot of subtle issues that deeply illustrate the difference between Set theory and Type theory.

[@neilbedwell7763]

In a past life, Thorsten was on the front line converting people from Roman Numerals to Arabic numerals 😂. 🎉 a hero and scholar.

[@johningham1880]

I would never have considered mixing computer modern with comic sans, but it sort of works

[@GRAYgauss]

Holy crap, you're right!

[@rrr00bb1]

i ran into this in the real world. say that you use a service that signs statements that it believes about you with a MAC; literally hashing strings: A=H("fname:thorsten"), etc. A is evidence that the string was hashed by our authority. (A(B ~ C)) = AB ~ AC. Where hashes are literally multiplied, and "~" means that they differ by some constant. Say that K is a secret key that we want to calculate to open a logical padlock, by storing values. (K - (AB ~ AC)) = K-AB ~ K-AC ... means that we can calculate K by adding AB to (K-AB), or adding AC to (K-AC). To handle not logic, we would need negated expressions (which are true), such as !D. That works fine because it has an actual witness value. AB and AC are "witnesses". But you get stuck when you want proof that a statement E is "missing". The certificate that a user has would be a list of statements "and" together, like: A B D E G H !M !N. We have evidence for these. But if we are asked to prove that X is MISSING from the certificate, such as X=H("DrugConviction2020"), we can easily walk the certificate to verify that X is not in the list. But we can't provide a specific witness value that calculates the key to unlock the padlock. ie: AB = 2394. AC =2300. K = 1300. case AB stores -1094 in the padlock, AC stores -1000. User must be able to supply the value of AB or AC to recover the key. This is very much like needing a witness. Because the key K must be calculated the same, no matter who the user is; We have a similar issue with general not(p) of propositions; in that we can't produce a consistent witness; unless the padlock brings the witness value with it. The intention is that the padlocks are totally public; and should not leak the values of any attributes, though they may leak what they are looking for. This is a reasonable definition of boolean logic, and it even admits a reasonable interpretation for values between 0 and 1: def and(a,b): return a*b def not(a): return 1-a def or(a,b): return not(and(not(a),not(b))) But, they lack witness information. I am definitely handling and/or/not, but the inputs are not just zero and one. With general circuits, it does not seem possible to make the user certificate provide all the witnesses required to handle NOT cases. The padlock may need to provide (ie: leak!) a witness value, to tell what to look for in the certificate. And there doesn't seem to be a way to enforce that the code honors a missing derogatory attribute from its certificate. It's not clear how to create a witness value for something proven missing from a certificate. I tried all kinds of crazy stuff. One thing was having user and padlock encode their beliefs into points on a polynomial (which amounts to polynomial neural nets for questioning witnesses), where they agree on what hashes to x, but disagree on what the y values are; and use the difference at a particular point between user (x,y) and padlock (x,y) (ie: H("DrugTest2020Pass")) answers in the polynomial. This is the first time that all this abstract gobbledygook I read in "Type Theory And Programming" made sense. Even when witnesses required to handle Not are not secrets, you can only walk the certificate (ie: an environment) to prove that the statement is "missing"; which is different from being explicitly asserted as false (giving an explicit witness value).

[@ronpanduwana8631]

Thanks. Why no subtitle though.

[@kamilziemian995]

Very interesting and enjoyable talk. Also: ja.

[@MCLooyverse]

I find the idea that "A function is a set of pairs" interesting. I must have learned enough computer science before set theory to not think of it that way, except (ironically?) for finite functions like &&, ||, !=, etc.. The way I think of a && b is as its logic table "00->0;01->0;10->0;11->1", which can be manipulated as a whole to show certain logic identities. For any other function, though, I think of it more as the way to *generate* the table (or graph), than as a lookup. Even for functions which I don't know how to calculate, I think of it like a blackbox, which hypothetically spits out values when you give it input.

[@tricky778]

It's not a lookup (unless you define the set via a lookup such as an indexed set).

[@MCLooyverse]

In set theory, we can say that ℕ ⊂ ℤ ⊂ ℝ, which encapsulates the idea that 3 :: ℕ behaves the same as 3 :: ℤ, so in some sense they are the same (and in set theory they literally are). It does seem important to be able to say that a `double` can represent the same things that an `int` can, and more.

[@tonaxysam]

Actually, in set theory they are not... In naive set theory they may actually be the same, but in ZF the "integers" are actually sets of pairs of natural numbers. So the fact that ℕ ⊂ ℤ ⊂ ℝ is not actually true (at least they are not contained inside the other as sets). But it is true that they behave in the same way. The proper way to phrase it is that there is a way to "insert ℕ into ℤ" that preserves every property of ℕ

[@fullfungo4476]

@@tonaxysamIt’s not necessarily false. You can define ℕ as the subset of ℤ that “behaves like” the set of natural numbers. This doesn’t brake any rules.

[@valshaped]

What's interesting is, it's not true that a double (64-bit float) is a superset of (64-bit) integers due to floating point precision. Any number with higher precision than the floating point format's mantissa may not be represented in the set of floating point numbers, even if it can be represented by an integer of the same width. You'll lose precision converting in either direction!

[@StephenPaulKing]

Real =/= Physical!

[@dr.c2195]

That is true. My consciousness is not physical but I am very certain that it is real. After all, I am all of me.

[@TimJSwan]

1:10:40 sounded like Musk

[@gentzen7116]

Thorsten seems to interpret "extensional" and "intensional" as some complicated, hard to explain concepts. But at least in philosophy, they were never meant to be complicated, see for example: philosophy.stackexchange.com/questions/16164/what-is-the-difference-between-intensional-and-extensional-logic. What worries me even more is that Thorsten feels that the name intentional type theory is paradoxical, and that he feels a paper by Per Martin-Löf explaining some closely related concepts would be based on some confusion. Maybe Thorsten just failed to get that people mean something utterly trivial when they say "extensional"...

[@lhpl]

I will readily admit to being stupid, but it really irritates me that I feel I almost but not just quite understand this lecture. Is there a place with a better explanation (viz. Explanation for dummies) of the Pi and Sigma thingamabobs?

[@neilbedwell7763]

​​​@@lhpl kzbin.info/www/bejne/jKmsf6KBe9JgiZY this lecture and the related book focus specifically on exploring dependent types, which is the direction for logic that here Thorsten is advocating for. (Usage of Pi & Sigma types)