viewtypedef initializable (vt:viewt@ype) =
  [initialized: bool] @{ initialized = bool initialized, obj = opt (vt, initialized) }

fun {vt:viewt@ype} uninitialized (v : opt(vt,false)): initializable vt

fun {vt:viewt@ype} exec_void (r: ref(initializable vt)):<!refwrt> void
fun {vt:viewt@ype} exec_void$fwork (v : &vt):<!wrt> void

fun {vt:viewt@ype} {a: t@ype} exec  (r: ref(initializable vt)):<!refwrt> a
fun {vt:viewt@ype} {a: t@ype}  exec$fwork (v : &vt):<!wrt> a

fun {vt:viewt@ype} initialize (r: ref(initializable vt)):<!ref,!wrt> void
fun {vt:viewt@ype} initialize$fwork (v: &vt? >> opt(vt,success)):<!wrt> #[success : bool] bool success