Resource-aware type systems statically approximate not only the expected result type of a program, but also the way external resources are used, e.g., how many times the value of a variable is needed. We extend the type system of Featherweight Java to be resource-aware, parametrically on an arbitrary grade algebra modeling a specific usage of resources. We prove that this type system is sound with respect to a resource-aware version of reduction, that is, a well-typed program has a reduction sequence which does not get stuck due to resource consumption. Moreover, we show that the available grades can be heterogeneous, that is, obtained by combining grades of different kinds, via a minimal collection of homomorphisms from one kind to another. Finally, we show how grade algebras and homomorphisms can be specified as Java classes, so that grade annotations in types can be written in the language itself.

翻译：资源感知类型系统不仅静态近似程序期望的结果类型，还近似外部资源的使用方式，例如，变量值被需要的次数。我们将羽量级Java的类型系统扩展为资源感知，参数化地基于一个任意级代数来建模资源的特定使用方式。我们证明了该类型系统相对于资源感知版本的计算归约是可靠的，即良类型程序具有一个不会因资源消耗而陷入停滞的归约序列。此外，我们展示了可用级可以是异质的，即通过在不同种类的级之间施加最小同态集合，将不同种类的级组合而成。最后，我们展示了级代数和同态可以指定为Java类，从而类型中的级注解可以用语言本身来编写。