The answer is positive. The reason is that exceptions
hide the types of values that they communicate, which may be recursive
types. We first to define two inverse functions
fold and unfold, using the following exception to mask types of
values:
| | |
| exception Hide of ((unit -> unit) -> (unit -> unit));; |
|
| | |
| let fold f = fun (x : unit) -> (raise (Hide f); ())
let unfold f = try (f(): unit); fun x -> x with Hide y -> y;; |
|
| | |
| val fold : ((unit -> unit) -> unit -> unit) -> unit -> unit = <fun>
val unfold : (unit -> unit) -> (unit -> unit) -> unit -> unit = <fun> |
|
The two functions fold and unfold are inverse coercions between
type U → U and U where U is unit → unit:
They can be used to embed any term of the untyped lambda calculus into
a well-typed term, using the following well-known encoding:
| [[x]] | = x |
| [[λ x. a]] | = fold (λ x. [[a]]) |
| [[a1 a2]] | = unfold ([[a1]] [[a2]]) |
|
In particular, [[fix ]] is well-typed.