[Ur] Need help with desugaring dml

[Sergey Mironov]

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