How to Reify?? When the Domain is a Function Type ?

• ?(???)?? v = ?x. v @ x　　　? Type Error

• ?(???)?? v = ?x. v @ (?y. x @ y)

• e.g. ?(b?b)?b (?f. f @ x) = ?y. (?f. f @ x) @ (?z. y @ z) = ?y. (?z. y @ z) @ x = ?y. y @ x
  

Previous slide

Next slide

Back to first slide

View graphic version