2 questions about enums and the closed/withdrawn JEP 301

Wed Mar 29 21:13:59 UTC 2023

I'll admit I have a high bias towards research mathematics, so maybe
unintentionally I gave an advice more fitting to people who want to work in
theoretical mathematics.

Large portion of my message came from conversations I had with Kevin
Buzzard, so it is indeed far from applications in actual programming
languages (±PoC languages, logic languages, and the rest of the PV gang).

One thing I'll stand by is the study of formal logic, apart from the fact I
believe it is generally helpful to learn it does appear in everyday
situations, especially for someone who is interested in the inner workings
of a type theory.

For example, to understand how to derive identities purely from the method
signature (see [1]).

I'm not saying that you should learn how Type theory embeds with logic, but
understanding FOL is definitely someone one should at least study when they
enter type theory.

[1] "Theorems For Free!" By F. Wadler
https://dl.acm.org/doi/pdf/10.1145/99370.99404
(The link is directly to the pdf, so if you prefer not to download from a
mail, quick search for "Theorems For Free!" Will find it)

On Wed, Mar 29, 2023, 23:50 Tesla Zhang <ice1000kotlin at foxmail.com> wrote:

> 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/20230330/6ed95311/attachment-0001.htm>