[Ur] Default settings using a generic record update
Ziv Scully
zivscully at gmail.com
Fri Dec 6 14:07:57 EST 2019
[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%7C46a639348ebc4f9a241108d75c865133%7Cbff7eef1cf4b4f32be3da1dda043c05d%7C0%7C0%7C637079604764017394&sdata=ueZ7e9P7Rzqhq7P4vuBDpbcq8QbIYA5i8vhL9%2BgCvEc%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%7C46a639348ebc4f9a241108d75c865133%7Cbff7eef1cf4b4f32be3da1dda043c05d%7C0%7C0%7C637079604764027387&sdata=RDT9vPh4qegdK9iiBr%2F2K7vpFc4z%2BF2y4cHa2eDe5Tw%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%7C46a639348ebc4f9a241108d75c865133%7Cbff7eef1cf4b4f32be3da1dda043c05d%7C0%7C0%7C637079604764027387&sdata=DQN4vR4Qr7o7m6U4zF6BnCKBn%2B2pWf5TSdKv0nt5G60%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
>>
>>
>> _______________________________________________
>> 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/20191206/fbae4e78/attachment-0001.html>
More information about the Ur
mailing list