型理論と型システムは違うらしい

型

来月末に修論の中間発表というのがあって、ボチボチそれの準備をしている。
だいたい論文でも口頭発表でも最初に「背景」みたいな項目があって、自分のやっている研究というのがどのように重要か、もっと大きな視点から見たときにどのようなポジションに位置づけられるかなどを書く。これがないと、ほかの分野を研究している人からしたら、研究内容なんかほとんどまったくわからない。もちろん、よくできた人は「あーこれこれのことね」と瞬時にそういう研究の位置づけを理解するのだが、どんな社会でもそうであるように、そういうことを瞬時に理解できる人はそういない。

で、自分の研究というのが全体から見てどういう位置づけにあるのか、というのを書こうとしているのだが、これがなかなか難しい。ということで、今日はぼくがやっている分野の入門書的な

Programming in Martin-Löf's Type Theory
http://www.cse.chalmers.se/research/group/logic/book/book.pdf
という論文（本？）の最初の方を読んでいた。

そもそもぼくがやっている研究がどんなものか一言で言うと、新しいプログラミング言語をつくる研究、ということになるかと思う。まだ実際に作るというレベルには達していないような言語について、いろいろ理論的に研究している、という段階である。

どんな理論なのかというと、構成的型理論とか、直観主義型理論とか、マーティン・レーフ型理論と呼ばれるものなのだが、このあたりの話から始めるとちょっと長くなるのでまたこんど。

以下、今日理解したことを自分へのメモとして。

  • いわゆるCやJavaみたいな言語でのプログラミングで使われる「型」というのは、あくまでプログラミングにおける型システムの「型」。
  • マーティン・レーフ型理論でプログラミング云々と言っているのは、上記論文の題にも"in"とあるように、プログラミング自体をすべて型理論の枠内でやってしまおうという試みの話。
  • まったく関係がないわけではないが、この２つはかなり違う
  • で、型理論の中で全部いろいろやることにはいろいろなメリットがある。すべてが数学的なオブジェクトとして表現できるので、仕様を命題（型）として表記すれば、その命題の証明（あるいは型のインスタンス）がプログラムになる。
  • 仕様もプログラムも同じ枠組みの中で記述できて、プログラマの仕事はその仕様とプログラムの間のギャップを埋めること。仕様からプログラムをひねり出すこと。それは数学の証明を書く作業に似ている。
  • で、このときにいわゆる副作用をどのように表現するか、という問題がある。例えばHaskellにおけるmonadで入出力を表現する、といった解決法の話。
  • このとき、型理論の枠内でうまくそういった入出力を表現する方法がある。それが、コマンドとそのレスポンスのペアを使うやり方

んー、こういったあたりをうまく文章としてつなげていけばよいのか。