[Ur] Given a value of a "transactional" type, how can it be used in an expression expecting a different, "non-transactional" type?

[Stefan Scott Alexander]

Summary:

I have been attempting to extend the Crud2 demo to include a foreign-key
field and provide a data-bound widget (using a <select> element containing
multiple <option> elements) to allow the user to easily edit the
foreign-key field.

My code is giving compile errors such as "unification failure" and
"incompatible constructors", which can be seen here:

https://github.com/StefanScott/urweb-crud2foreign/issues/1

Apparently these compile errors are happening because:

- My code instantiates functions Show, Widget, WidgetPopulated and Parse,
which are defined in crud.urs / crud.ur (in the Crud2 demo) and which are
expected to return values of type xbody, xml, and db;

- Meanwhile, my code uses Top.queryX1 and Top.oneRowE1 which return values
of "transactional" types - instead of the desired types xbody, xml and db.

So it seems that I need to run the transactional SQL functions queryX1 and
oneRowE1, grab their transactional output, and then from that somehow
obtain values of the appropriate types, such as xbody, xml, db.

I am fairly sure that all that is needed is minor adjustment to the
erroneous syntax currently being used by my code - but I have not been able
to hit on the correct syntax yet. (The 3 alternative syntaxes which I've
tried are illustrated further below.)

Thanks for any help!


Initial, oversimplified case (this works):

As an initial, oversimplified case, I extended the Crud2 demo by merely
adding a *non-foreign-key* field called LocalStatus. This works fine, and
can be seen in this small github repository:

https://github.com/StefanScott/urweb-crud2local

However, this approach is not very useful, as it merely "hard-codes" 3
'Status' values in the program text, and does not involve a "parent" table
providing a foreign key. The next approach will attempt to resolve this, by
creating a separate "parent" table 'Status'.


Next case (this doesn't work):

This case involves extending the Crud2 demo by adding a a new table
'status' and a *foreign-key* field t.ForeignStatus referencing status.Id.

This code is giving compile-time errors about about "record unification" or
"incompatible constructors". The (currently non-working) code can be seen
in a separate github repository here:

https://github.com/StefanScott/urweb-crud2foreign

To avoid cluttering up this mailing list, the compile errors (for the
version of the code used in the above crud2foreign repo) have been
reproduced as Issue 1 in the github repo, here:

https://github.com/StefanScott/urweb-crud2foreign/issues/1


Background:

The above approaches attempt to extend the existing Crud2 demo, which is
available here:

http://www.impredicative.com/ur/demo/crud2.html

Recall that the Crud2 demo involves a record of 6 functions (Nam, Show,
Widget, WidgetPopulated, Parse, Inject), whose declarations are shown below:

{Nam : string,
 Show : db -> xbody,
 Widget : nm :: Name -> xml form [] [nm = widget],
 WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget],
 Parse : widget -> db,
 Inject : sql_injectable db}

Informally, the functions Show, Widget, WidgetPopulated and Parse do the
following:

- The function Show accepts a db and returns an xbody.

- The function Widget accepts a nm of kind Name, and returns an xml. (If
the widget implements a data-bound dropdown, then it might contain a
<select> element, in turn containing multiple <option> elements).

- The function WidgetPopulated accepts a nm of kind Name and a db, and
returns an xml. (If the widget implements a data-bound dropdown, then it
might contain a <select> element, in turn containing multiple <option>
elements).

- The function Parse accepts a widget and returns a db.

To define Show, Widget, WidgetPopulated and Parse, I am using the functions
Top.QueryX1 and Top.oneRowE1, which are documented in the excellent
chatroom tutorial:
http://adam.chlipala.net/papers/UrWebPOPL15/UrWebPOPL15.pdf (eg, see page 2
for example usage, and see page 3 for nice English-language explanations of
that these functions are intended to do).

When compiling crud2foreign, the compiler give various errors about "record
unification" or "incompatible constructors".

So my code is obviously not producing the correct types.


Attempting various alternative syntaxes (none of these work):

I have been attempting various syntax alternatives (playing around with the
semi-colon and the 'return'), but they have all been incorrect.

(1) Below are 3 (non-working!) syntax alternatives I have attempted for the
definition of Show:

