changeset 413:6a0e54400805

Sum prose
author Adam Chlipala <adamc@hcoop.net>
date Tue, 21 Oct 2008 19:56:20 -0400
parents df4cbd90a26e
children cca935276869
files demo/link.ur demo/prose demo/sum.ur src/elab_err.sig src/elab_err.sml src/elaborate.sml
diffstat 6 files changed, 35 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/demo/link.ur	Tue Oct 21 19:31:11 2008 -0400
+++ b/demo/link.ur	Tue Oct 21 19:56:20 2008 -0400
@@ -3,5 +3,5 @@
 </body></xml>
 
 fun main () = return <xml><body>
-  <a link={target}>Go there</a>
+  <a link={target ()}>Go there</a>
 </body></xml>
--- a/demo/prose	Tue Oct 21 19:31:11 2008 -0400
+++ b/demo/prose	Tue Oct 21 19:56:20 2008 -0400
@@ -71,3 +71,28 @@
 <p>Other functions demonstrate use of the <tt>dml</tt> function, for building a transaction from a SQL DML command.  It is easy to insert antiquoted Ur code into queries and DML commands, and the type-checker catches mistakes in the types of the expressions that we insert.</p>
 
 <p>
+
+sum.urp
+
+<p>Metaprogramming is one of the most important facilities of Ur.  This example shows how to write a function that is able to sum up the fields of records of integers, no matter which set of fields the particular record has.</p>
+
+<p>Ur's support for analysis of types is based around extensible records, or <i>row types</i>.  In the definition of the <tt>sum</tt> function, we see the type parameter <tt>fs</tt> assigned the <i>kind</i> <tt>{Unit}</tt>, which stands for records of types of kind <tt>Unit</tt>.  The <tt>Unit</tt> kind has only one inhabitant, <tt>()</tt>.  The kind <tt>Type</tt> is for "normal" types.</p>
+
+<p>The unary <tt>$</tt> operator is used to build a record <tt>Type</tt> from a <tt>{Type}</tt> (that is, the kind of records of types).  The library function <tt>mapUT</tt> takes in a <tt>Type</tt> <i>t</i> and a <tt>{Unit}</tt> <i>r</i>, and it builds a <tt>{Type}</tt> as long as <i>r</i>, where every field is assigned value <i>t</i>.</p>
+
+<p>Another library function <tt>foldUR</tt> is defined at the level of expressions, while <tt>mapUT</tt> is a type-level function.  <tt>foldUR</tt> takes 6 arguments, some of them types and some values.  Type arguments are distinguished by being written within brackets.  The arguments to <tt>foldUR</tt> respectively tell us:
+
+<ol>
+<li> The type we will assign to each record field</li>
+<li> The type of the final and all intermediate results of the fold, expressed as a function over the portion of the <tt>{Unit}</tt> that has been traversed so far</li>
+<li> A function that updates the accumulator based on the current record field name, the rest of the input record type, the current record field value, and the current accumulator</li>
+<li> The initial accumulator value</li>
+<li> The input record type</li>
+<li> The input record value</li>
+</ol>
+
+An unusual part of the third argument is the syntax <tt>[t1 ~ t2]</tt> within a multi-argument <tt>fn</tt>.  This syntax denotes a proof that row types <tt>t1</tt> and <tt>t2</tt> have no field names in common.  The proof is not named, because it is applied automatically as needed.  Indeed, the proof appears unused in this case, though it is actually needed to ensure the validity of some inferred types, as well as to unify with the type of <tt>foldUR</tt>.</p>
+
+<p>The general syntax for constant row types is <tt>[Name1 = t1, ..., NameN = tN]</tt>, and there is a shorthand version <tt>[Name1, ..., NameN]</tt> for records of <tt>Unit</tt>s.</p>
+
+<p>With <tt>sum</tt> defined, it is easy to make some sample calls.  The form of the code for <tt>main</tt> does not make it apparent, but the compiler must "reverse engineer" the appropriate <tt>{Unit}</tt> from the <tt>{Type}</tt> available from the context at each call to <tt>sum</tt>.</p>
--- a/demo/sum.ur	Tue Oct 21 19:31:11 2008 -0400
+++ b/demo/sum.ur	Tue Oct 21 19:56:20 2008 -0400
@@ -4,6 +4,7 @@
     0 [fs] x
 
 fun main () = return <xml><body>
