Firefish 1.0.5-rc とりあえず deb だけは作った。そのうち試す
https://github.com/mizunashi-mana/firefish-dist-pkg/releases/tag/v1.0.5%2Brc-d2023112900-beta

Elasticsearch のリテンションポリシーも作らなきゃな

Firefish 1.0.5-rc とりあえず deb は作るか

圏論学んでるって言ってる人なら米田の補題の直感ぐらい持っとるやろ（？）

たまにそういうことしがちなので、もうちょっと self-contained にいきたいが、他の人たちがどういう requirement 持ってるのか分からないという問題があるんだよなあ

モナドを自己関手によるモノイダル圏のモノイド対象と呼ぶのと同じそう。その直感が持てる知識がある人に、わざわざモナドを教える必要はないんだよなあ（）

米田の補題の直感がある人に、表現の直感は説明しやすいが、問題は表現の直感を持ってない人の中で米田の補題の直感を持ってる人などいないってことだよな（）

ルンバがいないと思ったら、どうやって入ったんだってとこにいた

帰還した

家爆発してたりしないかな

帰宅タイム

今日家に帰れるか決まる

@qwjyh@misskey.qwjyh.net これですかね？
https://github.com/gfngfn/SATySFi/pull/369

ちょっと見てみます、ありがとうございます！

なるほど、現在進行形でエコシステム周りの整備が進んでるのか。これは確かに期待できそうだが、今はまだ開発中って感じなのか

このアカウントは、notestockで公開設定になっていません。

@qwjyh@misskey.qwjyh.net これよく分かってないんですけど、基本裏側 OPAM で、グローバルワイドにしかインストールできないって理解でいいんですよね？ TeX の latexmk & tlmgr ユーザなので、そこまで違いを感じられないという...

毎年 TeXLive のための docker イメージ作ってるの、いい加減やめたい

TeX に関する不満、基本的にエコシステム周り (構文とかはまあ移行する動機を持つほどではないかなという感じ) なので、SATySFi がそこら辺解決してくれるかというとうーんという感じなんだよな

今年のアドベントカレンダーはちょっと閑散としてそう
https://adventar.org/calendars/9214

SATySFiに関すること https://qiita.com/puripuri2100/items/a63e0c48f245dfcb0446 #miteru

SATySFi リトライしてみるか？

TeX から脱却したい

これ謎
https://github.com/mizunashi-mana/mizunashi-work-playbook/issues/22

リテンションポリシー作成タイムじゃん。めんどい

ようやく Elasticsearch の用語を理解してきた

もしかしたら世の中には祝日や土日という概念がない人の方が多いのでは？と思ったりする一日だった

明日週末なんだなあ (曜日感覚なし)

out_es plugin に Trace_Error オプションがあって、これを使えばいいのか。なんかシャード数が足りないって言われてんな。明日詳しく調べるか

16文字でもん？ってなっちゃう。せめて24文字にしてくれ

パスワード文字数上限8文字はちょっと許せないかな

上限値って偉大で、DoS 対策っていうのはまあそうなんだけど、世の中にはいろんな人がいて、やっていい範囲でやべーことを素でしてくる人がいるので、上限値下限値とかはまじでそこまでだったら耐えうるぐらいの値計算して設定しといた方がいいんすよね（）

諦め。とりあえず家帰るまでサイレンスしとこ

分からん。fluent bit のトラブルシューティングむずいな

動くこと、運用できるようにすることを分離するだけで見積もりに対する価値観が揃ってれば、それはそれで価値観揃ってない状態よりは良かったりするんじゃないかな

保守しやすいコードを書くっていうの、結構この先の負債に対するコードがどうのって話になりがちだけど、協業の場合動くことと、これから運用していくことどちらをゴールに置くかで見積もりがだいぶ変わるのでその価値観の違いでの摩擦を小さくするっていうのも結構比重として高い気がする

Elasticsearch bulk API が payload なしで 200 OK 返してくるんすか？なぜに？

fluent-bit の id が連番に振られて、どの ID がどのログのものなのか分からない問題って、どう解決すればいいんだろう？

