Class-type
Fixtype of Java (unannotated) class (and interface) types
[JLS14:4.3] [JLS14:8.3].
This is a tagged union type, introduced by fty::deftagsum.
Member Tags → Types
- :simple → class-type-simple
- :package → class-type-package
- :nested → class-type-nested
According to the grammar,
unann-interface-type is a synonym of unann-class-type,
and interface-type is a synonym of class-type.
These synonyms have been presumably introduced
to emphasize the difference between classes and interfaces.
However, in our formalization, it seems more convenient
to just define one syntactic entity for both, called `class type'.
This is not unlike other uses, in [JLS14] and [JVMS14],
of `class' in an attributive role to means `class or interface':
examples are `class loader' and `class file'.
We may revisit this choice in the future,
if we found it actually more convenient to make a distinction
between classes and interfaces at the syntactic level.
There are three kinds of class types.
The first one consists of
a type identifier and some optional type arguments:
this corresponds to simple names [JLS14:6].
The second one consists of
a package name, a type identifier, and some optional type arguments:
this corresponds to a name qualified by a package name [JLS14:6].
The third one consists of
a class type, a type identifier, and some optional type arguments:
this denotes a nested class [JLS14:8].
Since the three summands of this fixtype have two fields in common,
an alternative formalization approach is
to define a class type as a product of those two fields
plus a qualified that is nothing (for simple names)
or a package name or a class type;
that is, to factor the common fields.
We may do that in the future, if it turns out to be more convenient.
Subtopics
- Class-type-case
- Case macro for the different kinds of class-type structures.
- Class-type-equiv
- Basic equivalence relation for class-type structures.
- Class-type-package
- Class-type-nested
- Class-type-simple
- Class-typep
- Recognizer for class-type structures.
- Class-type-kind
- Get the kind (tag) of a class-type structure.
- Class-type-fix
- Fixing function for class-type structures.
- Class-type-count
- Measure for recurring over class-type structures.
