Gradually Structured Data
summary
A formal core language for “gradually structured data” introduces open and closed algebraic datatypes, two new runtime types—unknown datatype and unknown open datatype—and parameterized matching strategies (sound, complete, exact). The paper proves type safety, the two gradual guarantees, and conservative extension to the static language, and ships a prototype interpreter that reduces programs step‑by‑step and runs the examples. The design supports mixing tagged unclassified data with ADTs, documents where runtime checks and static errors occur, and notes performance work needed on cast reduction and representation.
AI-written summary · about
chapters (9)
- 0:00Intro
- 0:15Type imprecision
- 0:50Gradual typing
- 1:15Static guarantees vs. Flexibility in data structuring
- 4:42GSD in action
- 7:48Deriving GSD
- 9:00Gradual types
- 10:58Properties
- 11:24What's next?
related talks
27mA Programing Language for Data and Configuration!
21mDataEngBytes 2023 - SYD-T3-04 - Abhinav Goyal
56mEfficient array (and data) processing by leveraging structure
39mEventually Consistent Data Structures
46mMay Your Data Ever Be Coherent
14mMaking Data Quality an integral part of developing Machine Learning and Data Products
26mFrom Data 2.0 to Data 3.0: Making Data Autonomous for AI(Keynote)
32mDesigning Data Infrastructure in the Age of Generative AI