溺潮69日
今天没有很正常地工作，不过对于我来说，一直处于不正常吧（笑）
Skim 了 Contextual Modal Type Theory，这是 08 年的 paper 了，很老。感觉 JohnSterling 的那个 MLTT-lock 就是后续衍生作吧，CMTT似乎没有让 necessity 在 dependent setting 下，也在 CMTT 的 future works 里看见了 dependent-necessity。
也 Skim 了 Modular Denotational Semantics for Effects with Guarded Interaction Trees ，这篇是对 Interaction Trees 的衍生作，似乎结合了 Guarded TT 与 Iris ，但是我不懂后两者，我就说说 ITrees ，这个我应该在2022年就Skim过，今年上半年的想法，似乎就是要用 ITrees 的样子，也就是那些可能不停机的程序。GITrees 这篇，整了 Higher Order functions/effects 这个，而香草(vanilla) ITrees 只能一阶，但是根据 related work 里说的，GITrees 不支持 extract 和 executable，这就让人感到恶心了吧，我最初喜欢（但是忘记了）ITrees 就是因为这个缘故，说不定是改进方向吧，单纯 reasoning 而没有 execution 果然还是不美。
Another difference worth mentioning, is that regular interaction trees can be extracted and executed from Coq. Our formalization cannot be directly extracted, as it is built upon a layer of guarded type theory.
然后这个从标题上就说 Denotational Semantics，根据我现在的印象，这下真是把 function (从 object-level) 拉到 meta-level 里了, Domain Theory 其实我不懂，完了，我怎么什么都不懂.
好了，今天就 Skim 到这，下班收工。
溺潮68日 20240907
头疼，感冒了应该是。
溺潮67日
去了三联的活动，以及今晚练琴了。
溺潮66日
Lilac 的那个 idea 果然有问题，没有那么简单，新想了一个版本，希望是正确的，不过即便如此，也就先这样放着吧，终止性虽然没问题，但是 modular 似乎还没那么简单，所以可以放一放。
昨晚因为这个以及没休息好的缘故，导致心情直接爆炸，没有练琴。
溺潮65日
早上改了一点项目代码，比较麻烦呢，输出格式，再改改然后暂时这么用着吧，代码可能还得再整理一下，然后跑多点测试例子才是重点，要为论文服务才行。
下午睡过去了，然后就是刚才去聚餐，哎，小学弟，怎么说喵，感觉我有点没带起来，他一个人坐在边角呜呜呜。
现在去练琴吧，还有洗澡。第一次剃须喵，好w
该规划一下周五的年轻人之夜了。
溺潮64日
Lilac 的那个新idea写了一点formalization，暂时还不是很确定是否能保证性质；
去看了《通往夏天的隧道，再见的出口》电影，感觉还挺好的，中等喜欢，限于83分钟的篇幅，我觉得很多细节不太能够到位吧，晚上和虎子哥去新东方阅读空间看到了实体小说，感觉有点差异，之后会去看看小说。我还是很爱这种异常性的小说，世界系吗？尽管很多恋爱桥段，几乎都是典中典了，我对虎子哥锐评这部电影时也是如此，因此我是中等喜欢而不是特别喜欢？但是女主的那句，我想去到你的世界，这样的想法，我还是很喜欢很喜欢的吧，时间流速差异导致的姐弟恋也是超绝（笑）。然后看的时候想到一个小点，延续着之前那个物理狂想的，关于神秘与确定的点：只有抛弃与你的最后的信物，我才能让你从确定复归不确定，只有这样，才能从迷雾中再次看见你。这样的先破后立，会是很棒的恋爱小说点子吧。我发觉我还是喜欢点子文学这一套，语不惊人死不休？郑渊洁害的。
下午学琴，被教了某个练习曲（BEAN SCENT）作为节奏练习，以及四组和弦的往返练习。我想，跟节拍器这点，还是往返地要重复，要用右手的节奏带动左手。
PS: 第二日才补的笔记，与虎子哥吃晚饭之后，或许一整天的奔波，还挺劳累的吧。
溺潮63日
今天继续来读 paper，是这篇 Capturing Types
感觉可以锐评 MoonBit 的 map:List[A] -> (A->B) -> List[B] 竟然不能支持 effects 了，即没办法 map:List[A] -> (A->B!E) -> List[B]!E，这篇paper可以解决相应的问题，并且保持 map 的签名仍为前者，感觉这个设计很棒。
这篇的contribution应该是提出了如何分析捕获变量以及变量逃逸，比较新颖的设计是引入了 Contextual Modal Type(Box/Unbox)，不让 capture sets 爆炸和不精确，2.x 的例子分析写得很棒。
Cap hierarchy 似乎比 row poly 要更舒服一点，cap sets 可以做得比较小。
Lilac 想到了个新的东西，开心子。
练琴的话，感觉稍微熟练了点，自己的意识也更好了些，主要是后者喵。
溺潮62日 20240901
怎么就9月了，哎。
上午看了 A Core Calculus for Documents: Or, Lambda: The Ultimate Document, 简单锐评两句，感觉构造比较复杂，但是那个 strtpl(string-template) 的branch 比较清楚了，涉及 set x = e 在 template 里面怎么处理，这里直接抽象出来一个 template list，在做 interpretation(文中称之为 desugaring, 额，行吧) 做一个特化, 大概形如下述:
(| set x = e :: tl |)_desugar = let x = e in (| tl |)_desugar然后其他的各种variant branch差不多，啥treetpl, reference, reforest 之类的，然后 reactive (响应式) 的都能在这套 doc calculus 上面做，大概是这么个思路，这个 interpretation 大概是分为了2层？这个let x = e 范式的就是这么嵌进去的，服了，因此我也想到和 staging 的关联吧，大概？语义上相似，语法上（指quasiquote）也相似。
然后可能总结一下这篇paper的contribution？感觉总结了一大类（就Table 1的8种情形，像 x=${x} 、Markdown 与 Typst），给了一个很好的 formalizaiton；然后还给了一个 type system for template(5.1) ，这里其实我也觉得是最 staging 的吧，对 staged-expression 的 typing 呗（笑），但是作者没这么显式说；reactive 与 reference 的 local/global 也有趣，还有 dirty update 相关的讨论，不过我还不是很清楚具体细节，就先读到这吧。PS: reforestation 也有意思，语义(desugaring) 跟 set x = e 的形式比较像。
评价就是，我觉得工作很充分，但是要说有什么 novelity？我不确定，或许前面确实没有人做过相关的工作吧（草）。这里与 pretty printing 的关系我觉得也是可以延申一下的，我觉得像啊，很像啊，这个 staging 的 semantics/desugaring。
哎，下午 lilac 继续，然后晚上练琴，洗澡游戏！练琴感觉，要连贯流畅确实是一个很需要练习的地方呢！
溺潮61日
今天睡了很久，出门去麦麦吃好吃的了，吃了之后回办公室把项目的bug给搞清楚了，哎，永远都会被typo杀死吗？
吃晚饭后报修了下马桶，怎么塞住了，烦捏，然后练习了一小时的琴，难受子，记不住降八度升八度的位置在哪里，怎样才能更快地记住呢，条件反射般地期望。现在准备洗澡洗头和玩游戏啦~
溺潮60日 20240830
夏末了，但是突然变热、33℃，北京这是怎么了，久违地再开空调，中午睡觉时就感觉有点热，但是还没反应过来就睡着了。
溺潮59日
狠狠地继续写 lilac，应该说这样的才配得上溺潮的观感？但是也太过了吧，以至于没有练习吉他，日常练习还是得做。
溺潮58日
吉他练习了，然后写了lilac的notes，越写越上头喵，打算用Rust重写了。
溺潮57日 20240827
今天去学了吉他的第一节课，要去弹音阶了，一个要背熟音符在吉他上的位置，另一个是具体操作上的，左手要按住喵，按稳了喵。另外是，我似乎跟节拍还是不太行，之后还得练习一下子。
另外今日狂飙式补原神4.8的版本活动，可惜，最后只能拿了绮良良的皮肤，而角色本体没法拿到，对于萌新来说太难了，没有练度。
关于工作，明天应该要进行吧、感叹。