Typing Recursive Data Structures of Futures for Graph Types
The runtime execution of a terminating program can be represented as a DAG. Static analysis on this DAG would yield many benefits, but the DAG of many programs vary depending on the input. Muller introduced graph types, which are statically-derived representations of all DAGs that could be produced by a program. While these graph types have less specificity than DAGs, they still provide desirable information. However, the language presented by Muller has a notable limitation: the inability to support recursive data structures containing futures. The cause of this limitation is the requirement for each unique future to be typed with a unique reference, called a vertex. This limitation prevents an extensive amount of programs from utilizing the benefits of graph types.
To address this limitation, this paper introduces vertex structures, which are data structures of vertices. With some additional type constructors and graph types, vertex structures provide methods for types and graph types to iterate over vertices. We demonstrate how vertex structures allow recursive data structures containing futures to be assigned a type and a graph type, meaning that a new set of programs are able to utilize graph types.