Home | Notifications | New Note | Local | Federated | Search | Logout

きゅーけー@tojoqk@mastodon.tojo.tokyo

Lisp と自由ソフトウェアと行動分析学が好きです。
自分専用のマストドンサーバー(Docker on Guix System)を運用しており、このアカウントはそのサーバーで唯一アクティブなアカウントです。

Typed Racket や Coalton のような型のついている Lisp や、定理支援系の Agda、GNU Guix System に興味があります。
いまは Typed Racket での趣味開発がメインです。

個人サイト: https://www.tojo.tokyo
サブアカウント: https://fedibird.com/@tojoqk Joined: 2025-12-01 20:07:27 259 notes, 1 following, 1 followers

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-08-28 20:34:49) 結構考えたけど、もしも将来 Typed Rhombus を実現できるならそれは結構好みかもしれない。たぶんそれには Typed Racket にある Natural 型が実現されているはずでそういった面は差別化要素になりうるな

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-08-28 09:06:48) Typed Racketの自作ライブラリgraph-executorの真の使い方に気づいて、README.mdに載せている例を作り直した。
Rhombus のよさとしては見た目というものがあるので、ある意味 Rhombus の価値を大きく引き出すことに成功している気がする。

Racket版: https://github.com/tojoqk/graph-executor
Rhombus版: https://github.com/tojoqk/rhombus-graph-executor

#Racket #Rhombus ---Attachments--- image: https://mastodon.tojo.tokyo/system/media_attachments/files/117/170/209/869/374/207/original/116e5856d6397659.png
image: https://mastodon.tojo.tokyo/system/media_attachments/files/117/170/213/358/145/189/original/4f7dafe80c508d80.png

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-08-27 21:40:26) ヤバいかも、一回 Rhombus の機能をウォークスルーしたことによって、素の Racket の記述スキルが明らかに上がった感じがする…。Rhombusと同じことをしたいと感じるのだけど、普通にそもそもRacketでもできる(やってないだけ)みたいなことがある。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-07-17 21:53:08) 予測の通知でありすごい傾きの何かがあると思っていそいで犯人のリソースを止めなきゃ!って思ったわけなので冷静に考えると合理的な反応だったわ。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-07-17 21:01:37) 一定を超えるともはや「膨大な金額」とかしか思えなくなるのでそれがリアルにいくらなのかとか意識できなくなるんだな

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-07-17 20:49:45) AWSへの謝罪文を書いて送るしかないのかみたいなことを思いながらコストエクスプローラ的なのを開いていた

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-07-17 20:48:07) だいぶ取り乱した。フェルミ推定力が足りなかった感。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-07-17 20:39:27) ほんとびっくりした ---Attachments--- image: https://mastodon.tojo.tokyo/system/media_attachments/files/116/935/120/944/502/853/original/9b834f146ca908ad.png

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-07-17 20:37:21) C言語で領域外参照しちゃったときみたいな数値

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-07-17 20:35:34) 定理証明して絶対にバグらないようにしてくれ…

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-07-17 20:25:15) しっかりとご丁寧にメール通知までしてきおって…

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-07-17 20:22:22) クラウド破産したかと思った…。冷静に考えたら金額的に明らかにバクだわ…
https://www.itmedia.co.jp/news/spv/2607/17/news112.html

Reply to @tojoqk@mastodon.tojo.tokyo きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-07-15 22:31:33) おもちゃのLisp実装するのは簡単だけど、実用に耐えうるLispを書くのは簡単ではなく、おもちゃLispに相当するインタプリタを実装して本番環境にデプロイされてしまう状況は少なくないように思う。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-07-15 21:58:16) グリーンスパンの第10法則、いままでLispジョークだと思ってたけど、言語処理系の素人であるアプリケーション開発者が下手くそな劣化インタプリタをなんども至るところで再発明してしまうという深刻な問題についていっているのだと理解した。

https://ja.wikipedia.org/wiki/%E3%82%B0%E3%83%AA%E3%83%BC%E3%83%B3%E3%82%B9%E3%83%91%E3%83%B3%E3%81%AE%E7%AC%AC10%E6%B3%95%E5%89%87

きゅーけー@tojoqk@mastodon.tojo.tokyo boosted: @eniehack@mstdn.sublimer.me (2026-07-04 23:35:00) 自由を失ったandroidに意味はあるんか?という気持ちがある

