「多相関数」って言葉が意味不明ですが、それは一旦棚に上げて、リストの長さは多相関数の事例だとしましょう。リストの長さの宣言を次のように書くことがあります。
$`\quad \text{length} : \forall \alpha.\text{List}\, \alpha \to {\bf N}`$
ここで論理の全称記号を流用するのはやめて欲しい。確かに雰囲気は似てるけど、でもやめて欲しい。そう思う合理的な理由はありません。感情としてイヤなのね。
関数 $`\text{length}`$ はパイ型の要素になるので、次のように書けます。
$`\quad \text{length} \in \prod_\alpha [\text{List}\, \alpha , {\bf N}]`$
ここで、ブラケットは関数型〈指数型 | 内部ホム型〉です。$`\alpha`$ は型パラメータなので、“すべての型の集合”を仮に $`{\bf Type}`$ とすると、次のように書けます。
$`\quad \text{length} \in \prod_{\alpha\in {\bf Type}} [\text{List}\, \alpha , {\bf N}]`$
$`{\bf N}`$ は型パラメータに依存してませんが、パラメータによらず一定の型 $`{\bf N}`$ を返す型構成子〈型関数〉を $`\mathrm{K}_{\bf N}`$ とすると、次のように書けます。
$`\quad \text{length} \in \prod_{\alpha\in {\bf Type}} [\text{List}\, \alpha , \mathrm{K}_{\bf N}\,\alpha]`$
何か具体的な型 $`A`$ で型パラメータ $`\alpha`$ を具体化すると、次の関数が成分として現れます。
$`\quad \text{length}_A \in [\text{List}\, A , \mathrm{K}_{\bf N}\,A]`$
書き方を変えれば：
$`\quad \text{length}_A : \text{List}\, A \to \mathrm{K}_{\bf N}\,A`$
もう一度型パラメータに戻すと：
$`\quad \text{length}_\alpha : \text{List}\, \alpha \to \mathrm{K}_{\bf N}\,\alpha`$
この型パラメータ $`\alpha`$ は型の集合 $`{\bf Type}`$ 上を走るのだから、
$`\quad \langle \alpha \in {\bf Type}\rangle\: \text{length}_\alpha : \text{List}\, \alpha \to \mathrm{K}_{\bf N}\,\alpha`$
山形括弧を使ったのは、型パラメータは山形括弧に入れる印象があるから。
すぐ上のような書き方で僕は心が落ち着くけれど、2-射としての自然変換のプロファイルを書いたほうがよりスッキリします。
$`\quad \text{length}:: \text{List} \Rightarrow \mathrm{K}_{\bf N} : \mathcal{C} \to \mathcal{C}`$
ここで、$`\mathcal{C} `$ は集合圏の部分圏である適切なデカルト閉圏。
