Types from data: Making structured data first-class citizens in F#
Tomas Petricek, Gustavo Guerra, Don Syme

TL;DR
The paper introduces F# Data, a library that integrates external structured data into F# by inferring data shapes from samples and embedding them into the type system, enhancing safety and reducing code complexity.
Contribution
It develops a shape inference algorithm for external data and formalizes its integration into F#'s type system using type providers, with proven soundness.
Findings
Reduces data access code significantly
Provides safety guarantees over weakly typed methods
Formalizes shape inference with a soundness proof
Abstract
Most modern applications interact with external services and access data in structured formats such as XML, JSON and CSV. Static type systems do not understand such formats, often making data access more cumbersome. Should we give up and leave the messy world of external data to dynamic typing and runtime checks? Of course, not! We present F# Data, a library that integrates external structured data into F#. As most real-world data does not come with an explicit schema, we develop a shape inference algorithm that infers a shape from representative sample documents. We then integrate the inferred shape into the F# type system using type providers. We formalize the process and prove a relative type soundness theorem. Our library significantly reduces the amount of data access code and it provides additional safety guarantees when contrasted with the widely used weakly typed techniques.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Advanced Database Systems and Queries · Web Data Mining and Analysis
