# Disjunctive Views

The dataview VOR is declared as follows:

```dataview VOR (v0:view+, v1:view+, int) =
| VORleft (v0, v1, 0) of (v0) | VORright (v0, v1, 1) of (v1)
```

This declaration indicates that the dataview VOR is covariant in its first and second arguments and there are two proof constructors associated with it: VORleft and VORright. Given views V0 and V1, a proof of VOR(V0, V1, 0) can be turned into a proof of V0 and a proof of VOR(V0, V1, 1) can be turned into a proof of V1.

Let T be some type. The following function interface states that getopt takes an unintialized pointer and returns an integers indicating whether the pointer is initialized:

```fun getopt{l:addr}
(pf: T? @ l | ptr (l)): [i:int] (VOR (T? @ l, T @ l, i) | int (i))
```

The following code shows a typical use of getopt:

```fun foo (): void = let
var x: T?
val (pfor | i) = getopt (view@(x) | addr@(x))
in
//
if i = 0
then let
prval VORleft (pf0) = pfor in view@(x) := pf0 // uninitialized
end // end of [then]
else let
prval VORright (pf1) = pfor in view@(x) := pf1 // initialized
end // end of [else]
// end of [if]
//
end // end of [foo]
```

In ATS, there is a type constructor opt that takes a type T and a boolean B to form an opt-type opt(T, B) such that opt(T, B) equals T if B is true and it equals T? if B is false. The function getopt can be given the following interface that makes use of an opt-type:

```fun getopt (x: &T? >> opt (T, b)): #[b:bool] bool(b)
```

The code that calls getopt can now be implemented as follows:

```fun foo (): void = let
var x: T?
val ans = getopt (x)
in
//
if (ans)
then let
prval () = opt_unsome(x) in (*initialized*)
end // end of [then]
else let
prval () = opt_unnone(x) in (*uninitialized*)
end // end of [else]
// end of [if]
//
end // end of [foo]
```

where the proof functions opt_unsome and opt_unnone are assgined the following types:

```prfun opt_unsome{a:t@ype} (x: !opt (a, true) >> a): void
prfun opt_unnone{a:t@ype} (x: !opt (a, false) >> a?): void
```

Compared to the version that uses VOR, this version based on opt-type is considerably less verbose.