依存型の話
上記の記事を読んで、また少し、依存型についてのイメージが明確になったように思う。 圏論を勉強する途中で、その例として何度か依存型には出くわしているし、それとは独立の流れでも、「依存型っていうものがあるらしいけど、まだなかなか実践的なプログラミング言語には実装されていないらしい」みたいな言われ方をしているように記憶している（少しずつIdrisとかの話題を見るようになってきている気がしないでもないけど、自分はまったく詳しくないです）。
さて、圏論的な観点の話を続けることにする。定義をめちゃめちゃすっ飛ばして書いてるので雰囲気で察していただきつつ、2種類の依存型をそれぞれを「依存積」、
を「依存和」と呼ぶと、依存積が極限であり、依存和はその双対で余極限であることが上記のブログでは書かれている。依存積の方は
、つまり終対象だと考えるとわかりやすく、プログラミング言語でざっくりいうと「引数が同じ型を持つ関数から、一つの関数を作ることができて、できた関数の戻り値は元の関数の戻り値のいずれかを取る和型になる」ということですね。戻り値の型が2種類だとHaskellの
EitherやRustのResultで、TypeScriptだと元の戻り値がそれぞれX YだとするとX | Y型でしょうか。ということで普段よく見るものなのでそれほど違和感がない（上記ブログにもありますが、「依存積」だけどADTだと「和型」になるのがややこしいわけですね）。
そこでふと考えたんですが、それでは「依存和」のほうはプログラミング言語でいうと何に当たるんでしょう？自分なりにさっき思いついたことなので正解なのかどうか怪しいですが、圏論的には余極限ということなので、「依存積」の図式をひっくり返して考えてみると、「戻り値が同じ型を持つ複数の関数から、一つの関数を作ることができて、できた関数の引数は元の関数の引数のいずれかを取る」ということになるんでしょうか。これを上記の「和型」を引数に取る関数だと解釈してもいいですが、わたしの頭に浮かんだのはむしろ、オーバーロードされた関数でした。オーバーロードだと戻り値が同じでないといけないみたいな制限ってなかったでしたっけ…と思って調べてみると、必ずしもそういうわけでもないですね（JavaとC++を想定）。引数が全く同じなのに、戻り値だけ異なるメソッドを定義できない、という制限みたいです。うーん、違った、すいません。
さて、依存型の話題だと「要素数が制限された配列」みたいな話をよく見ます。これも「依存積」ですがADTの和型とは違っていて、結果の型が常に要素数の情報を持ち続けているということです。ただし、「値に応じて型が変化しうる」という点では同じなので、これも依存型です。その場合は極限になっている型が型コンストラクタにあたるわけですね。
Idrisの場合を見つけたので貼っておきます。わかりやすい。
Vectの定義
data Vect : Nat -> a -> Type where Nil : Vect 0 a (::) : x -> Vect n a -> Vect (S n) a infixl 7 ::
Vectの使い方
xs : Vect 5 Int xs = [1, 2, 3, 4, 5]
あ、冪と余冪の話もしたかったけど、またこんど。
