2 questions about enums and the closed/withdrawn JEP 301

[Tesla Zhang]

Hi, 


I am going to argue against formal logic, universal algebra, ring theory, category theory, and HoTT. I am doing so because I was told similarly before and I was scared away from learning type theory. It's great to learn things in general, but the prerequisites are not _that_ large.


I do not think you need to know formal logic well to learn type theory. You only need the notations. Modern presentations only use a very simple subset of it to express the typing derivation, say, you only need to know what does turnstile mean, what is Gamma, and what does the big horizontal line mean. That's literally it.


Universal algebra provides a categorical interpretation of algebraic data types with equations, but I would argue that they're going too far. In Java (and similarly weak type systems like Haskell) we're only talking about pattern matching, you don't have any equations. I'm also confused about ring theory, because it seems unrelated to type theory. 


Category theory in this context usually provides a framework of working with semantics and I'd argue that it's not required to learn basic type theory. The category theory used to study type theory is also very advanced, so the intro level things won't help. The same applies to HoTT, it's just too far from programming and type theory itself. Unless you're interested in (infinite, 1)-topoi and their internal languages, I would argue that these shouldn't be required.



Regards,
Tesla

---Original---
From: "Holo The Sage Wolf"<holo3146 at gmail.com>
Date: Wed, Mar 29, 2023 02:10 AM
To: "Tesla Zhang"<ice1000kotlin at foxmail.com>;
Cc: "amber-dev"<amber-dev at openjdk.org>;
Subject: Re: 2 questions about enums and the closed/withdrawn JEP 301


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/5f3f8d7f/attachment-0001.htm>