[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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 >>> [email protected] >>> 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 >> [email protected]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 >> >> >> _______________________________________________ >> Ur mailing list >> [email protected] >> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur >> >
_______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
