dependent type

ちょっとわかりにくかった

この\Pi n:{\mathbb N}.\mbox{Vec}({\mathbb R},n)というのは、

function make_size_n_vector(n) {
  return new Array(n);
}

のような関数の型を表すもの。

単に「型Nの引数を受け取って、『要素型RのVec』を返す関数」じゃなく、「型Nの引数nを受け取って、『そのn個の要素型RのVec』を返す関数」という型が表現できるようにするものをdependent type（拡張した型システム）という感じ。型そのものはΠ型とかともいうらしい。

Curry–Howard(対応/同型)では、プログラム(コード)＝証明(手順)であり、型＝命題である。普通の型システムの型チェックは命題論理の証明チェックと同等ということになるのかな。その型システムで使う論理を一階述語論理と同じ表現ができるよう拡張したらこうなる感じ。アトミックな型=命題、関数型=→論理であり、dependent type＝述語となる。

ほかにはΣ型とかあるようだ。

このあたりのことが(型として)表現やチェックが可能になっているのが、Coqとかの定理証明ほにゃららと呼ばれるシステムの言語になるのだろう。