1. 4
  1.  

  2. 1

    These concepts don’t really come from category theory, but definitely definitely applaud sharing this information!

    Also, Box can be a type (or at least a value in the type language) if your language supports higher kinded types.

    1. 1

      I didn’t spot it in the article, but it can be useful to distinguish between “types” and “tags”, where the former are a compile-time checking/inferring/elaboration thing, and the latter are a runtime checking/dispatching thing.

      In the Java/Kotlin scenario, I think a class would be both: we can check annotations at compile time, and we can dispatch method calls at runtime. The JVM’s “primitive types” like int are types but not tags: there are no sub-sets of int which can affect compilation or control flow, e.g. we can’t have odd and even ints dispatch to different method implementations; unless we do a manual check if (isEven(x)) { ... } else { ... }, but that gives us a standalone bool value, rather than something inherent to the int itself.