<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<font size="4"><font face="monospace">IMO the best introduction to
type theory is Pierce's _Types and Programming Languages_. </font></font><br>
<br>
<div class="moz-cite-prefix">On 3/29/2023 12:55 AM, Tesla Zhang
wrote:<br>
</div>
<blockquote type="cite" cite="mid:tencent_9143C8068CE6E405EC9B79E7D23E12E79D0A@qq.com">
<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 class="xm_write_text_sign">Regards,<br>
Tesla</div>
</div>
<div>
<div style="font-size:12px;padding:2px 0;" class="xm_mail_oringinal_describe">---Original---</div>
<div style="font-size:12px;background:#f0f0f0;color:#212121;padding:8px!important;border-radius:4px;line-height:1.5;">
<div class="xm_mail_oringinal_describe"><b>From:</b> "David
Alayachew"<a class="moz-txt-link-rfc2396E" href="mailto:davidalayachew@gmail.com"><davidalayachew@gmail.com></a></div>
<div class="xm_mail_oringinal_describe"><b>Date:</b> Tue, Mar
28, 2023 23:26 PM</div>
<div class="xm_mail_oringinal_describe"><b>To:</b> "Brian
Goetz"<a class="moz-txt-link-rfc2396E" href="mailto:brian.goetz@oracle.com"><brian.goetz@oracle.com></a>;</div>
<div class="xm_mail_oringinal_describe"><b>Cc:</b>
"amber-dev"<a class="moz-txt-link-rfc2396E" href="mailto:amber-dev@openjdk.org"><amber-dev@openjdk.org></a>;"Tesla
Zhang"<a class="moz-txt-link-rfc2396E" href="mailto:ice1000kotlin@foxmail.com"><ice1000kotlin@foxmail.com></a>;</div>
<div class="xm_mail_oringinal_describe"><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" moz-do-not-send="true" class="moz-txt-link-freetext">https://stackoverflow.com/a/70504547</a></div>
</div>
</div>
</div>
</blockquote>
<br>
</body>
</html>