日々の流転

λ. Towards Observational Type Theory. Thorsten Altenkirch and Conor McBride

• <URL:http://www.cs.nott.ac.uk/~ctm/ott.pdf>
• <URL:http://www.citeulike.org/user/msakai/article/585944>

Extensional Equality in Intensional Type Theory の話を発展させたもの。前の論文では proof irrelevance が本質的な役割を果たしていると思っていたが、実際にはそれほど本質的ではないというのにまず驚いた。

(詳しくは後で書く)

OTTは理論的にも面白いし、実用的にも便利そうな型理論だと思う。Epigramを使ってみたくなった。

λ. 高校の勉強ムズス

• 接弦定理なんて知らね
• 漢文の返り点の結合順位を誰か教えてくれ