Counting types for massive JSON datasets

International audienceType systems express structural information about data, are human readable and hence crucial for understanding code, and are endowed with a formal deenition that makes them a fundamental tool when proving program properties. Internal data structures of a database store quantitative information about data, information that is essential for optimization purposes, but is not used for documentation or for correctness proofs. In this paper we propose a new idea: raising a part of the quantitative information from the system-level structures to the type level. Our proposal is motivated by the problem of schema inference for massive collections of JSON data, which are nowadays ooen collected from external sources and stored in NoSQL systems without an a-priori schema, which makes a-posteriori schema inference extremely useful. NoSQL systems are oriented towards the management of heterogeneous data, and in this context we claim that quantitative information is important in order to assess the relative weight of diierent variants. We propose a type system where the same collection can be described at diierent levels of abstraction. Diierent abstraction levels are useful for diierent purposes, hence we describe a parametric inference mechanism, where a single parameter speciies the chosen trade-oo between succinctness and precision for the inferred type. is algorithm is designed for massive JSON collection, and hence admits a simple and eecient map-reduce implementation