2013-11-30

HaskellとType Theory

一昨日(20131128)はHaskell勉強会の２回目
Haskell(とそれを含む関数型言語)はType Theory(Wiki記事)と関係があるという
- Type Theoryは煎じ詰めると"In type theory, every "term" has a "type" and operations are restricted to terms of a certain type."
- Haskell(関数型言語)では、関数によって世界が構成されている
- 関数とは何かを取って、しかるべく評価して、何かを返すものである
  - 「しかるべく」とは「矛盾なく」とか「パラドクスに陥ることなく」と、論理学的には言う
  - 取る「何か」と返す「何か」とが、世界でうまく立ち回るためには、それは「どういうもの」なのかということを「はっきり」させる必要がある
  - 「どういうものなのか」を「はっきり」させる方法として「集合」があるが、言語学的に扱うと、(少なくとも初期の)集合だけではパラドクスが生じることが示された(ラッセルのパラドクス)
  - では、「どういうものなのか」を「はっきり」させる仕組みとして、「大丈夫」なものは何か、と考えたら、それが「Type Theory」だった
  - 一見しただけでは「同じ『何か』」であると見えて、「違う『何か』」であることがあって、その「一見では同じで本当は違う」ものは、「階層構造」を含むようだった
    - たとえば、"aである"と「"aである"ということである」は、ただの持って回った言い方のようだが、「発言」と「発言の引用(発言を括った再発言」という違いがある。これを区別するには、(少なくとも初期の)集合でやるのではなくて、「Type Theory」のように、階層構造を持ち込むのがよい、という経緯らしい
このことを言語学的には「一階の述語論理」「二階の術語論理」というような言い方で「階層構造の複雑化」を言い表す
扱う「何か」という『代数的データタイプ』(Wiki記事)
- また、「発言」と「発言を引用としての再発言」とは、「発言」に関する入れ子を作っていることになるのだが、それはHaskellのリストで言えばa:b:c:[]のように入れ子の重畳となる。このようにリストはType Theory的に、複雑な「何か定義」と関係するのだが、このリストのような「構成」をさらに一般化すると…
- 『代数的データタイプ』となる：すでに定義された何かをルールに基づいて(algebraicに処理できるというルールに基づいて)複雑化したもの、という意味
  - 何かしら、オブジェクト指向で作り上げるものと同じようだが、そこはどうも違うらしい(たとえばこちら)
  - どう違うか、というと「複雑な構造物」としてはOKだけれど、それが、システム全体として矛盾が生じないように作るという点に焦点を当てているのが、関数型言語でそれを支えているのがType Theory(複雑ではあるが矛盾がないようにね！、と言ったところ)。他方、オブジェクト指向は「局所的に、その人が作って動かす範囲で、なんとか整合性が取れていればよいという程度にだけ相互監視されている」という点が違う…？
  - じゃあ、人の操る自然言語は、まずまずコミュニケーションが取れている範囲(日本語内、とか)はオブジェクト志向的な『局所的範囲』であって、「ヒトたるもの、言語運用能力があってしかるべし」と言う部分は『関数型言語』的である、と、そういうことになる？？？
Haskellの型推論が強力なのは、型が「がっちり把握してある」からなのかなー、と