Ur/Web, a Domain-Specific Functional
Programming Language for Modern Web
Applications
Adam Chlipala
Web Applications: A Steaming Pile
of Text
HTML, CSS, JavaScript,
SQL, URLs, JSON, ...
Web App Developer
Strings, strings,
strings, ...
Compiler/Interpreter
Saner Languages/Frameworks
●
Links
●
Ocsigen
●
LINQ
●
WebSharper
●
OPA (“One-Pot Application”)
●
...?
3
Executive Summary
Ur/Web is a domain-specific language
with a fancy static type system
with first-class support for Web app architecture
including strong encapsulation
and statically-checked metaprogramming
with security by construction
Hello World!
fun main () = return Hello world!
Hello world!
5
Strong Encapsulation
Insert
Lookup
Hash Table
Module Interface
Client Code
6
Web 1.0 Encapsulation
Users Database Table
Login Cookie
Module Interface
Client Code
7
Encapsulation
structure Auth
: sig
val loginForm : unit > xbody
val whoami : unit > string
end = struct
table users : {Nam : string, Pw : string}
cookie auth : {Nam : string, Pw : string}
fun rightInfo r =
oneRow (SELECT COUNT(*) FROM users
WHERE Nam = {[r.Nam]}
AND Pw = {[r.Pw]}) = 1
fun login r = if rightInfo r then setCookie auth r
else error “Wrong info!”
fun loginForm () = (* Form handled by 'login'... *)
fun whoami () = let r = getCookie auth in
if rightInfo r then r.Nam
else error “Wrong info!”
end
8
Some Client Code
fun main () = return
{Auth.loginForm ()}
and somewhere () =
user < Auth.whoami ();
if user = “Fred Flintstone” then
return Yabba dabba doo!
else
return Boring
and evil () = oneRow (SELECT Pw
FROM Auth.user
WHERE Nam = 'Admin')
9
Web 2.0 Encapsulation
Subtree of
Dynamic Page
Structure
Module Interface
Client Code
10
Functional-Reactive GUIs
The Status Quo:
A
B
The Reactive Way:
Document Tree
(DOM)
Change the value
of this data source.
Script
C
Data Source
Find the node
named “B” and
replace its contents.
D
....
Data Source
Module
Pure Function
A
B
Script
D
C
D
11
A Client-Side Counter
structure Counter : sig
type t
val new : unit > t
val increment : t > unit
val render : t > xbody
end = struct
type t = source int
fun new () = source 0
fun increment c = n < get c; set c (n + 1)
fun render c = {[n]}}/>
end
12
Counter Client
fun main () =
c < Counter.new ();
return
{Counter.render c}
Backup copy: {Counter.render c}
13
Client-Server Communication
(AJAX and Comet)
Message-passing,
a la pi calculus
Web Server
14
Metaprogramming for the Web
Application Piece A
Parameter A
Application Piece B
Parameter B
Parameterized code generator
Already very popular in Ruby on Rails and other frameworks!
15
Automatic Admin Interface
Id
A
B
C
D
Metaprogram
SQL Table Schema
16
In-Browser Spreadsheet
17
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
....
18
Metaprogramming in a Nutshell
Compile-time Programming Language
(AKA, type system)
(not Turing complete, but includes basic lambda calculus)
Crucial feature: type-level records!
Included in
Run-time Programming Language
(Turing complete)
Key Property 1:
These types are expressive
enough to guarantee absence of
code injection, abstraction
violation, etc..
Metadata
controlling
code
generation
options
Metaprogram
Sub-Web
Key Property 2:
Effective static checking that the
metaprogram really has the
claimed type
Metadata's Type-level program
type
Sub-Web's
type
19
Core Language Features
::= Type |
::= | | ∀ :: . | | :: .
e ::= x | e e | x : . e | e [] | :: . e
20
Core Language Features
::= Type |
| Name | {}
::= | | ∀ :: . | | :: .
e ::= x | e e | x : . e | e [] | :: . e
For type-level
record field names
For type-level
records
21
Core Language Features
::= Type |
| Name | {}
::= | | ∀ :: . | | :: .
| #n | [] | [ = ] | ++ | $ | map | [ ~ ]
e ::= x | e e | x : . e | e [] | :: . e
Record concatenation
Singleton record
Empty record
Literal field name
22
Core Language Features
::= Type |
| Name | {}
::= | | ∀ :: . | | :: .
| #n | [] | [ = ] | ++ | $ | map | [ ~ ]
e ::= x | e e | x : . e | e [] | :: . e
Guarded type: require that
two type-level records
share no field names
Convert
“type-level record”
to
“record type”
Apply a function to
every field of a record
23
Core Language Features
::= Type |
| Name | {}
::= | | ∀ :: . | | :: .
| #n | [] | [ = ] | ++ | $ | map | [ ~ ]
e ::= x | e e | x : . e | e [] | :: . e
| {} | { = e} | e. | e – | e ++ e | [ ~ ] e | e !
Record
concatenation
Empty record
Singleton record
Field removal
Field projection
24
Core Language Features
::= Type |
| Name | {}
::= | | ∀ :: . | | :: .
| #n | [] | [ = ] | ++ | $ | map | [ ~ ]
e ::= x | e e | x : . e | e [] | :: . e
| {} | { = e} | e. | e – | e ++ e | [ ~ ] e | e !
Guard elimination
Guarded expression abstraction:
require that two type-level
records share no field names
25
The Type-Checker is Clever
Algebraic laws are applied automatically:
●
1 ++ 2 = 2 ++ 1
●
1 ++ (2 ++ 3) = (1 ++ 2) ++ 3
●
map (. ) =
●
map f (1 ++ 2) = map f 1 ++ map f 2
●
map f (map g ) = map (f g)
○
26
Demo
27
Ur/Web Available At:
http://www.impredicative.com/ur/
Including online demos with syntax-highlighted source code
28