Teaching old type systems
new tricks with type providers

Tomas Petricek
University of Kent and The Alan Turing Institutehttp://tomasp.net | tomas@tomasp.net | @tomaspetricek

DATA SCIENCEDEMO
Open, reproducible data visualizations

Tooling for data science
The gap between spreadsheets and programming

Tooling for data science
Making programming languages a bit easierTooling for data science
Learning from spreadsheet interaction modelReading data
Unsafe dynamic access in a typed language
var url = "http://dvd.netflix.com/Top100RSS";var rss = XDocument.Load(topRssFeed);var channel = rss.Element("rss").Element("channel");foreach(var item in channel.Elements("item")) {Console.WriteLine(item.Element("text").Value);}Not found!

Reading data
Unsafe dynamic access in a typed language
var url = "http://dvd.netflix.com/Top100RSS";var rss = XDocument.Load(topRssFeed);var channel = rss.Element("rss").Element("channel");foreach(var item in channel.Elements("item")) {Console.WriteLine(item.Element("title").Value);}Reading data
Accessing data from external data sources Languages do not understand data There is rarely explicit schema Manually de ne types to caputre it Easier in dynamic languages

Aggregating data
Athletes by number of gold medals from Rio 2016
Unknown file

olympics = pd.read_csv("olympics.csv")
olympics[olympics["Games"] == "Rio (2016)"].groupby("Athlete").agg({"Gold": sum}).sort_values(by="Gold", ascending=False).head(8)Column nameAggregating data
Language and data source features you need to know
 Python dictionaries {"key": value} Generalised indexers .[ condition ] Operation names sort_values
 Data column names "Athlete"

TYPE PROVIDERS∅ ⊢ e : τπ() ⊢ e : τDEMO
Reading data from an RSS feedF# Data library
Type providers for structured data Structural shape inference Language integration via type providers
 Relative type safety{title : string, author : {age : int}}{author : {age : ﬂoat}}{ title : option<string>, author : {age : ﬂoat} }{ coordinates : {lng:num, lat:num} }string{ coordinates : {lng:num, lat:num} } + stringShape inference
Pragmatic design choices for usability
 Prefers records for tooling Predictable and stable Open world assumption about sums

DEMO
Aggregating Olympic medalists

Dot-driven development
Encoding complex logic via simple member access Type providers for member generation
 Laziness for scaling to large hierarchies Fancy types for the masses!

Row types and phantom types
Row types to track names and types of eldsΓ ⊢ e : [f1 : τ1 , … , fn : τn ]
Γ ⊢ e. drop fi : [f1 : τ1 , … , fi−1 : τi−1 , fi+1 : τi+1 , … , fn : τn ]Embed row types in provided nominal types
Γ ⊢ e : C1whereΓ ⊢ e. drop fi : C2

f ields(C1 ) = {f1 : τ1 , … , fn : τn }f ields(C2 ) = {f1 : τ1 , … , fi−1 : τi−1 , fi+1 : τi+1 , … , fn : τn }

Fancy types for the masses!
Powerful idea that works in other contexts
 Row types and phantom types
 Session types for communication
 Add your own fancy type here!

BEHIND THE SCENES

Relative type safety
Well typed programs do not go wrong.
(As long as the world is well-behaved.)

F# Data and safety
Given representative samples and an input value
S(d) ⊏ S(d1 , … , dn )Any program written using a type provider reduces∗euser [x ← new C (d)] ⇝v

DEMOHandling schema change and errors

F# Data and schema change
Provided type can change only in limited ways

C [e] → C [e. M ]C [e] → C [match e with …]
C [e] → C [int(e)]Structure of a type provider
Context L maps names to de nitions and nested contexts¯¯¯¯¯L(C ) = type C (x : τ ) = m , L′

Pivot provider takes schema and provides a class with context
pivot(F ) = C , L

DEMO
Fancy types in action

Pivot type provider
Generate classes that drop individual columns

JSON type provider
Generate class corresponding to a record shape

SUMMARYFuture work
Making programming with data easier Learning from spreadsheets Understanding programmer interactions
 Handling joins and data cleaning Read, analyse and visualize!

DEMO
Learning from spreadhseetsThank you!

Teaching old type systems new tricks with type providers
Dot-driven
Towards minimal calculus of interactions
Fancy types
Encoding row types via type providers
Relative safety Necessity when working with data

Tomas Petricek
 tomas@tomasp.net | @tomaspetricek | tomasp.net/academic
 thegamma.net | fslab.org | gamma.turing.ac.uk

References
Don Syme, Keith Battocchi, Kenji Takeda, Donna Malayeri and TomasPetricek. Themes in Information-Rich Functional Programming forInternet-Scale Data Sources. In proceedings of DDFP 2013
Tomas Petricek, Gustavo Guerra and Don Syme. Types from data:
Making structured data rst-class citizens in F#. PLDI 2016
Tomas Petricek. Data exploration through dot-driven development.
In proceedings of ECOOP 2017