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! ###
_______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