Show = (fn fs =>
  statusNam <- oneRowE1 (SELECT Nam FROM status WHERE Id = {[fs]});
  return;
  <xml>{statusNam}</xml>)

Show = (fn fs =>
  statusNam <- oneRowE1 (SELECT Nam FROM status WHERE Id = {[fs]});
  return statusNam;
  <xml>{statusNam}</xml>)

Show = (fn fs =>
  <xml>{oneRowE1 (SELECT Nam FROM status WHERE Id = {[fs]})}</xml>)

(2) Below are the corresponding 3 (non-working!) syntax alternatives I have
attempted for the definition of Widget (and similar code is used for
WidgetPopulated, which simply accepts an additional argument of type db):

Widget = (fn [nm :: Name] =>
statusOptions <-
  queryX1 (SELECT Id, Nam FROM status ORDER BY Nam)
  (fn r => <xml><coption value={r.Id}>{r.Nam}</coption></xml>);
  return;
  <xml>
    <select{nm}>
      {statusOptions}
    </select>
  </xml>)

Widget = (fn [nm :: Name] =>
statusOptions <-
  queryX1 (SELECT Id, Nam FROM status ORDER BY Nam)
  (fn r => <xml><coption value={r.Id}>{r.Nam}</coption></xml>);
  return statusOptions;
  <xml>
    <select{nm}>
      {statusOptions}
    </select>
  </xml>)

Widget = (fn [nm :: Name] =>
  <xml>
    <select{nm}>
      {queryX1 (SELECT Id, Nam FROM status ORDER BY Nam)
       (fn r => <xml><coption value={r.Id}>{r.Nam}</coption></xml>)}
    </select>
  </xml>)

(2) And below are the corresponding 3 (non-working!) syntax alternatives I
have attempted for the definition of Parse:

Parse = (fn fsNam =>
  fsId <- oneRowE1 (SELECT Id FROM status WHERE Nam = {[fsNam]});
  return fsId;
  fsId)

Parse = (fn fsNam =>
  fsId <- oneRowE1 (SELECT Id FROM status WHERE Nam = {[fsNam]});
  return;
  fsId)

Parse = (fn fsNam =>
  oneRowE1 (SELECT Id FROM status WHERE Nam = {[fsNam]}))

In the absence of more detailed documentation and examples of how to use
functions such as queryX1 and oneRowE1 to write transactional code and
extract expressions, the above attempts are just clumsy shots in the dark
by an Ur/Web novice.


Discussion:

Examining top.urs, the declaration of queryX1 is:

val queryX1 : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp :::
{Type}
              -> sql_query [] [] [nm = fs] []
              -> ($fs -> xml ctx inp [])
              -> transaction (xml ctx inp [])

And the declaration of oneRowE1 is:

val oneRowE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type
               -> [tabs ~ [nm]] =>
    sql_query [] [] (mapU [] tabs) [nm = t]
    -> transaction t


Aside:

There is a bit of discussion about the absolutely essential files top.urs /
top.ur in the PDF manual, and online here:

http://enn.github.io/urweb-doc/node31.html

Other than that, the only documentation appears to be the source code of
the Ur/Web compiler itself - plus the very helpful descriptions of queryX1
and oneRowE1 in the chatroom tutorial:
http://adam.chlipala.net/papers/UrWebPOPL15/UrWebPOPL15.pdf


Further discussion:

Meanwhile, examining the code in crud.urs / crud.ur reveals that the
functions Show, Widget, WidgetPopulated, and Parse are not expected to
return "transactional" types - instead, they are expected to return types
involving xbody, xml and db:

Show : db -> xbody,
Widget : nm :: Name -> xml form [] [nm = widget],
WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget],
Parse : widget -> db,

Therefore, I have been trying to run queryX1 and oneRowE1 and then somehow
obtain values of types compatible with what crud.urs / crud.ur expects.

I suspect that the overall context involved in the chatroom example might
be different from the context involved the Crud2 demo - which would mean
that the code from the chatroom example cannot be used directly in my
crud2foreign code, which needs to be compatible with the Crud2 demo.

Thanks for any help!

- Scott
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20150718/fbac8126/attachment.html>