Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

Scrap Your Web Application Boilerplate, or Metaprogramming with Row Types

Adam Chlipala

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2006-120
September 29, 2006

http://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-120.pdf

I introduce a new functional programming language, called Laconic/Web, for rapid development of web applications. Its strong static type system guarantees that entire sequences of interaction with these applications ``can't go wrong.'' Moreover, a higher-order dependent type system is used to enable statically-checked metaprogramming. In contrast to most dependently-typed programming languages, Laconic/Web can be used by programmers with no knowledge of proof theory. Instead, more expert developers develop libraries that extend the Laconic/Web type checker with type rewrite rules that have proofs of soundness. I compare Laconic/Web against Ruby on Rails, the most well-known representative of a popular class of web application frameworks based around dynamic languages and runtime reflection, and show that my approach leads both to more concise programs and to better runtime efficiency.


BibTeX citation:

@techreport{Chlipala:EECS-2006-120,
    Author = {Chlipala, Adam},
    Title = {Scrap Your Web Application Boilerplate, or Metaprogramming with Row Types},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2006},
    Month = {Sep},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-120.html},
    Number = {UCB/EECS-2006-120},
    Abstract = {I introduce a new functional programming language, called Laconic/Web, for rapid development of web applications. Its strong static type system guarantees that entire sequences of interaction with these applications ``can't go wrong.'' Moreover, a higher-order dependent type system is used to enable statically-checked metaprogramming. In contrast to most dependently-typed programming languages, Laconic/Web can be used by programmers with no knowledge of proof theory. Instead, more expert developers develop libraries that extend the Laconic/Web type checker with type rewrite rules that have proofs of soundness. I compare Laconic/Web against Ruby on Rails, the most well-known representative of a popular class of web application frameworks based around dynamic languages and runtime reflection, and show that my approach leads both to more concise programs and to better runtime efficiency.}
}

EndNote citation:

%0 Report
%A Chlipala, Adam
%T Scrap Your Web Application Boilerplate, or Metaprogramming with Row Types
%I EECS Department, University of California, Berkeley
%D 2006
%8 September 29
%@ UCB/EECS-2006-120
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-120.html
%F Chlipala:EECS-2006-120