きゅーけー@tojoqk@mastodon.tojo.tokyo boosted: @eniehack@mstdn.sublimer.me (2026-07-04 23:33:54) Androidアプリを開発するにあたって基本的にgoogleの許可が必要になるのって、今年9月なのマジか
すぐじゃんね……
https://keepandroidopen.org/ja/

Reply to @tojoqk@mastodon.tojo.tokyo きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-06-13 13:25:40) Ollamaが対応してくれる可能性については引き続き期待している

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-06-13 13:23:00) うちの環境で12bのGemma4でMTPがあるのとないのではだいぶ回答速度に差があり、日本語チャットでの体感では最高で2倍くらい速くて、会話が長くなってくるとドラフターの予測が当たらなくなってきて徐々に遅くなるみたいな感じの動きしてる。MTPの有無で段違いだったんで、ROCmがフォークした llama.cpp をコンテナの中でビルドして使うのは大正解だった。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-06-13 10:56:26) Gemma4のMTP対応がOllamaにくるの待てなかったのでllama.cppを rocm が提供しているコンテナでビルドして使ってみたところ速くなった。よかったので新しいバージョンのllama.cppをGuixでビルドするチャレンジしようと思う。これをすればモデル以外はちゃんとビルド再現性がある状態になる。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-06-12 00:28:14) 久しぶりにZコンビネーターを導出するのをやってた。
導出する方法は10年前に学んだ「Scheme手習い」がベースで、何も見ないで繰り返しの抽象化を繰り返して最終的にZコンビネーターを作る感じ。
正確に計測はしてないけど途中結構はまったので、1〜2時間くらいかかった。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-06-10 11:51:19) Guix Systemを使ってるけどGNUとビルド再現性のシナジーの良さと、Guile Schemeが好きというのが使っている自分のメイン理由なので、人におすすめするときは何をいえばいいのかよくわからんな。
やはり、ビルド再現性でバイナリとソースコードの対応について信頼できることかな。
あとはSystemの設定をGuixで記述できてかつロールバック可能とか、Systemdじゃなくて shepherd を採用してて面白いとかそういうのか…

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-06-09 09:16:20) llama.cppで終わったと見られるGemma4のMTP対応がOllamaに取り込まれるのが楽しみすぎて何度も Relases ページにアクセスしてしまう問題が起きているので、 rss 購読することにした。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-06-09 09:12:18) laptop の Cpas Lock の戻りが悪くなったから外付けキーボードを持ちあるくようにしたけど、安定した机がある環境なら問題なさそう。

買ってから2年半経過しており、もう Caps Lock キーの寿命がもう尽きかけていることが判明してしまったため大切に使わねば……

Reply to @tojoqk@mastodon.tojo.tokyo きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-06-08 10:00:32) s/帰宅/二択/ (編集済)

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-06-08 09:55:52) まずいな。laptopのCaps Lock(実質Ctrl)の戻りが悪くなってきた。laptopの買い替えか外部キーボードの持ち運びの帰宅を強いられつつある

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-06-01 22:01:31) 使ったことのあるソフトウェアが過半数いってるな。

きゅーけー@tojoqk@mastodon.tojo.tokyo boosted: @fsf@hostux.social (2026-06-01 21:56:21) The May #GNU Spotlight by Amin Bandali is now available! Read it here: https://u.fsf.org/4b9 #FSF #GnuPG #G-Golf ---Attachments--- image: https://hostux.social/system/media_attachments/files/116/674/958/502/011/770/original/a679fcd452531b12.png

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-31 01:27:46) Podmanシステムの複雑性を理解したかもしれない……。
原因判明してないけど、Podmanが起動しなくなってしまったので、急遽 Podman on Guix System から Docker on Guix System に切り替えた。かなしい。いつかリベンジしたい…

Reply to @tojoqk@mastodon.tojo.tokyo きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-30 02:25:47) RMSの当時の判断が今のGuixにつながっているのはアツい

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-30 02:24:18) GuixをGuileのDSLとして構築するという、Lispの価値を最大化する活用しているのも最高すぎる。また、GexpsでGuix定義の中にGuileスクリプトを綺麗に埋め込めるのも最強。どちらも、Lispでないとできない。
Older Notes