From Impredicative Wiki
Revision as of 09:25, 4 February 2010 by Adam Chlipala (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Graftid is a platform for developing and hosting web applications using Ur/Web, targeted at both programmers and the general public. These two audiences naturally need very different views of the service. The standard view is meant to be self-explanatory; this wiki page documents the picture for developers.

Graftid is in a closed alpha right now. The main web site is password-protected, while hosted applications can be accessed by anyone. If you are interested in testing, please e-mail Adam to ask for access. Note that things are slightly complicated so that testing can exercise the account creation code: the initial password you get will allow you into the site, but once there you will still need to create a Graftid account.


At a high level, Graftid is a repository of application designers, which are like browser-based GUI wizards for building particular kinds of web applications. Developers upload designers, which are written in Ur/Web and also generate Ur/Web code. Ideally these designers do very little ad-hoc code generation, instead serving merely to build calls to metaprogramming libraries, which can be implemented in Ur/Web such that static types guarantee they work properly on any valid inputs. To layperson end users, these details are invisible. They just see web forms that can be used to bring new database-backed web applications into existence.

Graftid can store a tree of libraries, owned by different users and with different versions available at once. This tree is much like a standard filesystem. Its main aspects are:

  • Users, corresponding to accounts created by people
  • Groups, named sets of users
  • Directories, in the usual UNIX-y sense, with every directory but the root directory having another directory as its parent. Different users and groups may be assigned read, write, or admin rights on a directory. Admin rights make it possible to edit the permission matrix. Groups themselves belong to directories, so that directory permissions control who may modify a group's member set. All of the following kinds of things that belong to directories have similar inheritance of directory permissions.
  • Libraries, named groups of Ur/Web modules, situated in directories
  • Library versions, particular sets of source files that may be linked to build concrete applications. Each version is associated with a particular library, but no formal connection is enforced between different versions of one library.
  • Designers, GUIs for building applications from particular libraries, situated in directories
  • Designer versions
  • Applications, specific persistent applications, situated in directories
  • Application versions

Programming GUIs

To get started coding Graftid application designers, you will want to download and install the GUI library. This library defines some types and module signatures that you will need to use or implement. First, since the mission of a designer is to generate Ur/Web code, we have the Ur module, which gives a representation of a subset of Ur/Web syntax.

(* Constructors, i.e., type-level data *)
datatype constr =
             TFun of constr * constr
             (* The usual function arrow *)
           | TRecord of constr
             (* Builds a record type from a constructor of soome kind {K} *)

           | CVar of list string * string
             (* Variable reference, with CVar (m1 :: ... :: mn :: nil, x)
              * meaning m1.[...].mn.x (for module names mi) *)
           | CApp of constr * constr
             (* Constructor-level function application *)

           | CName of string
             (* Field name literal *)

           | CRecord of list (constr * constr)
             (* Explicit record fields, as pairs of names and values *)

           | CUnit
             (* The trivial constructor *)

           | CTuple of list constr
             (* Constructor-level tuple construction *)

(* Value-level constants *)
datatype prim =
         Int of int
       | Float of float
       | String of string
       | Char of char

(* Value-level expressions *)
datatype exp =
         EPrim of prim
         (* Constant *)
       | EVar of list string * string
         (* Variable reference, encoded as for CVar *)
       | EApp of exp * exp
         (* Function application *)
       | EAbs of string * exp
         (* Function abstraction *)
       | ECApp of exp * constr
         (* Applying a polymorphic function *)
       | EDisjointApp of exp
         (* Applying an abstraction over a row disjointness constraint *)
       | ERecord of list (constr * exp)
         (* Record construction *)
       | EField of exp * constr
         (* Record projection *)
       | ELet of string * exp * exp
         (* Local definition *)

(* Declarations *)
datatype decl =
         DCon of string * constr
         (* Constructor synonym *)
       | DVal of string * exp
         (* Value-level binding *)
       | DValRec of list (string * exp)
         (* Mutually-recursive value bindings (each exp must begin with EAbs) *)
       | DStr of string * str
         (* Structure (i.e., module) definition *)
       | DOpen of list string * string
         (* Import a module path *)

(* Modules *)
     and str =
         StrConst of list decl
         (* Structure with known contents *)
       | StrVar of string
         (* Variable reference *)
       | StrProj of str * string
         (* Project out a sub-structure *)
       | StrApp of str * str
         (* Apply a functor *)

type file = list decl
Personal tools