Introduction to Programming in ATS:
PrevChapter 14. Dataviews as Linear DatapropsNext

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.

PrevHomeNext
Dataviews as Linear DatapropsUpDataview for Linear Arrays