2 questions about enums and the closed/withdrawn JEP 301

[Tesla Zhang]

Hi David,




My guess would be the following subjects:


+ (Typed) lambda calculus (prerequisite)
+ Basic type theory. You need to know how the type system is defined formally
+ Subtyping in terms of type theory, such as System Fsub


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 :)



Regards,
Tesla

---Original---
From: "David Alayachew"<davidalayachew at gmail.com>
Date: Tue, Mar 28, 2023 23:26 PM
To: "Brian Goetz"<brian.goetz at oracle.com>;
Cc: "amber-dev"<amber-dev at openjdk.org>;"Tesla Zhang"<ice1000kotlin at foxmail.com>;
Subject: Re: 2 questions about enums and the closed/withdrawn JEP 301


Hello Brian,

Thank you for your response!


> F-bounds are weird-looking at first:
> 
>      abstract class Enum<T extends Enum<T>> { ... }
> 
> in part because it's not always obvious
> what "T" means at first. We're used to
> seeing type variables that represent
> element types (List<T>), or result types
> (Supplier<T>), but this T really means
> "subclass".  If it were written
> 
>      abstract class Enum<Subclass extends Enum<Subclass>>
> { Subclass[]
values(); }
> 
> it would already be clearer. 


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.


> You might first try writing it as> 
>      abstract class Enum<Subclass> { ... }
> 
> but this permits extension in unexpected
> ways:
> 
>      class FooEnum extends Enum<String> { ... }
> 
> You could try refining it as
> 
>      abstract class Enum<Subclass extends Enum> { ... }
> 
> but this still permits
> 
>      class FooEnum extends Enum<BarEnum> { ... }
> 
> What we're trying to express is that the
> type argument of Enum *is* the class
> being declared.  Which is where the
> f-bound comes in:
> 
>      abstract class Enum<Subclass 
>      extends Enum<Subclass>> { Subclass[]
values(); }
> 
> which can only be satisfied by a
> declaration of the form
> 
>      class X extends Enum<X> { ... }


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.


> The first few times you look at it, it seems
> weird and magic, and then at some point
> it seems obvious :)


Yeah, I can definitely feel the gears turning lol.


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?


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.


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.


Thank you for your time and help!
David Alayachew


[1] = https://stackoverflow.com/a/70504547
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/amber-dev/attachments/20230329/421656ce/attachment.htm>