データ容量と処理能力的にそもそもちゃんとした回答得られるbot作るの厳しそうかな
データ容量と処理能力的にそもそもちゃんとした回答得られるbot作るの厳しそうかな
GPTs って規約的に論文たくさん突っ込んで最強bot作っていい感じなんかな？ (調べるのが面倒)
これ完全なのは無理として、いい感じに決定可能なアルゴリズミックタイピング作れるかな？
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 か、すごいな
［速報］GitHub、組織のコードやドキュメントを学習しカスタマイズやファインチューニングが可能な「Copilot Enterprise」発表。GitHub Universe 2023 － Publickey
https://www.publickey1.jp/blog/23/githubcopilot_enterprisegithub_universe_2023.html
ポケモンのプロバトラー、バトルも育成も楽しむやべー奴らなのかなと思ってたが、普通に違ったんだ
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 は今もこの構成なんかな？
Fedibirdの現在の構成図です。
基本的な構成と比較していきます。
マシンの台数を増やしています。同じ構成のサーバを2台置いて、負荷の分散・処理能力の増強、片方が落ちてもサービスが停止しないように構成しています。
データベース（PostgreSQLとRedis）は、2台が同じものを参照する必要があるので、別のマシンに分けて実行しています。
Storageは、ローカルファイルシステムだと両方のマシンから読み書きできないので、外部のオブジェクトストレージ（Amazon S3）に変更しています。
Sidekiqは、キュー毎にプロセスを分離しています。
PostgreSQLへ同時接続するプロセスがどんどん増えていくので、pgbouncerを経由して接続することで、PostgreSQL側の接続数を一定以内に制限し、接続を再利用することで効率化しています。
2台の手前にHAProxyを置いて、外部からは一つのサーバに見えるようにして、2台のサーバに接続を分散させます。
全文検索用にElasticsearchを追加しています。
あとは、二重化したりバックアップする機構です。
Mastodonの基本的な構成図です。
Mastodonをシンプルに構成すると、図のような構成になります。
一番手前にNginxを置いて、バックエンド側の、WebUIとAPI（Puma）、ストリーミング（Node）、メディアファイル（Storage）へのアクセスを中継します。
データベース（PostgreSQL）へ、Puma、Node、Sidekiqがそれぞれ接続します。
もう一つのデータベース（Redis）へ、Puma、Node、Sidekiqがそれぞれ接続します。
ローカルファイルシステム（Storage）へは、Puma、Sidekiqが読み書きを行い、Nginxが読み出してユーザーのリクエストに応えます。
PumaとSidekiqは、インストールしたrubyの環境で実行されます。
Nodeは、node.js v12〜の環境で実行されます。
Pumaは、ユーザーのブラウザに初期値とJavaScriptのコード（WebUI）を渡して、それ以降はAPI経由でやりとりします。
この他、ImageMagickやFFmpegがメディアの変換に使われています。
このアカウントは、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()0 の言語と 1 の言語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 がさらに混乱を極めてる
の投稿
dev@post.naskya.net
このアカウントは、notestockで公開設定になっていません。
Fediverse Advent Calendar 参加することにした (12/7)
https://adventar.org/calendars/8812
