[Ur] Default settings using a generic record update

[Ziv Scully]

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/49c3dafd/attachment.html>