<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
Ziv,<br>
<br>
Thank you for this. I had hoped that the following code would work:<br>
<br>
con ab = [A=int, B=int]<br>
<br>
fun update_ab [write] (sub : Subset.t ab write) (w : $write) =<br>
Subset.set {A=1,B=2} w<br>
<br>
fun main () =<br>
let<br>
val a = update_ab {A=2} (* [line 8] {A=2, B=2} *)<br>
in<br>
return <xml><br>
<body><br>
a.A: {[a.A]}<p/><br>
</body><br>
</xml><br>
end<br>
<br>
However, I get an error "[line 8] Can't resolve type class instance<br>
Class constraint: Subset.t ([A = int, B = int]) ([A = int])"<br>
<br>
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?<br>
<br>
Again, thank you for the help with this.<br>
<br>
Kindly, Mark.<br>
<br>
<div class="moz-cite-prefix">On 6/12/19 8:07 pm, Ziv Scully wrote:<br>
</div>
<blockquote type="cite" cite="mid:CADK8yDT1HkARJsg1zWvojWrb5w5G=fED_8hPREOqPrNBmHxfrA@mail.gmail.com">
<div dir="ltr">[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....]</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Fri, Dec 6, 2019 at 2:05 PM Ziv Scully <<a href="mailto:zivscully@gmail.com" moz-do-not-send="true">zivscully@gmail.com</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">
<div dir="ltr">Hi Mark,
<div><br>
</div>
<div>Here's how you'd write the function:</div>
<div><br>
</div>
</div>
</div>
<blockquote style="margin:0px 0px 0px
40px;border:none;padding:0px">
<div>
<div>
<div><font face="monospace">fun update_ab [write] (sub : Subset.t [A = int, B = int] write) (w : $write) =</font></div>
</div>
</div>
<div>
<div><font face="monospace"> Subset.elim</font></div>
<div><font face="monospace"> (fn [other] [write ~ other] _ _ pf =></font></div>
<div><font face="monospace"> Eq.cast (Eq.symm pf) [record]</font></div>
<div><font face="monospace"> (Eq.cast pf [record] {A = 1, B = 2} --- write ++ w))</font></div>
</div>
</blockquote>
<div dir="ltr">
<div dir="ltr">
<div><br>
</div>
<div>The basic idea is to use <font face="monospace">Subset.elim</font> to "unpack" sub. This gives you access to the type-level record
<font face="monospace">other</font> and the value <font face="monospace">pf</font>, which allows you to cast between
<font face="monospace">{A : int, B : int}</font> and <font face="monospace">$(write ++ other)</font>. You can't do this sort outside of the function passed to
<font face="monospace">Subset.elim</font> because, among other reasons, you don't know what
<font face="monospace">other</font> is.</div>
<div><br>
</div>
<div>That said, this seems like a lot of work for what is a pretty simple pattern, so I added some new functions to
<font face="monospace">Subset</font> that should help.</div>
<div><br>
</div>
</div>
</div>
<blockquote style="margin:0px 0px 0px
40px;border:none;padding:0px">
<div>
<div style="color:rgb(0,0,0)"><font face="monospace">val set :</font></div>
<div style="color:rgb(0,0,0)"><font face="monospace"> fields ::: {Type} -> keep ::: {Type} -> t fields keep -></font></div>
<div style="color:rgb(0,0,0)"><span style="font-family:monospace"> $fields -></span></div>
<div style="color:rgb(0,0,0)"><font face="monospace"> $keep</font></div>
<div style="color:rgb(0,0,0)"><span style="font-family:monospace"> -> $fields</span></div>
<div><font face="monospace"><br>
</font></div>
<div><font face="monospace">val over :</font></div>
</div>
<div>
<div>
<div>
<div><font face="monospace"> fields ::: {Type} -> keep ::: {Type} -> t fields keep -></font></div>
</div>
</div>
</div>
<div>
<div>
<div>
<div><font face="monospace"> ($keep -> $keep)</font></div>
</div>
</div>
</div>
<div>
<div>
<div>
<div><font face="monospace"> -> $fields -> $fields</font></div>
</div>
</div>
</div>
</blockquote>
<div dir="ltr">
<div dir="ltr">
<div><br>
</div>
<div>With either of these, your function is much simpler :).</div>
<div><br>
</div>
<blockquote style="margin:0px 0px
0px 40px;border:none;padding:0px">
<div>
<div style="color:rgb(0,0,0)"><font face="monospace">fun update_ab [write] (sub : Subset.t [A = int, B = int] write) (w : $write) =</font></div>
<div><font style="color:rgb(0,0,0)" face="monospace"> Subset.set </font><font face="monospace" color="#000000"><span>{A = 1, B = 2} </span></font><span style="color:rgb(0,0,0);font-family:monospace">w</span></div>
</div>
<div style="color:rgb(0,0,0)"><font face="monospace"><br>
</font></div>
<div style="color:rgb(0,0,0)"><font face="monospace">fun update_ab [write] (sub : Subset.t [A = int, B = int] write) (w : $write) =</font></div>
<div style="color:rgb(0,0,0)"><font face="monospace"> Subset.over (fn _ => w) {A = 1, B = 2}</font></div>
</blockquote>
<div><br>
</div>
<div>Hope that helps!</div>
<div><br>
</div>
<div>Best,</div>
<div>Ziv</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Fri, Dec 6, 2019 at 10:20 AM Mark Clements <<a href="mailto:mark.clements@ki.se" target="_blank" moz-do-not-send="true">mark.clements@ki.se</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">
<div>Ziv: thank you for this suggestion. Note that I have raised an issue on UrLib on an unrelated matter.<br>
<br>
After some head-scratching, I got as far as:<br>
<br>
fun update_ab [write] (sub : Subset.t [A=int,B=int] write) (w : $write) =<br>
{A=1,B=2} --- write ++ w<br>
<br>
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).<br>
<br>
Kindly, Mark.<br>
<br>
<div>On 29/10/19 4:39 pm, Ziv Scully wrote:<br>
</div>
<blockquote type="cite">
<div>
<div dir="auto">One can capture subset constraints using a type class, as the following module does:</div>
</div>
<div dir="auto"><br>
</div>
<div dir="auto">
<div><a href="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" originalsrc="https://github.com/vizziv/UrLib/blob/master/UrLib/subset.urs" shash="jodSdp4DDU9/VblboRNSHlgiSCTR3kP/dCDGjhR4ELv2o+SUIbQXR3t991o0oeTW9LdpULKmOJdJL8+XXLbP7CAhJtl9knGzWN+iN3q6vY5bXyPIXpSmqcuG+gjP9yUnKnXaOHjv2BeLA4aHhoEZr5q3QuaLbdMQunqNzhCC7nM=" target="_blank" moz-do-not-send="true">https://github.com/vizziv/UrLib/blob/master/UrLib/subset.urs</a></div>
<div><a href="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" originalsrc="https://github.com/vizziv/UrLib/blob/master/UrLib/subset.ur" shash="f7eF07AJ47c9p5j0WZIB1baFWwsNaM3ryA+ghBp6pLiExpx+5a2tFu4GJe6PcqhzyQXsY3qF/y/apuqXwhJZDoOeFYpG6TuyUlge+lauhAkqelVSkk3b13IJRvcvAEJfrtVBzXgq3jm8jdXyPav4R8T+7CAmbTd40JzAanITtHM=" target="_blank" moz-do-not-send="true">https://github.com/vizziv/UrLib/blob/master/UrLib/subset.ur</a></div>
<br>
</div>
<div dir="auto">(It relies on another module, Eq, from the same project.)</div>
<div dir="auto"><br>
</div>
<div dir="auto">Ziv</div>
<div dir="auto"><br>
</div>
<div><br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Tue, Oct 29, 2019 at 11:21 Mark Clements <<a href="mailto:mark.clements@ki.se" target="_blank" moz-do-not-send="true">mark.clements@ki.se</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px
0px 0px
0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">
Adam: thank you for your prompt reply.<br>
<br>
To define defaultSettings properly, is there some way to constraint the<br>
type union (keep ++ change) to an existing type (e.g. {A:int, B:int})?<br>
The following also do not work:<br>
<br>
fun defaultSetting<br>
[keep] [change] [keep ~ change]<br>
(args : $change)<br>
: $(keep ++ change) =<br>
update {A=1, B=1} args<br>
<br>
(* or *)<br>
<br>
fun defaultSetting<br>
[keep] [change] [keep ~ change]<br>
(args : $change)<br>
: $(keep ++ change) =<br>
{A=1,B=1} --- change ++ args<br>
<br>
-- Mark<br>
<br>
On 29/10/19 12:52 am, Adam Chlipala wrote:<br>
> On 10/28/19 3:27 PM, Mark Clements wrote:<br>
>> fun defaultSetting args =<br>
>> update {A=1, B=1} args<br>
>><br>
>> val _ = defaultSetting {A=2} (* {A=2, B=1} *)<br>
>> val _ = defaultSetting {B=2} (* {A=1, B=2} *)<br>
> The problem is that polymorphism in Ur/Web is always declared<br>
> explicitly, not inferred as OCaml or Haskell. You must add binders<br>
> for type variables for defaultSettings just as you did for update.<br>
> (This statement applies to definitions of functions, not uses, so the<br>
> two example calls above should work once you get defaultSettings<br>
> defined properly.)<br>
<br>
<br>
<br>
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<<a href="https://ki.se/medarbetare/integritetsskyddspolicy" rel="noreferrer" target="_blank" moz-do-not-send="true">https://ki.se/medarbetare/integritetsskyddspolicy</a>>.<br>
<br>
<br>
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<<a href="https://ki.se/en/staff/data-protection-policy" rel="noreferrer" target="_blank" moz-do-not-send="true">https://ki.se/en/staff/data-protection-policy</a>>.<br>
_______________________________________________<br>
Ur mailing list<br>
<a href="mailto:Ur@impredicative.com" target="_blank" moz-do-not-send="true">Ur@impredicative.com</a><br>
<a href="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" originalsrc="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" shash="pSStF2EReiMDoPGk5hG+BReQCWGLKfbLeC5mJT65Dj3KtCoy6Ya+hsAXh5WYDrmVDOoG8p1zRPEBno78VKXR+PU38DS/PsPUBGTZDT2dBJYz/w5F3e29HMjMpBrnGW0uwMocp7OGrUYBPf8Zfw2X5RG9mwKJQqXhrDbzb923/SY=" rel="noreferrer" target="_blank" moz-do-not-send="true">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br>
</blockquote>
</div>
</div>
<br>
<fieldset></fieldset>
<pre>_______________________________________________
Ur mailing list
<a href="mailto:Ur@impredicative.com" target="_blank" moz-do-not-send="true">Ur@impredicative.com</a>
<a href="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" originalsrc="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" shash="rn47SfBN0cqiptjkarcWI3tXarl7N8lcSxf1e48Wy6pblsiWIrrSubS+4fvnZXHNGvdaJ4E3nB02CDXmK3GVy7hC1AjkL411M4BBI9QnbT5fSAxhmHF1Yp/RhiS00KfTss5I05fJj79GZIkrHHQrq/gXvMUCJfEx4mCodzjnKEo=" target="_blank" moz-do-not-send="true">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</a>
</pre>
</blockquote>
<br>
</div>
_______________________________________________<br>
Ur mailing list<br>
<a href="mailto:Ur@impredicative.com" target="_blank" moz-do-not-send="true">Ur@impredicative.com</a><br>
<a href="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" originalsrc="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" shash="E4p1UDqQ5gGQsxQ4bdTr0qgrxZNgegl/IfdgzzGVVhb9TA1Ihgzbk7rty+c13yoEGS1TTGsOuGcHeTZJENXE/IDmCnd3/DEEOXMR+K3ZQI9HmrM6BQSu7qyfpH/OUnzNI7gtTCn1XACmGSa2xdwk5WkjB/mA2GmVaSJxtd/EN7g=" rel="noreferrer" target="_blank" moz-do-not-send="true">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br>
</blockquote>
</div>
</blockquote>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Ur mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Ur@impredicative.com">Ur@impredicative.com</a>
<a class="moz-txt-link-freetext" href="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">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</a>
</pre>
</blockquote>
<br>
</body>
</html>