<div dir="ltr">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".<div><br></div><div>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".</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Dec 11, 2019 at 5:57 AM Mark Clements <<a href="mailto:mark.clements@ki.se">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,<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>On 6/12/19 8:07 pm, Ziv Scully wrote:<br>
</div>
<blockquote type="cite">
<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" target="_blank">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">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" target="_blank">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" target="_blank">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">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">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">https://ki.se/en/staff/data-protection-policy</a>>.<br>
_______________________________________________<br>
Ur mailing list<br>
<a href="mailto:Ur@impredicative.com" target="_blank">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" rel="noreferrer" target="_blank">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">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" target="_blank">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">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" rel="noreferrer" target="_blank">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br>
</blockquote>
</div>
</blockquote>
</div>
<br>
<fieldset></fieldset>
<pre>_______________________________________________
Ur mailing list
<a href="mailto:Ur@impredicative.com" target="_blank">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%7C637112561484387062&sdata=ZQa3WuTFgN%2BNjRTz%2BRf0daJsr906GOcGZtgqbwSbPoQ%3D&reserved=0" target="_blank">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>
</div>
_______________________________________________<br>
Ur mailing list<br>
<a href="mailto:Ur@impredicative.com" target="_blank">Ur@impredicative.com</a><br>
<a href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" rel="noreferrer" target="_blank">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br>
</blockquote></div>