Existential Type Packing for Structurally-Restricted Existential Types

摘要

A compiler may perform type checking as part of analyzing source code. The type checking may include existential type packing for structurally-restricted existential types. At compile time, the compiler may need to use an existential type that does not conform to the language's structural rules. The compiler may apply the “pack” operation described herein to produce a supertype of the desired existential type that does conform to the language's structural rules, and thus can be used as an approximation of the desired type. The compiler may then perform additional type checking using the resulting type.

主权项

1. A system, comprising:
one or more processors; and a memory comprising program instructions, wherein the program instructions are executed by the one or more processors to perform:
converting, by a compiler during type checking of source code, an input type that mentions one or more free type variables into a packed existential type that does not mention the one or more free type variables;wherein said converting comprises determining one or more bounds for an existential type variable of the packed existential type, wherein the one or more bounds comprises one or more of:
an upper bound for the existential type variable; ora lower bound for the existential type variable; andtype checking the source code based at least in part on the packed existential type and the one or more determined bounds.