Ur: Statically-Typed Metaprogramming with
Type-Level Record Computation
Adam Chlipala
PLDI 2010

Strength of Guarantee

Types

Verification
Dependent
Types

Web Applications

Type-Level
Ur/Web
,

Computation
a domain-specific
language for
metaprogramming
Operating Systems
Web applicationsCompilers
Runtime systems
....

Programmer Effort
2

Object-Relational Mapping

SQL Table Schema
Metaprogram

Object-Oriented Interface
● Add row
● Modify row
● Search
● ...

3

Automatic Admin Interface
Id

A

B

C

D
Metaprogram

SQL Table Schema

4

In-Browser Spreadsheet

5

Ad-Hoc Code Generation?
Edit some source files to customize....
Now change the database schema....

app
models
post.rb
views

Id

A

B

C

D

posts
Metaprogram

index.html.erb
show.html.erb

SQL Table Schema

....
config

script/generate scaffold T
Id:int A:string B:float
C:string D:int

routes.rb
....
6

Run-Time Reflection?
Native Object
(in your programming
language)

Id

A

B

C

Library uses
reflection to behave
differently based on
object metadata

D

SQL Table Schema

How do we know that this library is
correct?
How can we be sure that the library
never produces code vulnerable to
code injection attacks or other
failures of abstraction?

7

A Solution Inspired by Dependent
Typing
Metaprogram
Native types and values (Static type guarantees
correct operation!)

Specialized
program

Uses type-level computation
Code-level iteration over types
Id

A

B

C

D

SQL Table Schema

Guaranteed free of
injection vulnerabilities,
for any metaprogram
input
8

An Example Application
Id

A

B

C

D
Metaprogram

SQL Table Schema
table t1 : {Id : int, A : int, B : string,
C : float, D : bool}
PRIMARY KEY Id
open Crud.Make(struct
val tab = t1
val title = "Crud1"
val cols = {A
B
C
D
end)

=
=
=
=

Crud.int "A",
Crud.string "B",
Crud.float "C",
Crud.bool "D"}

Iterate over the
structure of this
record.
9

What's in the Type System?
●

Type-level functions: (t. t → t)

●

Type-level records: [A = (t. t → t), B = (t. t)]

●

Type-level record concatenation: A ++ B

●

Type-level map: map (t. t → t) [A = int, B = float]

●

Disjointness constraints: [A = int, B = float] ~ r

●

Automatic application of algebraic laws
–

E.g., map f (map g r) = map (f ○ g) r

10

Higher-Order Polymorphism
HtmlPage adminInterface<T>(Metadata<T> m) {
/* iterate over m */
}
fun 'T adminInterface (m : 'T Metadata) : HtmlPage =
(* iterate over m? *)
fun ['T :: Type] adminInterface (m : 'T Metadata)
: HtmlPage =
(* iterate over m? *)
fun ['T :: {Type}] adminInterface
(m : $(map Metadata 'T))
(it : 'T Iterator) : HtmlPage =
it (* appropriate arguments here... *)
11

Ur/Web Available At:
http://www.impredicative.com/ur/

Including online demos with syntax-highlighted source code

12