2023-09-10
昨日は大会運営の準備で一日外にいた。楽しいので後悔はないのだけど、だいぶ疲れて今日の夕方になったのにまだ疲れてぐたっとしている。
僕は疲れに気が付きにくいようで、周りが疲れたと言っていたり、翌日ダメージが残るよう場合でも、そのときは特に気が付かない。パフォーマンスには影響していると思うのだけど、気持ちは疲れていないので実際どれくらい疲れているかはわからない。酔っているとか深夜テンションとかみたいな感じに普段からなってしまうのだろう。
疲れや体調不良に鈍感なのは、子供の頃からずっと変わらない気がする。やる気が出ないのと体調が悪いのの区別はずっとつかない。一度インフルエンザにかかったとき、病院にかかったりする前に塾に行きたくなさすぎて、だるいと言って仮病を使ったら仮病じゃなかったことがある。その他にもなんか調子が出ないと思ったら花粉がすごい飛んでいた、みたいなことはよくある。
こういうことを書くと、やる気が出ないときは体調不良を疑おう、みたいな学びを得たくなるのだけど、単にめんどくさくてやる気が出ないことの方が僕は多いので、そんな甘えた学びを得てしまうと色々立ち行かなくなる（経験済み）。
今のところの付き合い方は以下の通り。
- 原因が明らかにわかっているだるさがあるときは、自分を甘やかすことにして、
- よくわからんけどだるいときは、寝る、走る、食べる、手を動かすを試してみる。
- 大抵は手を動かすと動き出すのだが、それでもダメなら人と喋ったり病院いくのが良いだろう
今日は疲れているのにVSCodeで使うフォントをノートパソコンにインストールした。とても偉い。これでターミナルの一部でレイアウトが壊れていたのが直った。やったーー。
5月くらいに秋吉台に行ってロゲインしたときに買ったちんぐを飲んでいる。ちんぐは麦焼酎で、黒麹を使っているのが特徴。
ちんぐは親友という意味らしいのだが、あのとき一緒に行った友達とはしばらく会っていない。元気だろうか。
SlackとかDiscordみたいなチャットで議論の最中に、議論に参加していない人に質問とかしたくなる。そのときどこでメンションを飛ばすか選択肢があるけど、議論の場でメンション飛ばす形で召喚するのがいいよなと思った話をする。
選択肢としてはいかがありそう。
- 議論の場
- DM
- その人がよく出没するチャンネル
- LINE、電話、メールなどの違う媒体
相手に文脈を理解する余地を残すためにも、議論の場に呼ぶのが誠意なんじゃないかと思っている。
今日久しぶりに静的型付けな言語（Rust）を書いて、 match式は書くブランチの型が一致しないといけないことを思い出して、じゃあreturnする場合はどんな型をつけるんだ、と思ったので型規則を定義するならこんなふうになるんだろうなと想像してみる。
returnがあるってことは、関数があるということだ。その関数の返り値の型とreturnの部分式の型が一致しないといけないはずだ。これをトラックするために、型は3項関係ではなく、今の関数の返り値型を表す項が必要なはず。
型規則では、次のような関係を定義すれば良さそう。 $\Gamma \vdash e : \tau | r$ ここで $r$ は今の関数定義の返り値の型。
関数定義では、次のような感じになるだろう。
G, x: t1 |- e: t2 | t2
-------------------------------- (fun)
G |- lam x: t1. e: t1 -> t2 | r
そしてreturn式はこんな感じだ。
G |- e: r | r
--------------------- (return)
G |- return e: t | r
こうすることで、returnに任意の型をつけられるので、フランクにブランチの末尾でreturnできる。任意の型ではなくてユニット型とかを不用意につけるとearly returnをしにくくなったりしそう。
書いてみると意外と単純だった。本当にこれでうまくいくかは知らないけれど。