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
92 notes, 1 following, 1 followers
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-13 13:02:43)
AIにさっきのコードを投げると、{} が特別な場合だから起きるんだ！普通は起きないんだ！変なことしなければTypeScriptは普通は大丈夫なんだ！とうるさいので記事のコード例を少し変えた。
```
const convert = <T, S>(value: T, witness: S): S => {
const obj1 = { a: witness, b: null } satisfies { a: S, b: null };
const obj2 = { a: value, b: null } satisfies { a: T, b: null };
const f = (x: { a: T, b: null }): { b: null } => x;
const obj = { ...obj1, ...f(obj2) } satisfies { a: S };
return obj.a;
};
```
https://qiita.com/tojoqk/items/1e37896757f847c97948
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-13 11:23:50)
TypeScriptはas, !, is, anyをすべて避けたうえで安全性を高めるすべての tsconfig を書いた上であらゆるリンターを有効にした上で危険
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-13 00:58:26)
TypeScriptに対していままで過度な期待をしていたことがよくわかったのでそれは本当によかった。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-13 00:48:52)
12月中に定理証明の記事を投稿することを目指して執筆しているというのに、貴重な時間をしょうもな矛盾の存在証明に使ってしまった。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-13 00:22:50)
TypeScript、一見安全そうにみえる7行のコードで任意の型(neverを除く)になりすませるというこの現実。
```
const convert = <T, S>(value: T, witness: S): S => {
const obj1 = { a: witness } satisfies { a: S };
const obj2 = { a: value } satisfies { a: T };
const empty = (): {} => obj2;
const obj = { ...obj1, ...empty() } satisfies { a: S };
return obj.a;
};
```
https://qiita.com/tojoqk/items/1e37896757f847c97948
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-13 00:01:56)
今日TypeScriptに感じた激しい怒りを怒りのままにするのではなくて、冷静な記事にして公開したとで収まった感じがする。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-12 23:42:52)
QIitaにTypeScriptの記事を投稿しました。
TypeScriptはあんまり自分のサイトにはなんとなく書きたくないからQiitaに書いた。
https://qiita.com/tojoqk/items/1e37896757f847c97948
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-05 01:07:04)
これでロック解除が超快適じゃん。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-05 01:06:44)
Fedoraでいまふと思って指紋のやつ使えるかなあって思って試したらできた！えー、指紋認証できるのか、これは超びっくり！
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-03 21:57:40)
ACL2がいろんなヒューリスティックを駆使して自動で定理証明するのはまさに実用Common Lispに書いてあるヒューリスティックな探索の話に通じるように思う。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-03 21:55:32)
PAIPの日本語訳の実用Common Lispをペラペラと呼んでいた結果、いま自分がACL2を使って定理証明をしているのはかつてのAI研究の成果を享受しているのだということがわかった。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-03 21:23:17)
@masso
総称関数の特異点だから特異メソッドと呼んでいたところを、メソッドを関数ではなくメッセージだと考えているシステムに同じ名前のまま別の解釈によって導入した結果なんですね。
結果として目的としても機能としても違うものになっているのにもかかわらず関連づけられているのは奇妙な話ですね…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-03 20:58:15)
最近Rubyの特異メソッドという概念をしっかりと把握したのだけど、CLOSのeql specializerとはやりたいことが全然違う機能であることがわかった。CLOSの方は特定のシンボルとか数値に対してディスパッチするのがメイン機能であって、eql と equal で意味が変わるようなものを指定するためのものではないと思う。
特異メソッドはCLOSを参考にしたというのは事実なのだと思うけどなんだかCLOSへの誤解をうむのではないかと感じる。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-02 13:42:57)
Emacs の拡張の magit というやつ使ってる