Link Details

While the approach to determine the depth of a type plays nicely with the Church encodings of natural numbers proposed in the paper Towards Equal Rights for Higher-kinded Types, defining arbitrary arithmetic operators seems problematic. Addition does not pose a problem. But there seems to be no easy generalization to other arithmetic operators. This is despite the fact that the authors of the above paper mention that Scala’s kinds correspond to the types of the simply typed lambda calculus.