先に、「同じ」型A に属する二つの項 aとb(a : A かつb : A)が「同じ」だという a = b : A で表現される「同じ」さと、二つの型AとB(A : Type かつB : Type)が同じだという A = B : Type で表現される「同じ」さは、同じ「同じ」でも、違う「同じ」であるという話をした。 前者は、例えば、Aを「三角形」という型だとして、三角形a と三角形b が「同じ」だと言っているのだが、後者は、例えば、Aを{異なる三つの点を結んでできる図形}、Bを{平行でない三つの直線で囲まれた図形}とした時、AとBは、同じ型の図形であることを主張している。 型を持つプログラミング言語の場合、あるインスタンスがどの型に属するかを意識することは大事なことだ。面倒と言えば面倒なのだが、そのことがプログラムの誤りを少なくするのに効果的なのだ。 型を持つプログラミング言語のうちのいくつかは(例えば、COQ, Agda, Haskell, 部分的にはScalaも)は、不思議な型 dependent type をサポートしている。dependent type は、パラメータによって(パラメータにdepend して)、型が変わる型だ。 パラメータxが型Bを持つなら、このdependent type E(x)を次のように表す。 (x : B) E(x) また、あるsが、dependent type Eを持つことを、次のように表す。 (x : B) s(x) : E(x) あまり正確ではないが、B={ 整数、実数、複素数 }として x : B なるパラメータ x によって、dependent type E(x)は、整数型、実数型、複素数型 に型が変わるのだ。 昔のwakhok時代、同僚の浅見さんから、dependent type がすごいことはよく聞いていた。ただその頃、僕はそれをよく理解できなかったのだと思う。僕が、その重要性に気づいたのは、だいぶ後になってからだ。 5年前の2013年のマルレク「「型の理論」と証明支援システム — Coqの世界」で、ようやく後追いを始めることになる。 https://www.marulabo.net/docs/typetheory-coq/