タイムゾーンはチェック済みとする

未来の日付のログが出てる時の原因 [検索]

それはそうとめっちゃ自鯖でアラート鳴ってるので対応しないと

ただもうちょっと焼いてもらっても良かったかもな

初さわやか食べたけど、めっちゃ美味しかった

ちょっと余裕があるスケジュールになった

@elpinal@mstdn.cbult.space そこは実装をコードで書いてます。簡単な説明は https://mizunashi-mana.github.io/blog/posts/2023/09/archived-activitypub-server/#archivedon にありますが、旧サーバの URL と content type から新しい URL のマップファイルを作って、それを参照するみたいな感じで結構ゴリ押ししてますね

具体的な実装箇所は https://github.com/mizunashi-mana/archivedon/blob/d38793a1d86a79a5a86b9394b580df0f4fd2c172/src/server/handler/redirect_map.rs になります

明日は休みの人が多いらしい

労働基準法って偉大や

労働ってまだ時間のゆとり持てたんだなって感じになってる

dependent types の型チェックはまあ普通に組めば良さそうなので、普通に組むか。結局タプルを扱う部分どうするかが地味にめんどいのかな

標識の意味がちゃんと分かるようになってちょっと楽しい

エヴァンスの DDD 本めっちゃいい本だと思うんだけど、内容としてはあんまり実践向きではないな感はあるけどこの感覚は正しいんかな? エヴァンスの本に書いてない戦略部分がいちばん大事そうだし、それを度々エヴァンス自身が強調してるのが、この本の好きなとこだな

DDD の巷にある記事とかスライド、エヴァンスの本ちゃんと共感して読んでたら絶対そういう内容にならんやろみたいな印象あるんだけど、やっぱこれはそう感じてる人そこそこいるんだな。安心した。ここまで多いと読み方か経験間違ってるのかって思うよな

Microsoft に伝えずにやってるの、ほんまかって感じやし、その後 Microsoft から圧力かけられそうなのもほんまかって感じやな...

そ、そっか... | OpenAIのCEO解任にMicrosoft CEOが激怒、取締役会は既にAltman氏の復帰を打診中とも
https://texal.jp/2023/11/19/microsoft-ceo-furious-at-openai-ceo-dismissal-board-of-directors-already-in-talks-to-reinstate-altman/

生活リズムというものに目覚めたため、寝すぎるのは良くないという感覚が分かるようになった

ルンバ、そろそろレンタルに切り替えるか

寒いかもしれない

cursor.sh、あんまり魅力が分からんかったんだけど、VSCode で Copilot / Copilot Chat 使ったり、GPT plugin 使うのと比べてどこら辺が良いん？

Yubikey、高価なデジタル認証用の鍵って感じなので、スペア作って持っておいた方が良いというのは物理鍵と同じなんだなって感じ

ホワイトボードがない環境に来てしまったのが辛いな

やっぱり内部的には依存積と関数型分けといた方がいいかな？

@elpinal@mstdn.cbult.space ありがとうございます！

中々推論難しい感じになりそうだな。まあ普通に単純な関数型じゃなくて、依存積込みにすればいいんだけど。だから #-> は演算子じゃなくて (...) #-> ... でセットにして扱わなきゃいけないんだな

雑に (^a: Type, fx: F(a), gx: G(a)) #-> a を、雑に argument 部分と return 部分でコンテキスト別々に扱ってたが、依存積部分のパラメータは return 部分まで scope を持つのか

依存積の依存パラメータが外に出る場合があるのか。これ単なる関数型だと無理か

気づいたが、雑に組んだ型システム、sound じゃねえな

f(^a: Type, fx: F(a), gx: G(a)): F(a) = fx

依存積の型推論の組み方って、いい文献あるんかな？

土日休みという習慣がない世界に来てしまってるので、週末という感覚が全然ない

世間では明日から週末らしい

ActivityPub、実はブログとか記事発信用で、それを短文 SNS として使ってる僕らがおかしいのではないかと思うことが時々あるな

何も確かなものがねえ。これほんとに sound なんか？

