#読み違えていました、すみません。
#Robert Harper 様達の最近のお仕事(POPLとか)を見ても、プログラミングテクニックであると（正確には汎用性の高い logical framework）書いてあるのですが、論文ですし簡単には読めません
#Ulf の Bool の例とか、誰かが書いていた（忘れた）Vec や Fin の性質を証明するときに Universe を経由する話、とかでは満足されないでしょうか？
#読む代わりに、自分でどこまで書けるか書いてみるというのもアリかもしれません。僕も書きたいと思っています
#3.2 Universesは「型システムがよしなにやってくれる状況が作れる」とこが重要で
#「既に与えられた情報から特定の性質も(自然に型システムによって)決定できてそれも使いたい」ようなとき便利なのかなと
#たとえば，今stdlibにData.Rational._÷_という演算がありますが
#numeratorとdenominatorが具体的に与えられると「既約分数になるかどうか」が決定されて有理数が構成されます
#有理数は既約でないとleibniz equalityを満たさないので有理数recordには分子分母の他"既約"を示すfieldがあります．
#agdaのインタラクティブ実行(非推奨らしいですが)で + 1 ÷ 2 と + 2 ÷ 4 をそれぞれ叩いてみると差が見えるでしょう．たぶん
haskell-ja > Archives > 2013/04/24