代数的データ型
この Haskell の List 型を型理論の別の形式で表すと、次のようになる。
μ φ . λ a .1 + α × φ α {\displaystyle \mu \phi .\lambda a.1+\alpha \times \phi \ \alpha }
μ {\displaystyle \mu } と λ {\displaystyle \lambda } が2つの定義で順序が入れ替わっている点に注意されたい。前者の形式は再帰型を本体とする型関数の定義であり、後者は型の再帰関数定義である。型変数 φ {\displaystyle \phi } は、これが β {\displaystyle \beta } のような基本型ではなく関数型であることを示している( φ {\displaystyle \phi } はギリシャ文字で "f" に相当する)。また、型本体の中の引数型 α {\displaystyle \alpha } に関数 φ {\displaystyle \phi } を適用しなければならない。
List の例の用途から考えると、これら2つの定式化に大きな違いはないが、後者の形式は「入れ子データ型; nested data type」と呼ばれる表現を可能とする。入れ子データ型とは、オリジナルとパラメータ的に異なる再帰型を派生させるものである。詳しくは、 Richard Bird、Lambert Meertens、Ross Paterson らの研究を参照されたい。