2 questions about enums and the closed/withdrawn JEP 301

[Brian Goetz]

IMO the best introduction to type theory is Pierce's _Types and 
Programming Languages_.

On 3/29/2023 12:55 AM, Tesla Zhang wrote:
> 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/b5ccb8e1/attachment-0001.htm>