Infectious Typing

Type theory has many kinds of typing mechanisms: product, sum, top, bottom, recursive, universal, existential, subtypes, linear, refinement, dependent, and so on. I have run across something different from all those, which I am calling “infectious typing”. If anyone knows a formal name and/or treatment for this mechanism, I would love to hear about it. Type composition allows us to create new types out of existing ones. A struct or class product types is composed of several fields, each with its own type.

Unified Variant Type

The prior post, When Sum Types Inherit, shows that we can (and should) use the magic of inheritance to enrich sum types to offer as powerful a capability as traditional classes. Graph-based, variant node data structures benefit from variant nodes being able to support common fields, methods, and virtual dispatch. That result, however, raises a new question: do we really need two separate language abstractions that offer very similar capabilities?