雰囲気で型システム作って、雰囲気で健全そうな双方向型システム作って、雰囲気でアルゴリズム化をやってる

@zundan@mastodon.zunda.ninja 10/23 時点では 9% ぐらいは 2.1 対応してましたね (2.1 の方が取れる情報は多い)。その内どれぐらいが 2.0 に対応してないかは見てないですが
https://github.com/mizunashi-mana/fediverse-stats/blob/main/notebook/fediverse-stats.ipynb

消灯なので寝よ

misskey.io はちゃんとお知らせで更新内容出してくれるのが偉いよね。あれは信用できるところだなと思う

ま、こういう法規制自体は大事なんだけど (世の中には悪い人や余裕ない事業者がたくさんいるので)、お陰で事業のハードルが上がりすぎるのはどうかとは思うよな

DM の保存は正当業務行為として認められると思うが、閲覧は一般的に正当業務行為として認められるかは微妙

@lithium03@mastodon.lithium03.info まあそれも一つありだと思いますね。結局ユーザにどれくらい説明されていて、ちゃんと同意が取れてるかが通信の秘密の例外規則においては (というか一般的な事業法では) 重要なので、そういう説明を足していきつつモデレート機能拡充していくのも一つの手ではありますね

@lithium03@mastodon.lithium03.info 一応補足で大体イメージはしていただけたんじゃないかと思いますが、現状の総務省の行政処分上あくまでユーザ側から見た時のサービス判断になることが多いので、ユーザリテラシーとしてどうなのかという反論は通用しない場合が多いです (ちゃんとそこを補填するための事業活動をしてない場合は特に)

@lithium03@mastodon.lithium03.info なので、例えばユーザ側から DM に対しての通信の秘密侵害の問題提起が行政にあった場合にどうかが焦点なので、そこにサービス側がそう思ってなかったが通用するかどうかだと思いますが、現状のコミュニティ的にはそこは通用しないんじゃないかという感じですね (技術的な立場がどうというのはあまり関係がない)

@lithium03@mastodon.lithium03.info うーんとこの場合紳士協定化を決めるのはサービス側ではなくユーザ側なので、ユーザ側が Misskey の DM という名の機能に DM としての機能を期待していて、それを Misskey コミュニティが一般的に認識している、つまりサービス側がそれを認知してる場合は、行政に対して言い訳はできないはずですね

なんか雑に例のイシューを追った感じ、ローカルユーザなら大丈夫みたいな議論をしていて不穏だな。とりあえず、電気通信事業での通信の秘密を守る必要があるコンテンツにはローカルユーザ同士の DM も含まれるはず

@lithium03@mastodon.lithium03.info Misskey というサーバで見た場合に、ローカルユーザ同士でのダイレクトメッセージが電気通信事業届出の条件に当たるはずですね。そこに AP は関係ないはず

僕も misskey.io に避難垢はあるので、他人事ではないけど、クリティカルではないからあんまり積極的に参入する気が起きないな。いい感じになってくれ（）

海外よく知らないんだけど、通信の秘密は日本独自の仕組みなんだっけ？

ま、必要性は分かるし、その一番簡単な解決手段が全閲覧というのも分かるな。僕は多分そういう機能載ってもブロックしないし (無条件に内容全公開されるとかだと流石にブロックするが...)

ま、とりあえず Misskey としてどう向かうかは分からんし、僕は Misskey のことよく知らないので一般論しか言えないけど、misskey.io に限った話で言えば、全閲覧機能載せて消費者センターとかに話が行くと総務省から行政調査が入る可能性は十分にある (多分今まで実例はない。電気通信業者法での別件でかなり悪質な奴については何度か行政処分は下ってるけど)。通報受けたやつだけ閲覧はちょっと分からないけど、そういう枠組みでやってるとこはある

で、一般的に正当業務行為で説明するのは難しいので、利用規約で明示的に書いて同意踏むか、「緊急避難」または「違法性脱却事由」の方に持ってくことになるが、この場合該当投稿だけ審査かける仕組みにしないと違法性があるということになる (日本ではの話だけど)

