A Sane Approach to Modern
Web Application Development
Adam Chlipala
February 22, 2010
1
Web 1.0
“Application”
Hello world!
2
Forms
Name:
Page
Submit to
URL “Bar”
Trigger for
URL “Bar”
Handler
blah
This field is called “name.”
Submit
Hello, Foo !
print (“Hello, “ + ENV[“name”] + “!”)
3
Database Access
Page
Name:
'; DELETE FROM balance
Foo
WHERE name <> '
Submit
SQL DB
Handler
Hello, Foo!
Your balance is $1.23.
query (“SELECT balance FROM customers
WHERE name = '” + ENV[“name”] + “'”)
4
Saner Languages/Frameworks
●
Links
●
Ocsigen
●
LINQ
●
WebSharper
●
OPA (“One-Pot Application”)
●
...?
5
Web 1.0 Components
Users Table
IsDisplay
Y the password
of user
X?
a login form
here.
Authentication
Which user is this?
What is user X's password?
Login Cookie
?
Main App
Tell me the cookie contents, so that
I can accidentally include them in a
web page!
6
Web 2.0 Components
Subtree of
Dynamic
Page
Structure
Write
a contents
new line to
Save
the
to the
the area.
server.
Writable Area
Server-Side RPC
Handler
Which
linesthe
arecontents.
there now?
Restore
?
Main App
Let me mess with your part of the
Let me call the RPC manually, so I
page manually, so I can break all
can save contents that I couldn't
your invariants and output some
add the honest way!
garbage!
7
Comet Components
How Many
Zombies Can
You
Barbecue?
Display the chat GUI in a part of the
page of my choosing.
Subtree of
Dynamic
Page
Structure
Chat Client
Persistent Channel
for Server Comm.
Replace chat log with
“BRAAAAAINS”!!!
?
Main App
Pretend to be the user and send a
message to the channel in his
name!
Facebook
8
Back to Basics....
Subtree of
Dynamic
Page
Structure
Users Table
Authentication
Writable Area
Server-Side RPC
Handler
Login Cookie
How do I dispatch
from URLs to all of
my different
components?
Combined Application
9
Code Generation
DB Schema
Standard
DB Admin
Interface
“Scaffolding”
Output program code as strings?
Gross!
Use run-time reflection?
Breaks all the abstractions
we just saw....
What is this and how do I use it?
The manual? Yeah, it's sometimes even accurate!
The source code? :-O
Examples? This is what happens today....
10
My Solutions
●
Strongly-encapsulated web components?
– First-class
language support for the key pieces of
web applications
– No
loopholes!
– Now
use the standard abstractions of functional
programming.
●
Principled metaprogramming?
–
Statically-typed metaprograms, using language
ideas from the world of dependent types.
11
Ur/Web
Ur/Web, a special standard library and compiler
Supporting modern web app development
Web 1.0: Links, forms, etc.
Web 2.0: AJAX and Comet
SQL database access
Ur, a new general purpose language
Inspired by ML and Haskell,
but with even richer type system features
12
Advantages
Productivity
Security
Performance
Important pieces
of web
applications are
first-class.
Any code to be
interpreted is
not “just a
string.”
New ways of
structuring
programs.
Rules out:
Optimizing
compiler
produces fast &
memory-efficient
native code.
New approach
to metaprogramming.
Cross-site scripting
Code injection
Malicious file exec.
Cross-site req. forgery
...
No garbage
collection!
Domain-specific
optimizations
13
Hello World!
fun main () = return Hello world!
Hello world!
14
Hello ___!
functor Hello(M : sig
val text : string
end)
: sig
val main : unit → page
end = struct
fun main () = return Hello {[M.text]}!
Hello {[M.text]}!
end
15
Two Hellos, Living in Harmony
structure World =
Hello(struct val text = “world” end)
structure Boston =
Hello(struct val text = “Boston” end)
fun main () = return
16
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
17
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')
18
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
C
Script
D
D
19
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
20
Counter Client
fun main () =
c ← Counter.new ();
return
{Counter.render c}
Backup copy: {Counter.render c}
21
AJAX
The Status Quo:
The Modular Way:
Or “open a hole”
in the module
interface
Web Server
Script
Call like a
normal function
URI #2
URI #1
RPC
Handler
Web Page
Script
Script
Script
URI #1!
(muahaha!)
22
A Server-Side List
structure ServList : sig
type view
val new : unit → view
val render : view → xbody
val add : string → unit
end = struct
table items : { It : string }
fun allItems () = query (SELECT * FROM items)
type view = source (list string)
fun new () = its ← rpc (allItems ()); source its
fun render v = return
fun doAdd s = dml (INSERT INTO items VALUES ({[s]}))
fun add s = rpc (doAdd s)
end
23
Comet
The Status Quo:
Hm... I think
Client #2 would
like to know
about this.
The Modular Way:
Script
Web Server
RPC
Persistent channel
(a typed,
unforgeable
capability)
Asynchronous
Message
Firewall
(no incoming
connections)
Answer my request with the
first message that is meant for
me.Fantasy
I don't World
mind waiting, and
I'll reconnect afterward for more
Script
messages.
I want messages!
Make sure you
forward mine to
me!
Client #1
And make sure he
can't spy on my
messages!!!
Script
Script
Ditto!!
24
Client #2
A More Proactive List
table listeners : { Chan : channel unit }
fun newListener () =
ch ← channel;
dml (INSERT INTO listeners VALUES ({[ch]}));
return ch
fun new () =
ch ← rpc (newListener ());
its ← rpc (allItems ());
v ← source its;
let fun loop () =
dummy ← recv ch;
its ← rpc (allItems ());
set v its;
loop ()
in spawn (loop ());
return v
end
fun doAdd s = dml (INSERT INTO items VALUES ({[s]}));
foreach (SELECT * FROM listeners)
(fn ch => send ch ())
25
Metaprogramming: An Executive
Summary
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
26
Demo
27
For more information...
http://www.impredicative.com/ur/
28