<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">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 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" target="_blank" rel="noreferrer">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" target="_blank" rel="noreferrer">brian.goetz@oracle.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>>;"Tesla Zhang"<<a href="mailto:ice1000kotlin@foxmail.com" target="_blank" rel="noreferrer">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" target="_blank" rel="noreferrer">https://stackoverflow.com/a/70504547</a></div></div></div>
</div></blockquote></div></div></div>