<div dir="auto"><div dir="auto">I'll admit I have a high bias towards research mathematics, so maybe unintentionally I gave an advice more fitting to people who want to work in theoretical mathematics.</div><div dir="auto"><br></div><div dir="auto">Large portion of my message came from conversations I had with Kevin Buzzard, so it is indeed far from applications in actual programming languages (±PoC languages, logic languages, and the rest of the PV gang).</div><div dir="auto"><br></div><div dir="auto">One thing I'll stand by is the study of formal logic, apart from the fact I believe it is generally helpful to learn it does appear in everyday situations, especially for someone who is interested in the inner workings of a type theory.</div><div dir="auto"><br></div><div dir="auto">For example, to understand how to derive identities purely from the method signature (see [1]).</div><div dir="auto"><br></div><div dir="auto">I'm not saying that you should learn how Type theory embeds with logic, but understanding FOL is definitely someone one should at least study when they enter type theory.</div><div dir="auto"><br></div><div dir="auto">[1] "Theorems For Free!" By F. Wadler <a href="https://dl.acm.org/doi/pdf/10.1145/99370.99404">https://dl.acm.org/doi/pdf/10.1145/99370.99404</a></div><div dir="auto">(The link is directly to the pdf, so if you prefer not to download from a mail, quick search for "Theorems For Free!" Will find it)</div><div dir="auto"><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Mar 29, 2023, 23:50 Tesla Zhang <<a href="mailto:ice1000kotlin@foxmail.com">ice1000kotlin@foxmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>Hi, </div><div><br></div><div>I am going to argue against formal logic, universal algebra, ring theory, category theory, and HoTT. I am doing so because I was told similarly before and I was scared away from learning type theory. It's great to learn things in general, but the prerequisites are not _that_ large.</div><div><br></div><div>I do not think you need to know formal logic well to learn type theory. You only need the notations. Modern presentations only use a very simple subset of it to express the typing derivation, say, you only need to know what does turnstile mean, what is Gamma, and what does the big horizontal line mean. That's literally it.</div><div><br></div><div>Universal algebra provides a categorical interpretation of algebraic data types with equations, but I would argue that they're going too far. In Java (and similarly weak type systems like Haskell) we're only talking about pattern matching, you don't have any equations. I'm also confused about ring theory, because it seems unrelated to type theory. </div><div><br></div><div>Category theory in this context usually provides a framework of working with semantics and I'd argue that it's not required to learn basic type theory. The category theory used to study type theory is also very advanced, so the intro level things won't help. The same applies to HoTT, it's just too far from programming and type theory itself. Unless you're interested in (infinite, 1)-topoi and their internal languages, I would argue that these shouldn't be required.</div><div><br></div><div><hr style="margin:0 0 10px 0;border:0;border-bottom:1px solid #e6e8eb;height:0;line-height:0;font-size:0;padding:20px 0 0 0;width:50px"><div>Regards,<br>Tesla</div></div><div><div style="font-size:12px;padding:2px 0">---Original---</div><div style="font-size:12px;background:#f0f0f0;color:#212121;padding:8px!important;border-radius:4px;line-height:1.5"><div><b>From:</b> "Holo The Sage Wolf"<<a href="mailto:holo3146@gmail.com" target="_blank" rel="noreferrer">holo3146@gmail.com</a>></div><div><b>Date:</b> Wed, Mar 29, 2023 02:10 AM</div><div><b>To:</b> "Tesla Zhang"<<a href="mailto:ice1000kotlin@foxmail.com" target="_blank" rel="noreferrer">ice1000kotlin@foxmail.com</a>>;</div><div><b>Cc:</b> "amber-dev"<<a href="mailto:amber-dev@openjdk.org" target="_blank" rel="noreferrer">amber-dev@openjdk.org</a>>;</div><div><b>Subject:</b> Re: 2 questions about enums and the closed/withdrawn JEP 301</div></div><br><div dir="auto"><div>This is highly depends on how theoretical you want to get.</div><div dir="auto"><br></div><div dir="auto">If you are only interesting in the practical results then typed lambda calculus and friends (e.g. lambda-mu-calculus, system U) as well as type system themselves (e.g. lambda-cube, Pure Type System).</div><div dir="auto"><br></div><div dir="auto">To truly understand everything you would probably also need to learn some Formal Logic (some would argue that Category theory is also necessary, but I from my experience this is an over estimate of how important the theoretical ideas to the practical)</div><div dir="auto"><br></div><div dir="auto">The more theoretical you want, the more prerequisite will be, but generally to study the theoretical side of type theory you want to know Formal Logic very well, to have a good understanding about universal algebras and algebra subject in general (Category theory, ring theory), and having at least some understanding in set theory (specifically about the foundational side) (although there are some great type theorists who definitely skipped the set theory step, I think that skipping it is not a good idea. I'm also a set theorist, so maybe I'm biased)</div><div dir="auto"><br></div><div dir="auto">If you want to go into the really deep end of type theory, knowing foundational alternatives like HoTT is also needed.</div><div dir="auto"><br></div><div dir="auto"><div class="gmail_quote" dir="auto"><div dir="ltr" class="gmail_attr">On Wed, Mar 29, 2023, 08:03 Tesla Zhang <<a href="mailto:ice1000kotlin@foxmail.com" target="_blank" rel="noreferrer">ice1000kotlin@foxmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="border-left:1px solid rgb(204,204,204);margin:0px 0px 0px 7.18435px;padding:14px 16px 14px 8.98044px;color:rgb(149,149,149);background-color:rgb(245,246,250)"><div>Hi David,</div><div><br></div><div><br></div><div>My guess would be the following subjects:</div><div><br></div><div>+ (Typed) lambda calculus (prerequisite)</div><div>+ Basic type theory. You need to know how the type system is defined formally</div><div>+ Subtyping in terms of type theory, such as System Fsub</div><div><br></div><div>Type theory is a very interesting yet extremely hard area of research, though I personally find it very enjoyable. But again, don't fully trust me, maybe other experts have better suggestions :)</div><div><br></div><div><hr style="margin:0 0 10px 0;border:0;border-bottom:1px solid #e6e8eb;height:0;line-height:0;font-size:0;padding:20px 0 0 0;width:50px"><div>Regards,<br>Tesla</div></div><div><div style="font-size:12px;padding:2px 0">---Original---</div><div style="font-size:12px;background:#f0f0f0;color:#212121;padding:8px!important;border-radius:4px;line-height:1.5"><div><b>From:</b> "David Alayachew"<<a href="mailto:davidalayachew@gmail.com" rel="noreferrer noreferrer" target="_blank">davidalayachew@gmail.com</a>></div><div><b>Date:</b> Tue, Mar 28, 2023 23:26 PM</div><div><b>To:</b> "Brian Goetz"<<a href="mailto:brian.goetz@oracle.com" rel="noreferrer noreferrer" target="_blank">brian.goetz@oracle.com</a>>;</div><div><b>Cc:</b> "amber-dev"<<a href="mailto:amber-dev@openjdk.org" rel="noreferrer noreferrer" target="_blank">amber-dev@openjdk.org</a>>;"Tesla Zhang"<<a href="mailto:ice1000kotlin@foxmail.com" rel="noreferrer noreferrer" target="_blank">ice1000kotlin@foxmail.com</a>>;</div><div><b>Subject:</b> Re: 2 questions about enums and the closed/withdrawn JEP 301</div></div><br><div dir="auto"><div>Hello Brian,<div dir="auto"><br></div><div dir="auto">Thank you for your response!</div><div dir="auto"><br></div><div dir="auto">> F-bounds are weird-looking at first:</div><div dir="auto">> </div><div dir="auto">> abstract class Enum<T extends Enum<T>> { ... }</div><div dir="auto">> </div><div dir="auto">> in part because it's not always obvious</div><div dir="auto">> what "T" means at first. We're used to</div><div dir="auto">> seeing type variables that represent</div><div dir="auto">> element types (List<T>), or result types</div><div dir="auto">> (Supplier<T>), but this T really means</div><div dir="auto">> "subclass". If it were written</div><div dir="auto">> </div><div dir="auto">> abstract class Enum<Subclass extends Enum<Subclass>></div><div dir="auto">> { Subclass[]</div><div dir="auto">values(); }</div><div dir="auto">> </div><div dir="auto">> it would already be clearer. </div><div dir="auto"><br></div>This clarified the F bounds fully, thank you. Thinking of a type parameter as a sort of subclass is something I never thought of before. I see how it applies and works here though.</div><div dir="auto"><br></div><div dir="auto">> You might first try writing it as<div dir="auto">> </div><div dir="auto">> abstract class Enum<Subclass> { ... }</div><div dir="auto">> </div><div dir="auto">> but this permits extension in unexpected</div><div dir="auto">> ways:</div><div dir="auto">> </div><div dir="auto">> class FooEnum extends Enum<String> { ... }</div><div dir="auto">> </div><div dir="auto">> You could try refining it as</div><div dir="auto">> </div><div dir="auto">> abstract class Enum<Subclass extends Enum> { ... }</div><div dir="auto">> </div><div dir="auto">> but this still permits</div><div dir="auto">> </div><div dir="auto">> class FooEnum extends Enum<BarEnum> { ... }</div><div dir="auto">> </div><div dir="auto">> What we're trying to express is that the</div><div dir="auto">> type argument of Enum *is* the class</div><div dir="auto">> being declared. Which is where the</div><div dir="auto">> f-bound comes in:</div><div dir="auto">> </div><div dir="auto">> abstract class Enum<Subclass </div><div dir="auto">> extends Enum<Subclass>> { Subclass[]</div><div dir="auto">values(); }</div><div dir="auto">> </div><div dir="auto">> which can only be satisfied by a</div><div dir="auto">> declaration of the form</div><div dir="auto">> </div><div dir="auto">> class X extends Enum<X> { ... }</div><div dir="auto"><br></div><div dir="auto">I had had a discussion with someone long ago [1], arguing over whether or not T extends Something<T> is meaningfully different from T extends Something<?>. I now see the difference. It communicates what the only type permitted should be.</div><div dir="auto"><br></div><div dir="auto">> The first few times you look at it, it seems</div><div dir="auto">> weird and magic, and then at some point</div><div dir="auto">> it seems obvious :)</div><div dir="auto"><br></div><div dir="auto">Yeah, I can definitely feel the gears turning lol.</div><div dir="auto"><br></div><div dir="auto">Let me ask though, is there a formal name for these type of relationships? I have seen in other discussions things like L types or Q types on Valhalla. Maybe they are entirely unrelated. Moreso my question is, is there some formal name that captures this type of relationship or logic?</div><div dir="auto"><br></div><div dir="auto">For example, if I want to learn integrals, I would need to first understand derivatives, how they play with that E shaped summation thing, then learn antiderivatives, and then I can learn about integrals. However, if I look up Calculus, I get a nice overhead view of each of these components, allowing me to learn one after the other until I can understand. Googling calculus is all I need to be able to learn everything I need to understand integrals.</div><div dir="auto"><br></div><div dir="auto">Is there a similar blanket term that covers this type of logic? I understand f bounded types now, but I want to learn about other relationships like this and don't really know the parent term they fall under.</div><div dir="auto"><br></div><div dir="auto">Thank you for your time and help!</div><div dir="auto">David Alayachew</div><div dir="auto"><br></div><div dir="auto">[1] = <a href="https://stackoverflow.com/a/70504547" rel="noreferrer noreferrer" target="_blank">https://stackoverflow.com/a/70504547</a></div></div></div>
</div></blockquote></div></div></div>
</div></blockquote></div>