+  {[sum {}]}<br/>
   {[sum {A = 0, B = 1}]}<br/>
   {[sum {C = 2, D = 3, E = 4}]}
 </body></xml>
--- a/src/elab_err.sig	Tue Oct 21 19:31:11 2008 -0400
+++ b/src/elab_err.sig	Tue Oct 21 19:56:20 2008 -0400
@@ -49,7 +49,7 @@
            | COccursCheckFailed of Elab.con * Elab.con
            | CIncompatible of Elab.con * Elab.con
            | CExplicitness of Elab.con * Elab.con
-           | CKindof of Elab.kind * Elab.con
+           | CKindof of Elab.kind * Elab.con * string
            | CRecordFailure of Elab.con * Elab.con
 
     val cunifyError : ElabEnv.env -> cunify_error -> unit
--- a/src/elab_err.sml	Tue Oct 21 19:31:11 2008 -0400
+++ b/src/elab_err.sml	Tue Oct 21 19:56:20 2008 -0400
@@ -109,7 +109,7 @@
        | COccursCheckFailed of con * con
        | CIncompatible of con * con
        | CExplicitness of con * con
-       | CKindof of kind * con
+       | CKindof of kind * con * string
        | CRecordFailure of con * con
 
 fun cunifyError env err =
@@ -131,8 +131,8 @@
         eprefaces "Differing constructor function explicitness"
                   [("Con 1", p_con env c1),
                    ("Con 2", p_con env c2)]
-      | CKindof (k, c) =>
-        eprefaces "Unexpected kind for kindof calculation"
+      | CKindof (k, c, expected) =>
+        eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")")
                   [("Kind", p_kind k),
                    ("Con", p_con env c)]
       | CRecordFailure (c1, c2) =>
--- a/src/elaborate.sml	Tue Oct 21 19:31:11 2008 -0400
+++ b/src/elaborate.sml	Tue Oct 21 19:56:20 2008 -0400
@@ -481,7 +481,7 @@
          (case hnormKind (kindof env c) of
               (L'.KArrow (_, k), _) => k
             | (L'.KError, _) => kerror
-            | k => raise CUnify' (CKindof (k, c)))
+            | k => raise CUnify' (CKindof (k, c, "arrow")))
        | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
        | L'.CDisjoint (_, _, _, c) => kindof env c
 
@@ -497,7 +497,7 @@
        | L'.CProj (c, n) =>
          (case hnormKind (kindof env c) of
               (L'.KTuple ks, _) => List.nth (ks, n - 1)
-            | k => raise CUnify' (CKindof (k, c)))
+            | k => raise CUnify' (CKindof (k, c, "tuple")))
 
        | L'.CError => kerror
        | L'.CUnif (_, k, _, _) => k
@@ -546,7 +546,7 @@
              case hnormKind (kindof env c) of
                  (L'.KRecord k, _) => k
                | (L'.KError, _) => kerror
-               | k => raise CUnify' (CKindof (k, c))
+               | k => raise CUnify' (CKindof (k, c, "record"))
 
          val k1 = rkindof c1
          val k2 = rkindof c2
@@ -2318,7 +2318,7 @@
                                                      val env = if n1 = n2 then
                                                                    env
                                                                else
-                                                                   E.pushCNamedAs env x n1 (L'.KType, loc)
+                                                                   E.pushCNamedAs env x n1 k'
                                                                                   (SOME (L'.CNamed n2, loc))
                                                  in
                                                      SOME (env, denv)