[Ur] Need help with desugaring dml

[Adam Chlipala]

It should be fixable by adding [val injs = _] at the right place in the 
functor argument.  I'm not entirely sure why it isn't populated by 
default, but did you try also removing the [con] line?

On 02/12/2017 02:40 PM, Sergey Mironov wrote:
> I collected the sources in the functor-inj-err branch of the repo.
> Here are the links:
>
> https://github.com/grwlf/urweb-callback/blob/functor-inj-err/Callback.ur
> https://github.com/grwlf/urweb-callback/blob/functor-inj-err/demo/Callback1.ur
>
> In this setting, the error is as follows:
>
> /nix/store/n3nc28ms0wvggslcx2c29hjn4amxmslm-urweb-urp-CallbackDemo/Callback1.ur:6:14:
> (to 15:1) Unmatched signature item
> Item:  val injs : (fn t :: {Type} => $t) (map sql_injectable u)
>
>
> Regards,
> Sergey
>
>
> 2017-02-12 16:44 GMT+03:00 Adam Chlipala <adamc at csail.mit.edu>:
>> 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
>>
>> _______________________________________________
>> Ur mailing list
>> Ur at impredicative.com
>> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
> _______________________________________________
> Ur mailing list
> Ur at impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur