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

[@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).

[@kamilziemian995]

Very interesting and enjoyable talk. Also: ja.

[@ronpanduwana8631]

Thanks. Why no subtitle though.

[@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 ℕ

[@fullfungo]

@@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!

[@TimJSwan]

1:10:40 sounded like Musk

[@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.

[@kinbolluck476]

OH GOD WHYYYY HEEELP MEEEEEEeeee

[@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)