Think of this like quoting and eval in Lisp. The type "expression of type U" might work with operations like

    eval: "expression of type U" -> U
    quote: U -> "expression of type U"

chriswarbo's reply higher up should be taken to supersede my reply -- he's obviously more current on this stuff.