めっちゃ効きそう
> AWS Private CA失効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効効 OCSP では
https://docs.aws.amazon.com/ja_jp/privateca/latest/userguide/PcaRevokeCert.html
Debian bullseye で立てた後にすぐ bookworm にアップグレードすることになりそうだな
bookworm はもう hard freeze したんか
https://release.debian.org/bookworm/freeze_policy.html
Debian testing に今載ってる Ruby は 3.1 なんだな。3.2 は間に合わなんだか
ローカルで make vagrant-up すれば一発で Mastodon 鯖立てられるようにしたので、遊んでる
人間もそう複雑なはずがないんだから、インジェクションの口ぐらいありそうだが、人権という壁があるのがネック
プロンプトインジェクションにより悪い人に支配されちゃったロボットたちを、プロンプトインジェクションで過去の思い出とともに元に戻して回るゲームを妄想するなどした
ポケモンBGMがいっぱいのWebサイト #ポケモンゲームサウンドライブラリー ！
今わたしが聴いているのはこの曲！
きみも1曲、いかがですか？
戦闘！チャンピオン（ポケットモンスター ダイヤモンド・パール） https://soundlibrary.pokemon.co.jp/musicbox?id=dp-145
いや、まあ全部形式的に考えようとか、形式的に考えないのはよくないという話ではなく、単純に数学において本当に形式的な話してるとこってあまりないよなっていう話。つまり、数学は形式さがものをいう分野ではないんだよなあ
等価関係とか何も考えずに使いがちだけど、いざじゃあ何が成り立てば等価関係で、どういう推論できるのって言われたらアバウトにならざるを得ない、そんな基礎がゆるふわな分野が数学の大部分を作っているわけで、そんな人たちが形式的に考えてるわけないよなあっていう
大体の数学分野、標準ライブラリをなんとなく使えばなんとかなるし、相手納得させれば勝ちなので、普通に論理の飛躍含むこと可能っていう
いい感じにはなってきた。しかし、完全な自動化は諦めやな
https://github.com/mizunashi-mana/mizunashi-work-playbook
このアカウントは、notestockで公開設定になっていません。
クソコード量産したり、細かいとこ自分好みに修正したり、バグ調査はやるんで、AI さんはそれ以外のことを担ってくれ
AI でプログラマの仕事がなくなるとか煽るんじゃなくて、AI がメンテしてくれるようになるので好き勝手コード書いていける世界目指そうぜw とは思う
自動でコード生成してくれるやつでソフトウェア作られたら、結局一番楽しいところがなくなって、辛いメンテ業務だけが残るやつでしょ
private CA、構築してる人は構築してるけど、やっぱ絶対数として構築してる人あんまいない印象だな
世の中には治安の悪いブラウザとサイトとプロバイダが多いって分かって、ニコニコしてる
alert rule は config 書いて deploy したい、scrape 先 / rule の状態管理は Web UI から管理したいんだよなあ
これ便利なんだけど、欲しいのはこれじゃないんだよな感はある
https://line.github.io/promgen/
そろそろ Ruby 3.0 のノーマルメンテは終わるよな。Life 自体は 2024/3 まで続くっぽいが
https://www.ruby-lang.org/ja/downloads/branches/
そういや、ここで Ruby 3.0.4 使ってるのは何故なんだ。更新されてないだけ？
https://docs.joinmastodon.org/admin/install/
@tadd おひとり様 Mastodon サーバでの利用を想定してるので、スループットよりは省メモリでの安定性が欲しいですね
Ruby 3.0.4 + jemalloc vs Ruby 2.7.4 でどんくらい性能に違い出るかだな
まあ、Ruby の deb ぐらい気が向いたら作るか。しかし、Ruby の security updates 追ってないので、メンテしていけるかが問題なんだよなあ
各個でサーバ立てる思想のソフトウェアが、セットアップに Ruby build / bundle install / yarn install を各サーバでやらせるの、割と正気を疑う (いや、まあ Rails 系ではそれが普通なのは知ってるが...)
Mastodon 公式の systemd services、ちゃんとしてるようで割と適当だよな。分かってる人は自分で変えろってスタイルか。sidekiq って、redis 死んでても、ちゃんと立ち上がるまで死なずに待ってるんか？
ソースコード直置きサーバが、いろんなところで動いてるの正気じゃないな。アップグレードとかどうしとるんや。git checkout やってんのか？
mastodon、だれか gem package 作ってる人おらんのか
今なら大体 kernel がなんとかしてくれるでしょw してくれないんかな
まあおいおい rule と system properties の方も見直した方が良さそうだな
改めて nftables のルール見直しとるけど、ping flood 対策を ping death 対策と言ってたり、結構めちゃくちゃやった
ようやく playbook 書き始めた
https://github.com/mizunashi-mana/mizunashi-work-playbook
Ubuntu のことよく知らんが、Ubuntu は今だに iptables 使っとるんか？
https://docs.joinmastodon.org/admin/prerequisites/
ロケット打ち上げたいわけではないんよ。ロケットが打ち上げられるようになって何がしたいか何だよなあ
打ち上がらなきゃ話は始まらんが、打ち上がったら話が始まるわけではないんだよなあ
ロケット打ち上げに実際に携わってる人と、傍観してる人で、あまりに考えてる戦略が違いすぎるんだろな
H3ロケット打ち上げ失敗で分かったことは、どうやら世の中の人はとりあえず打ち上がればいいと思ってるらしいということだな
Microsoft Store で Debian って検索してインストールボタン押すと Windows で Debian が動くって、10年前に言ったら正気を疑われるシリーズやん
Vagrant で generic/debian10 box 動かしたいだけなのに...
@elpinal まだ、やっぱり「Bidirectional Typing でモデル化すると型検査の実装が簡単になる」や「Bidirectional Typing では単一化は必要ない」みたいな主張には強い抵抗はありますが、なんとなくそういう主張の出所というか、そう主張する動機は理解できた気がします。
ありがとうございます！
@elpinal 改めてリプライツリーを見ていて、
* 言語の本質的な型付け可能性に対する難しさ (bidirectional typing でそもそもモデルをどう作るか)
* bidirectional typing が作れた時のアルゴリズム生成の難易度
は分けて考えられ、「bidirectional typing が作れた時のアルゴリズム生成の難易度」についても
* bidirectional typing の基本的な規則から生成された部分の取り扱い
* モデル特有の判定に対して生成されたアルゴリズム
も分けて考えられ、実装の簡単さに寄与する部分は「bidirectional typing の基本的な規則から生成された部分の取り扱い」の部分という話なのかなと少し思いました。確かにそれでいうと、Dunfield & Krishnaswami 2013 の本質的に単一化 like なアルゴリズムや global な状態が必要になってる部分は、「モデル特有の判定に対して生成されたアルゴリズム」の部分なのかなという気はしてきました。
@elpinal なるほど、確かにそれはそうかもしれないですね。
ただ、多相型を扱う、つまり Algorithm W が扱える範囲以上のものを扱うとなると、結局何らかの状態の保存と単一化のような仕組みが bidirectional typing でも必要になってくる気がして、そこまでいくと bidirectional typing を元にしたアルゴリズムの生成や実装が Algorithm W の拡張などと比べて簡単であるという主張は誇張な気がしていて、ちょっと疑問を感じていた点でした。
Debian on Vagrant with VirtualBox on WSL Debian on Windows on Remote Desktop
になった
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をしないことで実装が簡単になる
に反論があっただけでした
@elpinal ありがとうございます。
> bidirectional typecheckingの中でも、多相型、特に暗黙のinstantiationを扱うものが大変ということです。
これはそう思います。STLC のような体系の場合や多相型の特殊化、一般化は必ず注釈をつける必要があるみたいな体系では、もう少し自然に双方向の型システムが作れると思います。
【#H3 】H3ロケット試験機1号機 打上後記者会見 #りあライブ アーカイブ視聴会🌟 2023.3.7 #Vtuber 【#宇推くりあ 】 https://www.youtube.com/live/Ir4gcDdXjto?feature=share
ファルコン1なんて、延期しまくって、2回破壊して、そこからようやく成功やからな。ま、さっさと再計画して、再打ち上げ目指してこうとしか思わんわ
成功するまで失敗してこうぜってできないのが、金がかかるプロジェクトの辛いとこか
【#H3 】H3ロケット試験機1号機 先進光学衛星だいち3号 ミッション #りあライブ パブリックビューイング🌟 2023.3.7 #Vtuber ... https://www.youtube.com/live/JbS_g77eZwc?feature=share
Mastodon icon の svg で、いい感じのライセンスのってあるかな？
本当に簡単な図形なら、font awesome に頼る必要ないな
後は自動遷移実装して、reset 実装して、About page 書いて、言語選択実装したら完成！案外やること多いな
これ気持ちわかるけど、本来文句言う先は検索側か、Qiita 側なんだよな
このアカウントは、notestockで公開設定になっていません。
Mastodon の share link、投稿した後 portal 画面に戻る動線がなくて、ログアウトしかできないの微妙やな
vivaldi.net のリダイレクタが、CORS header 返してこないので、Web finger 叩くのに失敗するな
Misskey とかもこういうの作れんのかな？ Mastodon しか見てないけど
@elpinal ありがとうございます。こういうフィードバックがもらえる機会はあまりないので、ありがたいです
@elpinal scope があるのはあくまで変数生成においてであって、変数のインスタンス化が起こるところではなく、これは Algorithm W でも取り入れられると思っています (Algorithm W も、単一化で変数を生成しているわけではなく、また別に生成した変数を最後まで残す必要はないので。逆に bidirectional typing で残す実装にしてもいいはずです)
@elpinal Sub 規則では、基本 G |- e <= t1 の parameter G, e, t1 が全て入力になるわけですが、そこから G |- e => t2 で、e の型 t2 を synthesize して、synthesize した t2 から入力の t1 が subtyping 関係を満たせるかという検証を行います。これは、例えば subtyping が equal しかないならまさに unification で、t1, t2 が変数を全く含まない場合も、変数を複数含むことも、どちらも単なる変数でない大きな型であることもありえます。実際、https://dl.acm.org/doi/10.1145/2500365.2500582 では、subtyping の検証で変数と型の比較以上のことをしていて、その過程で変数のパターンマッチを行うため、hat{a} = t みたいな制約を環境に入れてます。変数の cyclic 使用のチェックなども入っていて、個人的には MM unification algorithm の純粋な拡張に思えました
@elpinal 確かに、Agda のコードを読んでましたが、あまり双方向検査やってないように思えてきましたね。ちょっと修正しときます
ついでに、bidirectional typechecking で単一化が必要ないって話ってどこが発祥かご存知ですか？少なくとも、https://dl.acm.org/doi/10.1145/2500365.2500582 を読んだ感じは、単一化相当のものは sub 規則で必要になってましたし、単一化アルゴリズムを直接使うような構成方法も普通にできるように思えました。また、今のところ単一化が入ってないことを要件にしている文献が見つけられていません
@elpinal ただ、Agda はそこまで使ったことはないので、あまり自信がなくて、https://github.com/agda/agda/blob/71a6396ba727768910ed48e2da910532fdb66a63/src/full/Agda/TypeChecking/CheckInternal.hs は双方向検査 (unification あり) が入ってそうですし、bidirectional type checker とコメントに書いてあるので、共通認識がありそうな気がするんですが、こいつが表層レベルの推論で使われているかは https://github.com/agda/agda/blob/71a6396ba727768910ed48e2da910532fdb66a63/src/full/Agda/TypeChecking/Rules/Term.hs 見てもよくわからないなって感じでした
@elpinal なるほど？僕個人は unification を使わないことは、bidirectional typing の定義には含んでいませんでした。実際、さっき書いた記事は unification っぽいことは普通にしてますね
https://arxiv.org/pdf/1908.05839.pdf でも、
> Another extension to ... use bidirectional typing to produce GADT-related
annotations, which provide the missing information for non-bidirectional type inference. OutsideIn ... also use bidirectional typing for
GADTs. Both use unification to propagate equality information.
とあり、unification を使わないことは bidirectional typing の要件に入ってないように思えます
@elpinal Scala の方は嘘だった... 訂正しました。申し訳ないです。指摘ありがとうございます。
Agda の方は合ってそうです。一応注釈つけときました。https://github.com/agda/agda/blob/71a6396ba727768910ed48e2da910532fdb66a63/src/full/Agda/TypeChecking/CheckInternal.hs を軽く流し読みした感じは、双方向に検査する実装使ってそうですね
Scala が双方向型検査使ってるは嘘だった。申し訳ねえ。訂正した
@elpinal 嘘かもしれない。https://plfa.github.io/20.07/Inference/#bidirectional-inference-in-agda を見て雑にそうなんだとか思ってたが、そういや後でちゃんと調べようと思ってそのままにしてた... ちょっと調べて後で参考注釈足しときます
書いた | 続くといいな日記 – 双方向型検査: 検査と構築の融合 https://mizunashi-mana.github.io/blog/posts/2023/02/bidirectional-typing/
今月中に終わらんと Hostdon から請求が来ちゃう。締切駆動開発じゃん
とりあえず bidirectional typing survey 記事書けたので、Mastodon サーバ構築やってくぞって気持ち
の投稿
romantic1000@misskey.io
このアカウントは、notestockで公開設定になっていません。
RSS to ActivityPub の Manged service が流行って、公共がそれ利用するようになれば、Twitter / Facebook / Instagram アカウント開設とかいう意味わからん状況打開できるのでは？感がある (そう簡単には行かんか)
このアカウントは、notestockで公開設定になっていません。
Bing AI はよ、stack overflow 翻訳広告貼りサイトとか、いかがでしたかサイトとか、滅ぼしてくれ
misskey io が動いてると断然 HTL の流速が違うので、人口を感じる
Activity-Relay v2.0.0 をリリースしました 🎉
このバージョンでは、 Pleroma やそのフォークからも利用できるようになりました 🎉
いくつかの重要な破壊的変更と注意があるため、リリースページをよく確認してください！
- Release v2.0.0 · yukimochi/Activity-Relay https://github.com/yukimochi/Activity-Relay/releases/tag/v2.0.0
このアカウントは、notestockで公開設定になっていません。
中毒性がある。ファルコム中毒性がある曲作るのが上手い
#NowPlaying 神代の地 / イース セルセタの樹海 オリジナルサウンドトラック / ファルコム・サウンド・チーム・JDK
#AppleMusic
このアカウントは、notestockで公開設定になっていません。
user id と domain 入力してもらって local storage に突っ込んどいて、次回以降それ見て web-finger で endpoint 取ってきて、投稿するみたいな感じか。これなら、できそう。参考にさせてもらお
なんか form 立ち上がる実装に見えるが、立ち上がらんな。しかし、なるほど、何となく実装の仕方はわかった > Mastodon Share ボタン
Scala.js 製？良さそうだが、動かんかった😇 | マストドンのシェアボタンを自作した(追記あり)(今日から使えます) - Lambdaカクテル https://blog.3qe.us/entry/2023/01/26/220631
いや、正確には bidirectional typing がむずいというより、System-F がむずいわけだが
これ decidable かつ sound なまま拡張できる人おるん？
双方向型検査、永遠とわかる分からないを繰り返してる。ちょっと難しすぎんか？
Universal domain 検索性ゴミやな。まあ普通話題にせんか。その昔、「untype lambda の項に対して型ってどうなるんやろ？」と考えた人がいて、「なんかうまいモデルないかな？せや、λx.x と (λx.x) (λx.x) には型的な違いはないことにしよ。untyped lambda は uni-typed lambda や」で、モデルが上手く作れちゃった話があってなみたいな
この考えは分かるが分からないという感じがある。個人的には型は結局モデルによってかなり変わってくるし、その中でプログラムに実用的なモデルの型が選ばられてるというのが実情だと思っていて、その意味で普遍的な型はないんだと思っている
https://mstdn.maud.io/@karno/109953444524320783
＿人人人人人人人人人人＿
＞ Universal Domain ＜
￣ＹＹＹＹＹＹＹＹＹＹ￣
このアカウントは、notestockで公開設定になっていません。
型があっても、そいつが静的解析として機能してなければただのゴミ (言葉を選べ) だし、まともな静的解析があれば型なんていらない
Ruby で一番辛いの、型がないことよりも、scope check とか nil-able check がないことだしな
file のパースエラーが、NPE でクラッシュとして現れるのを見てると、結局大事なのは型じゃないんですよとなるわけ
他人をレビューするという行為、自分にある程度肯定感がないとできない
