Danvy の TDPE: Reification

reify = 「eval の逆」

値 v とその型 ? ? eval(e) = v なる式 e の強正規形

?
関数の場合が問題 （他の場合は自明）
reify (? ? ?) v :=
(1) 引数の「代表」となる ? 型の値を生成

(2) 生成した値に v を適用
(3) 適用した結果である ? 型の値を reify

Previous slide

Next slide

Back to first slide

View graphic version