まず責任逃れのため、正確な詳細は日本政府発行のガイドライン及び専門家に確認してくれと前置きはしておくけど、

通報システムは一般的にはこの「緊急避難」または「違法性脱却事由」、「正当業務行為」に該当する枠組みで作るはず

RE: https://ff.mizunashi.work/notes/9m3cpqf1kyej4qaa

ということらしい。個人名義申請なんかな？

@morikapu@otadon.com なるほど、そういうのがあるんですね。ありがとうございます！

とりあえず、電気通信事業者向けのガイドはこれ
https://www.soumu.go.jp/main_content/000739290.pdf

で、通信の秘密に関する該当部分は p.46 の

電気通信事業者等（第三号事業を営む者を含む。）は、その取扱中に係る通信の秘密を侵してはならない。通信の秘密に該当する事項については、通信当事者の同意がある場合、裁判官の発付した令状に従う場合、正当業務行為に該当する場合又は正当防衛若しくは緊急避難に該当する場合等、違法性阻却事由がある場合を除き、取得、保存、利用及び第三者提供が許されていない。

https://www.soumu.go.jp/johotsusintokei/field/tsuushin04_01.html には misskey.io はいない気がする？

https://www.soumu.go.jp/main_content/000799137.pdf を見る感じは misskey.io は届出が必要な事業には該当しそうだが

misskey.io って流石に電気通信事業の届出は日本政府に出してるんだよね？広告あるし、多分条件には該当する？ (misskey.io をよく知らない)

まあ、DM に限っては AP じゃなく E2E の別システム搭載して、UI だけ統一というのは理想としては賛成ではあるが、今それを言ってもしゃーないし、開発側・運用側の負担が大きすぎるんだよな

日本、間違いなく違憲とされる法律が多すぎて... (これで立憲国家名乗ってるの、ほんまかという感じ)

電気通信事業者の通報制度などによる検問システムは、現法律上は違法でない仕組みが作れるはずだが、違憲かどうかについては、自衛隊の憲法9条問題と同じくらいには未知数みたいな話だった気がするな

もしかしたら僕って人間だったかもしれない

生活リズムというものを感じている

完全敗北だ...

ダメだ、IPv6 化諦めて、IPv4 の世界に戻ろう...

Oh... Caddy 2.7.5 には acme_server が動作しなくなるバグがあるんか。修正済みなので次リリースで治るっぽい
https://github.com/caddyserver/caddy/issues/5911

今日のどこかで

Debian 12.2 へのアップグレードのため、しばらく鯖落とします

データ容量と処理能力的にそもそもちゃんとした回答得られるbot作るの厳しそうかな

GPTs って規約的に論文たくさん突っ込んで最強bot作っていい感じなんかな？ (調べるのが面倒)

type1 ~ type2 がどうなるか次第か

これ完全なのは無理として、いい感じに決定可能なアルゴリズミックタイピング作れるかな？

Haskell 的なレイアウトルール、頑張って再現しなくても、前処理だけで入れれるレイアウトルールぐらいで十分じゃねってなっちゃった

GPT、はよいい感じに declarative type system 与えたら、complete じゃなくていいので annotation つけたら sound にはなる bidirectional type system 作って

CLTT と比べると SGL って、丁寧だしちゃんと常識も書いてくれてたんだなってなっちゃうね

単純に圏論が面白いという話なら共感できるんだが。圏論、特にプログラミングへの理解の助けにはならんが、面白いし、みんな categorical logic 話せるようになって、set theoretic logic 撲滅していこうな
(なお、Categorical Logic and Type Theory 挫折したマンです)

個人的に圏論がプログラミング理解の助けになるという論に乗せられて、圏論学んだ結果得られたこと、特に助けにならないだしな

universality based な equational reasoning model は最適化屋には便利なことがあるし、その方面での理解や手法解析には役立つことがあるけど、あくまでそういうモデルが現実との乖離をなるべく抑えて作れればだしな

Applicative、Monad、Arrow とかは Moggi 先生-like な categorical semantics インタプリタが便利なだけ感があるし、そこって別に圏論だけ学んでも特に理解できないよな感あるし

