[Ur] Changing a single identifier in crud.ur causes a compiler error - leading to some questions about field names and table names
Stefan Scott
stefanscottalexx at gmail.com
Tue Sep 1 13:45:32 EDT 2015
Consider the (only) two occurrences of the identifier `Tab` in file crud.ur
in the Crud demos, in the function `upd (r : int)`, on lines 126 and 138,
underscored using the coomment `(* ^^^ *)` in the excerpt quoted here
below:
http://hg.impredicative.com/urweb/file/010ce27228f1/demo/crud.ur#l126
http://www.impredicative.com/ur/demo/crud.ur.html
fso <- oneOrNoRows (SELECT tab.{{map fst M.cols}} FROM tab WHERE tab.Id =
{[id]});
case fso : (Basis.option {Tab : $(map fst M.cols)}) of
(* ^^^ *)
None => return <xml><body>Not found!</body></xml>
| Some fs => return <xml><body><form>
{@foldR2 [fst] [colMeta] [fn cols => xml form [] (map snd cols)]
(fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] v (col :
colMeta t)
(acc : xml form [] (map snd rest)) =>
<xml>
<li> {cdata col.Nam}: {col.WidgetPopulated [nm] v}</li>
{useMore acc}
</xml>)
<xml/>
M.fl fs.Tab M.cols}
(* ^^^ *)
<submit action={save}/>
</form></body></xml>
What if we change these two occurrences of the (upper-case) identifier,
from `Tab` to `Tabx` - leaving the lower-case identifier `tab` (which also
occurs many times elsewhere in the module) unchanged?
The code no longer compiles! It gives the following error:
crud.ur:126:32: (to 126:70) Error in final record unification
Can't unify record constructors
Have:
[Distinct = bool,
From =
sql_from_items ([])
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols]),
Where =
sql_exp
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols])
([]) ([]) bool,
GroupBy =
sql_subset
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols])
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols]),
Having =
sql_exp
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols])
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols])
([]) bool,
SelectFields =
sql_subset
([Tab = (map (fn t :: (Type * Type) => t.1) M.cols) ++ [Id = int]])
([Tab = map (fn t :: (Type * Type) => t.1) M.cols]),
SelectExps = {}]
Need:
[Distinct = bool,
From =
sql_from_items ([])
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols]),
Where =
sql_exp
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols])
([]) ([]) bool,
GroupBy =
sql_subset
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols])
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols]),
Having =
sql_exp
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols])
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols])
([]) bool,
SelectFields =
sql_subset
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols])
([Tabx = map (fn t :: (Type * Type) => t.1) M.cols]),
SelectExps = {}]
Field: #SelectFields
Value 1:
sql_subset
([Tab = (map (fn t :: (Type * Type) => t.1) M.cols) ++ [Id = int]])
([Tab = map (fn t :: (Type * Type) => t.1) M.cols])
Value 2:
sql_subset
([Tab = ([Id = int]) ++ map (fn t :: (Type * Type) => t.1) M.cols])
([Tabx = map (fn t :: (Type * Type) => t.1) M.cols])
Can't unify record constructors
Have: [Tab = map (fn t :: (Type * Type) => t.1) M.cols]
Need: [Tabx = map (fn t :: (Type * Type) => t.1) M.cols]
$
The above suggests that there is some sort of "relationship":
BETWEEN:
(1) the *lower-case* identifier `tab`:
- whose *type* is *declared* (in the parameter signature of the
declaration of Crud.Make in crud.urs and crud.ur) as follows:
table tab : ([Id = int] ++ map fst cols)
- and whose *value* is *defined* in (eg) crud1.ur, in the argument in the
call to Crud.Make, as follows:
val tab = t1
... where (eg) the table `t1` (defined earlier in crud1.ur) is in lexical
scope:
table t1 : {Id : int, A : int, B : string, C : float, D : bool}
VERSUS:
(2) the *upper-case* identifier `Tab` - which appears to be:
- (a) a *field name* whose presence is being "asserted", or
- (b) (perhaps?) a *pattern* being assigned to in some sort of
record-level or type-level pattern-matching - in the "type declaration" -
or "assertion?" or "pattern-matching"?? - provided for `fso` in the `case`
statement (*after* `fso` was "created", by the way):
case fso : (Basis.option {Tab : $(map fst M.cols)}) of ...
---
I have several questions arising from the above:
(1) What is this relationship between identifier `tab` and identifier `Tab`
here?
One appears to refer to a table, the other appears to be a field.
Is there some sort of pattern-matching or assertion or assignment going on
between them?
(2) This compile error seems to indicate that identifier `tab` and
identifier `Tab` need to be the *same* (except for upper-case versus
lower-case).
Is this true?
If so, why?
(2.1) Is it true that an Ur/Web database application can be associated with
exactly *one* SQL database (mentioned in the .urp file)?
(2.2) If (2.1) is true, then is there some relationship:
BETWEEN:
- the namespace of unique (upper-case) *field names* defined at the "top
level" of an Ur/Web program;
VERSUS
- the namespace of unique (lower-case) identifiers assigned to *table
names* - in statements such as:
table t1 : {Id : int, A : int, B : string, C : float, D : bool}
which generate CREATE TABLE statements in the *.sql script (with names
optionally mangled with a "uw_" prefix) for the associated SQL database
mentioned in the .urp file?
(3) What does the syntax:
{Tab : $(map fst M.cols)}
ie:
{ ... : ... }
mean?
(3.1) Is the syntax `{ ... : ... }` an instance of the following kind-level
production in section 4.2, page 15 of the manual:
Kinds κ ::=
...
{κ} type-level records
...
Question (3.1.1) If so, is this perhaps somehow combined with some *other*
production(s) in the present case, to yield (in the present example):
{Tab : $(map fst M.cols)}
(3.1.2) Could the other production being combined here be:
Kind ::= Type
(also from Section 4.2, page 15)
in this case instantiating ``Type`` as:
Tab : $(map fst M.cols)
?
Question (3.2) Is the above syntax `{ ... : ... }` as used eg in:
{Tab : $(map fst M.cols)}
related to the "table-definition syntax" (seen frequently in the examples -
but never actually explicitly described "as such" in the manual), eg:
table t1 : {Id : int, A : int, B : string, C : float, D : bool}
?
(3.3) Is this syntax `{ ... : ... }` as used eg in:
{Tab : $(map fst M.cols)}
perhaps also somehow related to the following fragment of code in basis.urs
- in particular, the section underscored using the comment `(* ^^^ *)`:
http://hg.impredicative.com/urweb/file/010ce27228f1/lib/ur/basis.urs#l488
val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
-> fieldType ::: Type -> agg ::: {{Type}}
-> exps ::: {Type}
-> tab :: Name -> field :: Name
-> sql_exp
([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
agg exps fieldType
(4) Finally, the manual (towards the bottom of page 19) states:
A declaration
table x : {(c = c,)∗}
is elaborated into
table x : [(c = c,)∗]
However, a *different* syntax is commonly seen in the "table declarations"
frequently used in the demos - ie, in the demos, the "copulas" are `:` not
`=`, eg:
table t1 : {Id : int, A : int, B : string, C : float, D : bool}
(4.1) What does the following syntax in the manual (using `=` not `:`)
refer to:
table x : {(c = c,)∗}
table x : [(c = c,)∗]
(4.2) Are the any examples of its use?
Thanks for any help!
###
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20150901/84c95b25/attachment.html>
More information about the Ur
mailing list