2 questions about enums and the closed/withdrawn JEP 301

[Holo The Sage Wolf]

This is highly depends on how theoretical you want to get.

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

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)

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)

If you want to go into the really deep end of type theory, knowing
foundational alternatives like HoTT is also needed.

On Wed, Mar 29, 2023, 08:03 Tesla Zhang <ice1000kotlin at foxmail.com> 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/bf13ff13/attachment-0001.htm>