[Ur] Need help with desugaring dml

[Adam Chlipala]

Your example doesn't show the functor being applied.  The problem would 
need to be in the details of that application, since such arguments do 
indeed get inferred under many circumstances.

On 02/12/2017 04:56 AM, Sergey Mironov wrote:
> Thanks, very interesting. I've managed to fix my original code, it is
> attached below.
>
> During the work I discovered a fact that UrWeb automatically infers a
> record of [sql_injectable] instances if it is passed as function
> argument, but refuses to do so if I try to pass it as Functor
> argument. In the latter case, the error is as follows:
>
> Callback1.ur:6:14: (to 12:1) Unmatched signature item
> Item:  val injs : (fn t :: {Type} => $t) (map sql_injectable u)
>
> Is it a generic limitation or just an undone feature?
>
> Regards,
> Sergey
>
> ---
>
> con jobinfo = [
>      Id = int
>    , ExitCode = option int
>    , Cmd = string
>    , Hint = string
>    ]
>
> functor Make(M : sig
>
>    con u
>
>    val fu : folder u
>
>    (* val injs : record (map sql_injectable u) *)
>
>    constraint [Id,ExitCode,Cmd,Hint] ~ u
>
>    table t : (jobinfo ++ u)
>
>    sequence s
>
> end) = struct
>
>    type row' = record (jobinfo ++ M.u)
>
>    fun createSync (cmd : string)
>                   (injs : record (map sql_injectable M.u))
>                   (fs : record M.u)
>                   : transaction (option int) =
>
>      i <- nextval M.s;
>
>      dml (insert M.t (
>
>          { Id = sql_inject i,
>            ExitCode = sql_inject None,
>            Cmd = sql_inject cmd,
>            Hint = sql_inject "" } ++
>
>          (@Top.map2 [sql_injectable] [ident] [sql_exp [] [] []]
>            (fn [t] => @sql_inject) M.fu injs fs)
>        )
>      );
>
>      return (Some i)
>
> end
>
> 2017-02-11 16:59 GMT+03:00 Adam Chlipala <adamc at csail.mit.edu>:
>> The key things missing in the original functor argument are a folder for [u]
>> and a record of [sql_injectable] instances for it, both of which you'll see
>> used in similar UPO functions mentioned earlier.
>>
>> BTW, the type of [insert] (in lib/ur/basis.urs) isn't magic and can be
>> inspected just like any Ur type, and it should be possible to understand
>> from first principles.
>>
>>
>> On 02/11/2017 04:19 AM, fold at tuta.io wrote:
>>
>> Actually, it might be quite simple.
>> Incomplete, but, hopefully, clear example:
>>
>> table tab : $([Ix = int] ++ someColumns ++ otherColumns) PRIMARY KEY Ix
>>
>> fun test () : transaction xbody =
>>      <...>
>>      tn <- now;
>>      easy_insert tab ({Ix = ix} ++ field_defaults ++ {Dated = tn});
>>      <...>
>>
>>
>>
>> 11. Feb 2017 22:09 by fold at tuta.io:
>>
>> Sergey,
>>
>> Something similar to this:
>> https://github.com/achlipala/upo/blob/master/sql.ur#L44
>> and this:
>> https://github.com/achlipala/upo/blob/master/sql.ur#L50
>> might help you a bit.
>>
>> Also check other functions in sql.ur
>>
>> I believe you also can figure out desugared type expressions from compiler
>> error output if you replace parts of your code with simple expressions of
>> known type.
>>
>> https://wiki.haskell.org/GHC/Typed_holes
>>
>>
>>
>>
>>
>> 11. Feb 2017 21:18 by grrwlf at gmail.com:
>>
>> Hi. I'm trying (again) to write an Ur/Web module to provide API for
>> managing OS-level processes. I expect users to pass it a table
>> containing _at_least_ id, process command name, arguments, placeholder
>> for exit code and status string. It is expected that users will use
>> tables containing more problem-specific columns.
>>
>> The problem is that I cant use simple dml operations anymore. As a
>> start, I tried to write dummy insert using [demo/more/orm.ur] as
>> example, but was stopped by difficult [ensql] function. Could you
>> please help me to implement it? The code is quite short and listed
>> below.
>>
>> Regards,
>> Sergey
>>
>> ---
>>
>> con jobinfo = [
>> Id = int
>> , ExitCode = option int
>> , Cmd = string
>> , Hint = string
>> ]
>>
>> functor Make(M : sig
>>
>> con u
>>
>> constraint [Id,ExitCode,Cmd,Hint] ~ u
>>
>> table t : (jobinfo ++ u)
>>
>> sequence s
>>
>> end) = struct
>>
>> open CallbackFFI
>>
>> type row' = record (jobinfo ++ M.u)
>>
>> (* fun ensql [avail ::_] (r : row') : $(map (sql_exp avail [] []) fs') = *)
>> (* @map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail
>> [] [] ts.1] *)
>> (* (fn [ts] meta v => @sql_inject meta.Inj v) *)
>> (* M.folder M.cols r *)
>>
>> (* createSync will start the job, but in this example it just does a
>> simple insert.
>> args is a problem-specific part of the table record.
>>
>> How to make this dml(insert..) work? *)
>>
>> fun createSync (ji : record jobinfo, args : record M.u) :
>> transaction (option int) =
>> i <- nextval M.s;
>> dml(insert M.t ({Id = sql_inject ji.Id,
>> ExitCode = sql_inject ji.ExitCode,
>> Cmd = sql_inject ji.Cmd,
>> Hint = sql_inject ji.Hint} ++ (ensql args) ));
>>
>> return (Some i)
>>
>> end