[Ur] Default settings using a generic record update

Mark Clements mark.clements at ki.se
Wed Dec 11 05:55:57 EST 2019 

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<mailto: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<mailto: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<mailto: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<mailto: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 list
Ur at impredicative.com<mailto:Ur at impredicative.com>
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%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<mailto: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 list
Ur at impredicative.com<mailto:Ur at impredicative.com>
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%7C637112561484387062&sdata=ZQa3WuTFgN%2BNjRTz%2BRf0daJsr906GOcGZtgqbwSbPoQ%3D&reserved=0


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20191211/12f1ef24/attachment-0001.html>

More information about the Ur mailing list