長年疑問なんだけど、Haskell とか Scala 界隈にたまにいる、圏論を学ぶことがプログラミングに役に立つ論主張してる人って、どういう成功体験からそういう主張してるのかいまだに分からない

1ユーザ辺り月額 $39 か、すごいな

なかなかにアレな言語ができつつある

良い曲ばかりでプレイリストを作ると止めどきを見失う

ポケモンのプロバトラー、バトルも育成も楽しむやべー奴らなのかなと思ってたが、普通に違ったんだ
https://www.gamespark.jp/article/2023/11/10/135837.html

Copilot というか GPT、下手に補完してくれるので、要望 -> GPT 提案が普通に通ってしまい、別に GPT 提案させる前に設計を挟み込む必要がなくなりそうという。そこに人間による設計が先というのは、後の顛末を分かってる人だけで、後の顛末を知らない人にとっては別に必要性がないんだよなあ

普通に Copilot が単純コード生成やってくれるのは便利だし、Copilot Chat が設計レビューとかコードの読み方教えてくれるのも便利で、他のプロダクトも未来があるけど、じゃあプログラマ不要論とかよりプログラマの仕事がより上流作業になりそうかというと Copilot 使ってる限りはそういう未来が見えないんだよなあ

コード書けないやつが設計して AI が書き散らしコードを後から仕様変えずに整理していくのがプログラマの役割になるの、完全に悪夢だがそうなりそうなのは危機感がちょっとあるよな。逆になってくれ、頼む

多分 Copilot でコード書けば書くほど、創造的な作業がしにくくなってくんだよなあ（）

Copilot、基本的にはコピペを簡単にする機能なので、今まで以上に保守管理コストがやべーコードが量産されてくって感覚はまあ分かる

はい、アライズは良いです

このアカウントは、notestockで公開設定になっていません。

Bluesky の Web UI、めちゃくちゃ初回ロード時間かかるようになってない？

Mastodon は今も基本構成はこれなはずだが、Fedibird は今もこの構成なんかな？

このアカウントは、notestockで公開設定になっていません。

そういや、Scala は

val x = x + 1

更新系と束縛系が多く、方程式の解と読む言語は割と少ない印象だな。Haskell、Prolog 辺りがそう？ (どちらも解釈はもうちょっと特殊だが)

= が代入とは限らないのもあれ。 x = x + 1 というのは旧環境での x + 1 の結果を x に束縛し直してると読む言語もあれば、 x = x + 1 の方程式の解と読む言語もあれば、変数 x の値を x + 1 に更新すると読む言語もある

x = 0
f = () => { println(x) }
x = x + 1
f()

nowplaying テスト | Criss Cross
Artist: 中河健
Album: イリスのアトリエ グランファンタズム オリジナルサウンドトラック - 2
https://music.apple.com/jp/album/criss-cross/974588726?i=974589483
#nowplaying

Threads は AP 連合以外にやりたいこと・やるべきことが多そう

これすき

このアカウントは、notestockで公開設定になっていません。

そうか、Firefish の UI から見ると、4ヶ月前の投稿って割と自明なんだけど、Mastodon の UI だとめっちゃわかりにくいのか

Threads 連合間近かという投稿に対して、リリース当初から Threads は AP 連合詐欺だったよということを示すため、Threads のリリース直前の投稿がブーストされてるが、それが直近投稿と間違えられ Threads 連合間近みたいに誤解され、TL がさらに混乱を極めてる

Sonoma アップグレードチャレンジ

このアカウントは、notestockで公開設定になっていません。

Fediverse Advent Calendar 参加することにした (12/7)
https://adventar.org/calendars/8812

今 Firefish 一番見てるけど、この鯖が一年後にも稼働してる保証がないのが悩みどころだよな。連絡手段としてはもうちょっと安定性高いサービス併用したいところだな

Firefish から Fediverse 参加してますって言うのに、めちゃくちゃ知識を求めなきゃいけないの、どうすればいいんだろう

Fediverse、やっぱり簡単に説明しづらいのがダメ

第三までできてるのか、すご

Pixel、思ったより重かった