登山は、人生と同じく、始まりと終わりのある物語である。
普段はこのブログには学術的、技術的なことを書くことが多いが、今回は趣向を変えて、登山について書くことにする（行ったのは8月）。
山に、行きたい。今年に入ってからまだまともに登山していない。去年せっかく買った1人用テントが泣いている（このテントの元を取るには最低10泊以上使う必要がある計算であるが、この時点でまだ3泊しかしていない）。
まず、どこに行くか。北アルプス？今現在北アルプスで行きたいと思っているコースは3泊4日以上あって大変だし、先日富山の実家に帰省したばっかりなのにまた戻るのはだるい。南アルプス？南アルプスの主だった山は全て登頂済みだ。まだ登ったことのない山、まだ行ったことのない山域に行きたい。
八ヶ岳。八ヶ岳は、メジャーな山域な割に筆者はまだ行ったことがなく（！）、標高2800mを超える高山で、東京からのアクセスも割と良い。八ヶ岳に行こう。 続きを読む
自分用メモ。 続きを読む
引き続き、型システムの勉強をしつつ、ラムダ計算の体系を実装している。 続きを読む
TVアニメ「クロムクロ」には富山県に実在する場所が数多く登場する。今年の1月に帰省した際に新湊周辺、8月に帰省した際に呉羽駅周辺の聖地巡礼をしてきたので、その記録を書いておく。 続きを読む
型システムの勉強の続き。
有界量化を持つ体系 System F<: (Fsub) に続いて、交差型を持つ体系 F∧ (Finter) を実装する。
作ったものは、前と同じ GitHub に置いてある：
https://github.com/minoki/LambdaQuest
TaPL でも交差型について言及されているが、あまり詳しく書いてあるとは言えない。そこで、B. C. Pierce の Programming with Intersection Types and Bounded Polymorphism (1991) という論文を参考にした。著者のサイトにPDFが置いてある。似たようなトピックの論文が他にもあるようだが、それらとの関係は確認していない。
論文の Finter では有界量化の上界に関して反変な部分型関係を入れているが、それをやると（TaPLにもあるように）部分型関係が決定手続きでなくなるらしいので、今回実装した Finter には（前回実装した Fsub にも）それは入れていない。
型システムを自分で設計したいと思ったので「型システム入門 プログラミング言語と型の理論」（原題：Types and Programming Languages, 略して TaPL）を読んで勉強している。
この記事は私の雑な理解を吐き出したものであり、あまりまとまっていない。しかし、何かしらをアウトプットすることに意義がある（ｷﾘｯ 続きを読む
JavaScriptで値を文字列化するにはいくつかの方法が考えられる。 続きを読む
ソースコードの -> や => などの記号を表示する際に、アスキー文字の組み合わせではなく → や ⇒ という風な本物の記号を使いたい。 続きを読む
Haskell で CGI を書いてみよう。 続きを読む
要約：Xy-pic か TikZ-cd を使おう。
LaTeX において可換図式を描くためのパッケージはいくつか存在する。この記事では、そういうパッケージをいくつか調べ、試してみた。 続きを読む