型と整数

http://d.hatena.ne.jp/m-hiyama/20080118/1200624718 にしたコメント

proj<0>(each:List):car(List) is car(each);
proj(each:List):proj(cdr(List)) is
proj(cdr(each):cdr(List));
で、再帰的に定義でしょうか。
C++ Templates: The Complete Guide に似たような案が載っていましたが、あま
り美しくないような(^^;
それと、あまりにも複雑な型システムは、型システム自体が停止問題に出会って
しまいそうな気がします。

Haskell の名前付きフィールドを連想しましたが、たぶんそういうことではない
のでしょうね。

型パラメータと値パラメータは違うか、ということでしたら、
ペアノ算術風に
class ZERO;
class SUC;
を型で定義して、パターンマッチができるならば本質的には何も変わらず、
値パラメータは略記だ、と思えばよいのではないでしょうか。

以前、
http://ripjohn.net/diary/2008_04.html#D2008_04_05
mmap 0 = id
…
mmap 3 = map . map . map
というような関数を考えた。これは Haskell の型付けではもちろんできない。

うーん。きれいにこういったものを受け入れられるような型システムはあるのかな。
型ではないが template Haskell?