[Ur] Default settings using a generic record update
Ziv Scully
zivscully at gmail.com
Wed Dec 11 11:31:14 EST 2019
That error means you need to explicitly pass a type class instance. In this
case, it means replacing "update_ab" with "@update_ab Subset.intro".
Here "Subset.intro" is a polymorphic type class instance (see subset.urs).
In concrete cases like this, the compiler can usually figure out what
folders to pass to "Subset.intro", but in other cases (especially
polymorphic ones) you might need "@Subset.intro some_folder another_folder".
On Wed, Dec 11, 2019 at 5:57 AM Mark Clements <mark.clements at ki.se> wrote:
> Ziv,
>
> Thank you for this. I had hoped that the following code would work:
>
> con ab = [A=int, B=int]
>
> fun update_ab [write] (sub : Subset.t ab write) (w : $write) =
> Subset.set {A=1,B=2} w
>
> fun main () =
> let
> val a = update_ab {A=2} (* [line 8] {A=2, B=2} *)
> in
> return <xml>
> <body>
> a.A: {[a.A]}<p/>
> </body>
> </xml>
> end
>
> However, I get an error "[line 8] Can't resolve type class instance
> Class constraint: Subset.t ([A = int, B = int]) ([A = int])"
>
> From magicTable.ur, you use Subset.intro with folders to represent the
> class constraint. Is there a nice way to do that in this setting?
>
> Again, thank you for the help with this.
>
> Kindly, Mark.
>
> On 6/12/19 8:07 pm, Ziv Scully wrote:
>
> [Apologies for the double post, but wanted to correct a confusing typo I
> made: the word "sort" should be "sort of thing". There is no sorting
> algorithm here....]
>
> On Fri, Dec 6, 2019 at 2:05 PM Ziv Scully <zivscully at gmail.com> wrote:
>
>> Hi Mark,
>>
>> Here's how you'd write the function:
>>
>> fun update_ab [write] (sub : Subset.t [A = int, B = int] write) (w :
>> $write) =
>> Subset.elim
>> (fn [other] [write ~ other] _ _ pf =>
>> Eq.cast (Eq.symm pf) [record]
>> (Eq.cast pf [record] {A = 1, B = 2} --- write ++ w))
>>
>>
>> The basic idea is to use Subset.elim to "unpack" sub. This gives you
>> access to the type-level record other and the value pf, which allows you
>> to cast between {A : int, B : int} and $(write ++ other). You can't do
>> this sort outside of the function passed to Subset.elim because, among
>> other reasons, you don't know what other is.
>>
>> That said, this seems like a lot of work for what is a pretty simple
>> pattern, so I added some new functions to Subset that should help.
>>
>> val set :
>> fields ::: {Type} -> keep ::: {Type} -> t fields keep ->
>> $fields ->
>> $keep
>> -> $fields
>>
>> val over :
>> fields ::: {Type} -> keep ::: {Type} -> t fields keep ->
>> ($keep -> $keep)
>> -> $fields -> $fields
>>
>>
>> With either of these, your function is much simpler :).
>>
>> fun update_ab [write] (sub : Subset.t [A = int, B = int] write) (w :
>> $write) =
>> Subset.set {A = 1, B = 2} w
>>
>> fun update_ab [write] (sub : Subset.t [A = int, B = int] write) (w :
>> $write) =
>> Subset.over (fn _ => w) {A = 1, B = 2}
>>
>>
>> Hope that helps!
>>
>> Best,
>> Ziv
>>
>> On Fri, Dec 6, 2019 at 10:20 AM Mark Clements <mark.clements at ki.se>
>> wrote:
>>
>>> Ziv: thank you for this suggestion. Note that I have raised an issue on
>>> UrLib on an unrelated matter.
>>>
>>> After some head-scratching, I got as far as:
>>>
>>> fun update_ab [write] (sub : Subset.t [A=int,B=int] write) (w :
>>> $write) =
>>> {A=1,B=2} --- write ++ w
>>>
>>> which also does not work. Any guidance here would be appreciated - I
>>> admit to being stuck after looking closely at UrLib's subset.ur(s) and
>>> magicTable.ur(s).
>>>
>>> Kindly, Mark.
>>>
>>> On 29/10/19 4:39 pm, Ziv Scully wrote:
>>>
>>> One can capture subset constraints using a type class, as the following
>>> module does:
>>>
>>> https://github.com/vizziv/UrLib/blob/master/UrLib/subset.urs
>>> <https://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fvizziv%2FUrLib%2Fblob%2Fmaster%2FUrLib%2Fsubset.urs&data=02%7C01%7Cmark.clements%40ki.se%7Cd990bdb24bb54a4d7adc08d77a7fc2af%7Cbff7eef1cf4b4f32be3da1dda043c05d%7C0%7C0%7C637112561484327090&sdata=WX21odLl3MYxCLbMBFtIs%2FPzgXTqEvyAPoFkskuY2Jk%3D&reserved=0>
>>> https://github.com/vizziv/UrLib/blob/master/UrLib/subset.ur
>>> <https://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fvizziv%2FUrLib%2Fblob%2Fmaster%2FUrLib%2Fsubset.ur&data=02%7C01%7Cmark.clements%40ki.se%7Cd990bdb24bb54a4d7adc08d77a7fc2af%7Cbff7eef1cf4b4f32be3da1dda043c05d%7C0%7C0%7C637112561484337089&sdata=y%2BGTSLpNO9jOz0xLcWjxOzRgrEv7bT7d5%2BQLrQ%2Fudag%3D&reserved=0>
>>>
>>> (It relies on another module, Eq, from the same project.)
>>>
>>> Ziv
>>>
>>>
>>> On Tue, Oct 29, 2019 at 11:21 Mark Clements <mark.clements at ki.se> wrote:
>>>
>>>> Adam: thank you for your prompt reply.
>>>>
>>>> To define defaultSettings properly, is there some way to constraint the
>>>> type union (keep ++ change) to an existing type (e.g. {A:int, B:int})?
>>>> The following also do not work:
>>>>
>>>> fun defaultSetting
>>>> [keep] [change] [keep ~ change]
>>>> (args : $change)
>>>> : $(keep ++ change) =
>>>> update {A=1, B=1} args
>>>>
>>>> (* or *)
>>>>
>>>> fun defaultSetting
>>>> [keep] [change] [keep ~ change]
>>>> (args : $change)
>>>> : $(keep ++ change) =
>>>> {A=1,B=1} --- change ++ args
>>>>
>>>> -- Mark
>>>>
>>>> On 29/10/19 12:52 am, Adam Chlipala wrote:
>>>> > On 10/28/19 3:27 PM, Mark Clements wrote:
>>>> >> fun defaultSetting args =
>>>> >> update {A=1, B=1} args
>>>> >>
>>>> >> val _ = defaultSetting {A=2} (* {A=2, B=1} *)
>>>> >> val _ = defaultSetting {B=2} (* {A=1, B=2} *)
>>>> > The problem is that polymorphism in Ur/Web is always declared
>>>> > explicitly, not inferred as OCaml or Haskell. You must add binders
>>>> > for type variables for defaultSettings just as you did for update.
>>>> > (This statement applies to definitions of functions, not uses, so the
>>>> > two example calls above should work once you get defaultSettings
>>>> > defined properly.)
>>>>
>>>>
>>>>
>>>> När du skickar e-post till Karolinska Institutet (KI) innebär detta att
>>>> KI kommer att behandla dina personuppgifter. Här finns information om hur
>>>> KI behandlar personuppgifter<
>>>> https://ki.se/medarbetare/integritetsskyddspolicy>.
>>>>
>>>>
>>>> Sending email to Karolinska Institutet (KI) will result in KI
>>>> processing your personal data. You can read more about KI’s processing of
>>>> personal data here<https://ki.se/en/staff/data-protection-policy>.
>>>> _______________________________________________
>>>> Ur mailing list
>>>> Ur at impredicative.com
>>>> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>>>> <https://eur01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.impredicative.com%2Fcgi-bin%2Fmailman%2Flistinfo%2Fur&data=02%7C01%7Cmark.clements%40ki.se%7Cd990bdb24bb54a4d7adc08d77a7fc2af%7Cbff7eef1cf4b4f32be3da1dda043c05d%7C0%7C0%7C637112561484337089&sdata=l%2FOV5rcU3ra8BwP%2BWB%2BnH%2FkbZX1VG%2FHQmwRXLbkuUHs%3D&reserved=0>
>>>>
>>>
>>> _______________________________________________
>>> Ur mailing listUr at impredicative.comhttps://eur01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.impredicative.com%2Fcgi-bin%2Fmailman%2Flistinfo%2Fur&data=02%7C01%7Cmark.clements%40ki.se%7C46a639348ebc4f9a241108d75c865133%7Cbff7eef1cf4b4f32be3da1dda043c05d%7C0%7C0%7C637079604764057370&sdata=PQE3WAaKAftQmRM4kIKJ%2B%2BiqJG%2F%2BAW9D8dHeJ8ab0WY%3D&reserved=0 <https://eur01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.impredicative.com%2Fcgi-bin%2Fmailman%2Flistinfo%2Fur&data=02%7C01%7Cmark.clements%40ki.se%7Cd990bdb24bb54a4d7adc08d77a7fc2af%7Cbff7eef1cf4b4f32be3da1dda043c05d%7C0%7C0%7C637112561484347082&sdata=wNwz0jrC4fUcr2c4PHgV9xNu6s2zcYQEt24HieSV0tY%3D&reserved=0>
>>>
>>>
>>> _______________________________________________
>>> Ur mailing list
>>> Ur at impredicative.com
>>> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>>> <https://eur01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.impredicative.com%2Fcgi-bin%2Fmailman%2Flistinfo%2Fur&data=02%7C01%7Cmark.clements%40ki.se%7Cd990bdb24bb54a4d7adc08d77a7fc2af%7Cbff7eef1cf4b4f32be3da1dda043c05d%7C0%7C0%7C637112561484357077&sdata=yhgjOhsbD77Jync0VtjqoaCp0uI6FwU5yjhLN5i%2FoyI%3D&reserved=0>
>>>
>>
> _______________________________________________
> Ur mailing listUr at impredicative.comhttps://eur01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.impredicative.com%2Fcgi-bin%2Fmailman%2Flistinfo%2Fur&data=02%7C01%7Cmark.clements%40ki.se%7Cd990bdb24bb54a4d7adc08d77a7fc2af%7Cbff7eef1cf4b4f32be3da1dda043c05d%7C0%7C0%7C637112561484387062&sdata=ZQa3WuTFgN%2BNjRTz%2BRf0daJsr906GOcGZtgqbwSbPoQ%3D&reserved=0
>
>
> _______________________________________________
> Ur mailing list
> Ur at impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20191211/0048b065/attachment.html>
More information about the Ur
mailing list