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 welltyped term, using the following wellknown encoding:
[[x]]  = x 
[[λ x. a]]  = fold (λ x. [[a]]) 
[[a_{1} a_{2}]]  = unfold ([[a_{1}]] [[a_{2}]]) 

In particular, [[fix ]] is welltyped.