間違いなく賢くないんだよなあ
Debian on Vagrant with VirtualBox on Debian on UTM on M1 Mac は賢い？
Mastodon は Ansible provision で立ててくことをとりあえず目指すことにした
技術系の記事は自分が後で読んで分かるように整理するのが大事なんだけど、創作はそうじゃないからなあ。妄想さえ膨らめばいいし、過去に縛られる必要がないというか
創作、人に伝える努力までしたくないところがネック。なんか自分で分かったらそれで満足しちゃうというか、別に人に読んでもらわなくても楽しいというか
やっぱ Mastodon の share リンク、導線なさすぎて死ぬほど使い難くないか？なんか使い方間違えてんのかな
書いた | 続くといいな日記 – Mastodon へのシェアボタンを追加した https://mizunashi-mana.github.io/blog/posts/2023/03/mastodon-share-button/
まあ日本語は、責任回避に優れた機能を持っているという面は否めないし、そう言う方向で使ってる人も多いと思うが (僕もそう言う方向でも使ってる時はあるが)、「思っている」みたいな表現を封殺するとそれはそれで情報伝達に齟齬が生じるというか、まあそんな感じ
そういや何かで見て、元を忘れてしまったので供養という感じ。
「〜と思います」「〜と聞きました」というのが責任をとりたくない人の発言、もっとちゃんと責任もって断言しろよみたいなやつについてなんだが、気持ちは分かるんだが、あれって責任を取りたいか取りたくないかと別軸として、事実を言うべきかどうかという話があると思っている (これも責任回避のための「思っている」ではない)。個人の意見をまるで事実かのように断言してしまうと、それって他の人の意見を封殺することになるし、事実誤認にもつながる。なので、「思っている」と言ってもらうこと、つまり個人の意見であると表明してもらうことって事実確認としてはかなり大事なことなんだよなという
@elpinal ただ、確かに unification が必要ないと言うのは、bidirectional typing の文脈で度々聞くので自分の考察にあまり自信が持てなかったと言う感じです
多相型のない世界だと多分 unification が必要ないというのは誇張でもないと思うのですが、多相型のある世界だと unification を導入するのもそれほど間違った方向ではないのかなと言う感じです (もちろん、unification を導入しない方向もあると思います。ただ、導入するのが正しい、導入しないのが正しいと言う話ではないのかなと言う感じです)
@elpinal
> unificationは暗黙のinstantiationを扱うための機構でしかなく、bidirectional typecheckingの本質とは言えないんじゃないかなと思います
僕の主張を明確にしておくと、
* unification が必要になるかならないか、unification を使った方が実装が楽になるかならないかは、bidirectional typing の本質ではない
* HM-type system と比べて多相型を扱うアルゴリズムが楽に作れるか作れないかは bidirectional typing の本質ではない
* bidirectional typing の本質は、あくまで双方向性であり、synthesize / check 2 つの mode をモデルに落とし込める点
と言う感じです。なので、
https://mi.mashiro.site/notes/9bx61n73ku
> bidirectional typecheckingっていうのはunificationをしないことで実装が簡単になる
に反論があっただけでした
