寒いかもしれない

cursor.sh、あんまり魅力が分からんかったんだけど、VSCode で Copilot / Copilot Chat 使ったり、GPT plugin 使うのと比べてどこら辺が良いん？

Yubikey、高価なデジタル認証用の鍵って感じなので、スペア作って持っておいた方が良いというのは物理鍵と同じなんだなって感じ

ホワイトボードがない環境に来てしまったのが辛いな

やっぱり内部的には依存積と関数型分けといた方がいいかな？

@elpinal@mstdn.cbult.space ありがとうございます！

中々推論難しい感じになりそうだな。まあ普通に単純な関数型じゃなくて、依存積込みにすればいいんだけど。だから #-> は演算子じゃなくて (...) #-> ... でセットにして扱わなきゃいけないんだな

雑に (^a: Type, fx: F(a), gx: G(a)) #-> a を、雑に argument 部分と return 部分でコンテキスト別々に扱ってたが、依存積部分のパラメータは return 部分まで scope を持つのか

依存積の依存パラメータが外に出る場合があるのか。これ単なる関数型だと無理か

気づいたが、雑に組んだ型システム、sound じゃねえな

f(^a: Type, fx: F(a), gx: G(a)): F(a) = fx

依存積の型推論の組み方って、いい文献あるんかな？