型レベル関数と型族、型演算子｜Haskellでの型レベルプログラミング

[kirakking]

あーなるほど、型レベルの関数に停止性を仮定できるから非左線形の書き換え規則が安全なのか。停止性は型の正規形を求めるために必要で、合流性は orthogonality により保たれていると。