Home | Notifications | New Note | Local | Federated | Search | Logout
きゅーけー@tojoqk@mastodon.tojo.tokyo
Lisp と自由ソフトウェアと行動分析学が好きです。
自分専用のマストドンサーバーを運用しています。
Typed Racket や Coalton のような型のついている Lisp や、定理支援系の Agda、GNU Guix System に興味があります。
いまは Agda 学習がメインです。
生活リズムの安定のため、深夜 02:00 から 10:00 までの間はアカウントロックをかけています。その間は何も反応しません。
個人サイト: https://www.tojo.tokyo
サブアカウント: https://fedibird.com/@tojoqk
Joined: 2025-12-01 20:07:27
190 notes, 1 following, 1 followers
きゅーけー@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 で文芸的プログラミングできるようになったのが大きい
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-03-30 08:48:00)
なんか、Agdaで日付ライブラリを作ることに熱中しすぎて全てが二の次になっていたので直したいところ。。。とりあえずだいぶ完成しており、今後はこれを紹介する記事を書いていく漢字になる
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-02-23 11:24:43)
あとは紹介記事を書くくらいだけど結構力尽きた感あるな。数週間くらいずっと日付のこと考えてたから一旦離れたい気がする
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-02-23 10:35:52)
グレゴリオ歴の日付を形式的に扱うためのAgdaのライブラリの開発が一区切りついたのでGitHubに公開した。
型で閏年から月ごとに日数の違い、そして日付の隣接関係を扱えているのですごい。
コンパイルした時点で日付のバグ発生しないといえるように設計できた。
とくに Day 型の構造がうまくできていて、「月末」を型として完全に表現できるようになっている。
https://github.com/tojoqk/gregorianum/tree/main
---Attachments---
image: https://mastodon.tojo.tokyo/system/media_attachments/files/116/117/358/014/620/043/original/efd6233ef1c1f79b.png
image: https://mastodon.tojo.tokyo/system/media_attachments/files/116/117/358/019/064/779/original/16c43c11c4c1ff83.png
image: https://mastodon.tojo.tokyo/system/media_attachments/files/116/117/358/020/537/171/original/fdf250f4e05ee9be.png
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-16 01:51:33)
すでによく本質が理解されているものを再利用するときに高階帰納型はものすごく価値を発揮しそうな感じがする。
自分でうまく定義できる気は正直まったくしない。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-16 00:37:50)
制約が重くなっていくと、目的に対して制約のかけかたが正しい限りは全てがうまくいくけど、正しくできていないと何もかもうまく行かないという印象があるからなあ。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-16 00:34:37)
高階帰納型すごいかもしれない。。。すごい異次元の表現力を見た気がする。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 20:49:44)
PLFAにでてくる Bin の正規化された構造が自然数と同型な構造のいい具体例なのでちょうどいい。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 20:48:01)
Agdaの取り組みに戻れるのが最大の回復といっていい。PLFAの1章をCubical Agdaでやってみようと思っていたところで体調不良で倒れていたので、これをやってみる。
本当は1labをしっかり学習した方がいいような気がするけど、なんというか私は暇なので色々勝手に試行錯誤した方が身につきそうでかつ楽しいので。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 20:38:08)
結構な日数の日記の穴があいたけど、普段の日記の網羅度が高いため、日記が書かれていないという事実がある意味記録になる。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 20:35:15)
重い体調不良によって、しばらくの間パソコンを開いてタイピングすることすら困難な状態だったのが、今日仕事をしたことでパソコンタイピングに対する壁が無事に消失した
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 12:59:32)
生まれて初めてマクドナルドで野菜ジュース頼んだかも
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 08:44:31)
寒すぎ。。。すごく病み上がりで家を出た選択が誤りだったのではないかと悩ましく思う。引き返して寝たほうがいいのかこれ。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-11 08:41:19)
体温計、ピピピってなったあとに挟み続けているとちゃんとした正確な体温を測れる仕様はちょっと隠し機能すぎる気がする。
Older Notes