Higher-Order Abstract Syntax
Represent binding in the target language by binding in the meta langauge
datatype hexp = HAbs of hexp -> hexp
| HApp of hexp * hexp
| HSym of string
For example,
HAbs(fn x => HApp(HAbs(fn y => y), x)) : hexp
represents ?x. (?y. y) @ x