和を持つラムダ計算

ツリーデータ型のモナドのモナドを具体的に書き下すととなると、けっこう難しいようだ。何が障害かというと：

1. 型がうまく定義できない。
   1. 空型と単位型
   2. 部分集合型、内包的記法
   3. ベキ集合型
   4. 直積型
   5. 指数型
   6. 直和型
   7. 依存和型
   8. 依存積型
   9. 型カインド
2. 処理がうまく書けない
   1. ラムダ記法
   2. 型付けと型注釈
   3. 型のラムダ抽象
   4. タグ付き値〈タグ付きインスタンス〉 v@t
   5. case-of-or-end文
   6. forsome-use文 インデックス付き型、依存和型のデータを処理する文
   7. tuple-and-end文
   8. cotuple-or-end文

より具体的な細かいこと

1. f(x), f[x], x.f, f_x, f<x> などの違いに惑わされる。
2. 型カインド（K⊆|C|）、型ファミリー（f:I → |C|） などに馴染みがない。型ファミリーは圏の離散図式。
3. 依存和型とタグ付き値が扱えない。

型理論だと、独自の用語法・記号法とぎごちない定式化になっている。