comparison doc/manual.tex @ 554:193fe8836419

Intro
author Adam Chlipala <adamc@hcoop.net>
date Sun, 07 Dec 2008 15:10:59 -0500
parents effd620d90da
children 0b2cf25a5eba
comparison
equal deleted inserted replaced
553:effd620d90da 554:193fe8836419
1 \documentclass{article} 1 \documentclass{article}
2 \usepackage{fullpage,amsmath,amssymb,proof} 2 \usepackage{fullpage,amsmath,amssymb,proof,url}
3 3
4 \newcommand{\cd}[1]{\texttt{#1}} 4 \newcommand{\cd}[1]{\texttt{#1}}
5 \newcommand{\mt}[1]{\mathsf{#1}} 5 \newcommand{\mt}[1]{\mathsf{#1}}
6 6
7 \newcommand{\rc}{+ \hspace{-.075in} + \;} 7 \newcommand{\rc}{+ \hspace{-.075in} + \;}
14 \author{Adam Chlipala} 14 \author{Adam Chlipala}
15 15
16 \maketitle 16 \maketitle
17 17
18 \tableofcontents 18 \tableofcontents
19
20
21 \section{Introduction}
22
23 \emph{Ur} is a programming language designed to introduce richer type system features into functional programming in the tradition of ML and Haskell. Ur is functional, pure, statically-typed, and strict. Ur supports a powerful kind of \emph{metaprogramming} based on \emph{row types}.
24
25 \emph{Ur/Web} is Ur plus a special standard library and associated rules for parsing and optimization. Ur/Web supports construction of dynamic web applications backed by SQL databases. The signature of the standard library is such that well-typed Ur/Web programs ``don't go wrong'' in a very broad sense. Not only do they not crash during particular page generations, but they also may not:
26
27 \begin{itemize}
28 \item Suffer from any kinds of code-injection attacks
29 \item Return invalid HTML
30 \item Contain dead intra-application links
31 \item Have mismatches between HTML forms and the fields expected by their handlers
32 \item Attempt invalid SQL queries
33 \item Use improper marshaling or unmarshaling in communication with SQL databases
34 \end{itemize}
35
36 This type safety is just the foundation of the Ur/Web methodology. It is also possible to use metaprogramming to build significant application pieces by analysis of type structure. For instance, the demo includes an ML-style functor for building an admin interface for an arbitrary SQL table. The type system guarantees that the admin interface sub-application that comes out will always be free of the above-listed bugs, no matter which well-typed table description is given as input.
37
38 The Ur/Web compiler also produces very efficient object code that does not use garbage collection. These compiled programs will often be even more efficient than what most programmers would bother to write in C.
39
40 \medskip
41
42 The official web site for Ur is:
43 \begin{center}
44 \url{http://www.impredicative.com/ur/}
45 \end{center}
19 46
20 \section{Ur Syntax} 47 \section{Ur Syntax}
21 48
22 In this section, we describe the syntax of Ur, deferring to a later section discussion of most of the syntax specific to SQL and XML. The sole exceptions are the declaration forms for tables, sequences, and cookies. 49 In this section, we describe the syntax of Ur, deferring to a later section discussion of most of the syntax specific to SQL and XML. The sole exceptions are the declaration forms for tables, sequences, and cookies.
23 50