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-05-08 09:15:28)
なんか私が6年前にGuixに寄稿した ddskk のビルド定義、Emacs でよく使われている Melpa とか Straight と比べて品質がいいことが分かった。
SKKは歴史的なソフトウェアなので事前にビルドする必要があるのに Melpa などではビルドしてないから不完全な状態で降りてきてる。
それに対して Guix の ddskk はビルドされた ddskk 環境が構築されている。
Reply to @graywolf@fosstodon.org
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-08 01:55:25)
@graywolf
お知らせいただきありがとうございます。
nonguix のリポジトリをみる度にバージョンアップ対応のコミットをされているのを認識しています。
いまのところは LibreWolf で満足していますが、 Firefox を使いたくなったときに検討しようと思います。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-08 01:11:28)
GNU Guix のリポジトリにFirefoxが入ってなくて困る問題が、LibreWolfのおかげで解決した気がする
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-08 00:51:03)
guix のリポジトリで git log した感じの印象では librewolf の方が圧倒的にメンテナンスされている印象を受ける状態なので、 librewolf を使うことにした。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-08 00:32:28)
いまの GNU IceCat は Firefox Multi-Account Containers がちゃんと動作するのか。。。どっちがいいか分からなくなってきた。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-08 00:14:25)
LibreWolf というブラウザを発見してめちゃくちゃテンションが上がっている。
Firefoxのフォークだと思うのだけど、Firefoxから要らない機能が無効化されていて、必要な設定が最初から設定されている最強のブラウザかもしれない。
https://librewolf.net/
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-08 00:08:25)
久し振りにメインのノートパソコンにGuix Systemを入れて使っている。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-05 09:06:52)
サードパーティのメーラーを簡単に使いたかったので Proton をやめて Fastmail に移行した経緯が実はある。Evolution と K-9 Mail を使いたかったので…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-05 08:54:17)
AIでだれでもコードを読めるし書けるし編集できるんだったら、いままでいわれていた「専門家しかコードを読み書きできないから、自由ソフトウェアの恩恵は一般の人に対しては薄い」という主張はAIが進歩すればするほど弱くなる。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-05 08:52:08)
AIが進化したことで、自由ソフトウェアの安全性をAIにある程度確認させることができるようになったわけだから、いままでも自由ソフトウェアがより安全になっているのでは？
そもそも、専門知識を持たない人でもある程度ソースコードをAIを使って解釈・編集できるようになることは、自由ソフトウェアの普及においてかなりプラスな側面があるということにいま気づいた。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-05 08:42:05)
Fastmailが、 KeepAndroidOpen を応援しているのは相当に印象がよい。やはり Fastmail を選んでよかったと心から思える展開となっている。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-05 08:39:13)
Mastodon のPWA、5系のUI使いやすいかも。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-05 08:38:15)
AndroidでF-Droidが事実上の締め出しをくらいそうなのだいぶやばい。
F-Droid, home to thousands of free and open-source Android apps, calls Google's developer verification an "existential threat." An estimated 85% of F-Droid apps could face distribution issues because their developers signed through F-Droid, not through Google. @keepandroidopen #KeepAndroidOpen https://keepandroidopen.org
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-03 19:43:08)
グレゴリオ暦の自作ライブラリ、とりあえず自分がほしいの過去記録についてはざっくり DateHour まででいいでしょって思っていたけど、未来の予定をたてるのにもちょっと使いたくなってきて、分まで表現する DateTime を実装する予定が少しある状態になっている。
世の中的には DateTime と命名したら秒とミリ秒までないとダメでしょと思われかねないけどそこは気にせずに好きにやっていこうと思う…
https://github.com/tojoqk/gregorianum/tree/main
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-03 19:27:55)
あんま最近Mastodoonしていなかった故にモチベーション低めなためやってなかった Mastodon のバージョンアップ対応が無事完了したはず。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-02 11:52:13)
短い期間で復旧する前提で書いてたけど、長期化するようなら話変わってきそう
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-01 22:21:07)
家計簿をAgdaでつけるところまで今年中にはいきたいかもしれない。
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@zetamatta@misskey.flowers (2026-05-01 22:14:39)
家計簿アプリは… GNU Cash !
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-01 22:11:54)
マネフォの件、初見の印象としてはBtoB、BtoCともに信頼を失って倒産までいってもおかしくないと思ったが、世の中のITリテラシーの低さを考慮にいれると大して問題なさそうと判定されてシステム再開で労われ、そのまま何事もなかったことになりそう。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-23 20:55:26)
(通知いくけどもったいないので編集して直した)
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-23 20:53:28)
s/優先されいてる/優先されている/
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-23 20:37:20)
プログラミング言語が関数型言語かどうかを見分ける方法について思いついた。
1. 再帰関数を定義できること
2. データの並びを表現するデータ構造として、配列よりも単方向連結リストが優先されいてること
この1, 2を満たしているプログラミング言語が関数型言語であると認識すれば間違いがないように思う。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-23 00:36:13)
Agdaの標準ライブラリにあるの同型の定義を使った。すばらしい。
https://github.com/tojoqk/gregorianum/commit/4beaa459cc1a27fce4982ca15e2b46efcf486454
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-22 23:49:38)
ほしいのこっちっぽいな。。。
_↔_ : Set a → Set b → Set _
A ↔ B = Inverse (≡.setoid A) (≡.setoid B)
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-22 23:45:20)
ようやく欲しい物をみつけた。Function.Bundles にあったのか。。。
_⤖_ : Set a → Set b → Set _
A ⤖ B = Bijection (≡.setoid A) (≡.setoid B)
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-22 21:44:47)
TypeScript の as const で定義して定数配列から Union 型を作るやつ、あれと同じこと Agda でやりたいけどやり方わからないなあ〜とずっと思っていたけど完全に解決した。
そもそも要素の重複のない長さnの配列というものは Fin n と同型であり、Agda でそれを実現するには Fin n で定義して、それぞれの要素にドメインに沿った別名をつければいいんだ。。。
そしてこれは既に Gregorianum ライブラリで曜日を定義するにあたってやってた。今後列挙する機会のあるユニオン型を定義したいときは最初から Fin n を使って定義しようと思う。
https://github.com/tojoqk/gregorianum/blob/main/src/Gregorianum/Date/Weekday.agda
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-20 21:37:47)
JVMってようするにLispのランタイムじゃんってことについて今日初めて知った。仕事でAIにKotlinについていろいろ聞いていたらなんかJVMでJITがどうとかいいだしてそこから芋づる式に本質的にJVMがLisp環境と同じであり、すべての型を強化したJVM言語達がAltJSと状況的に大差ないことまで分かった。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-13 20:26:34)
org-roam と lagda.org で自分のデータを整合的に管理するのがいま一番やりたいことであって、Gregorianumについて解説する記事は一番やりたいことではない…。いたしかたなし。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-04-13 20:14:25)
Agda で開発していた日付ライブラリの Gregorianum、一旦ここで開発を完了していいかと思い始めた。
https://github.com/tojoqk/gregorianum
今後は本来の目的である、org-mode 上で Agda のコードを文芸的に記述し、睡眠記録の入力を Agda のコンストラクタの追加で実現するという目的の実現へと移ろう。そのために、時刻を扱う必要があるけどそこはそんなに一般的な感じにならないからライブラリにはしないでいいやっていう感じ。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-03-30 08:49:36)
あと、.lagda.org で文芸的プログラミングできるようになったのが大きい
Older Notes