Simple Linear Objects

Objects in the physical world are conspicuously linear: They cannot be created from nothing or simply go vanished by turning into nothing. Thus, it is only natural to assign linear types to values that represent physical objects. I choose the name simple linear object here to refer to a linear value representing an object of some sort that does not contain built-in mechanism for supporting inheritance.

Let us first introduce a boxed abstract viewtype as follows for simple linear objects:

absviewtype sobjptr (a:viewt@ype+)

Given a viewtype VT, sobjptr(VT) is essentially meant for a pointer to some memory location L where a value of the viewtype VT is stored. The following function template sobjptr_new and function sobjptr_free are for creating and destroying (i.e., freeing) simple linear objects, respectively:

fun{a:viewt@ype} sobjptr_new (): sobjptr (a?)
fun sobjptr_free {a:t@ype} (x: sobjptr (a)): void

The abstract viewtype sobjptr can be given the following definition:

assume
sobjptr (a:viewt@ype) = [l:addr] @{
  atview= a @ l, gcview= free_gc_v (a?, l), ptr= ptr l
} // end of [sobjptr]

Subsequently, sobjptr_new and sobjptr_free can be implemented as follows:

implement{a}
sobjptr_new () = let
  val (pfgc, pfat | p) = ptr_alloc<a> ()
in @{
  atview= pfat, gcview= pfgc, ptr= p
} end // end of [sobjptr_new]

implement
sobjptr_free {a} (pobj) =
  ptr_free (pobj.gcview, pobj.atview | pobj.ptr)
// end of [sobjptr_free]

Clearly, a simple object needs to be initialized before it is of any use. This can be done by calling the following function sobjptr_init:

extern
fun sobjptr_init {a:viewt@ype}
  (pobj: !sobjptr (a?) >> sobjptr (a), f: (&a? >> a) -> void): void
// end of [sobjptr_init]

implement
sobjptr_init
  (pobj, f) = let
  prval pfat = pobj.atview
  val () = f !(pobj.ptr)
  prval () = pobj.atview := pfat
in
  // nothing
end // end of [sobjptr_init]

As a simple object may contain resources, it needs to be cleared out before it is allowed to be freed. This can be done by calling the following function sobjptr_clear:

extern
fun sobjptr_clear
  {a:viewt@ype} (
  x: !sobjptr (a) >> sobjptr (a?), f: (&a >> a?) -> void
) : void // end of [sobjptr_clear]

implement
sobjptr_clear
  (pobj, f) = let
  prval pfat = pobj.atview
  val () = f !(pobj.ptr)
  prval () = pobj.atview := pfat
in
  // nothing
end // end of [sobjptr_clear]

Note that each type T (of the sort t@ype) is a subtype of T?, implying that sobjptr(T) is a subtype of sobjptr(T?) (as sobjptr is co-variant). Therefore, sobjptr_free can be called directly on a value of the type sobjptr(T) without need to call sobjptr_clear on the value first.

Let us now see a concrete example of simple linear object. Suppose that a timer (that is, stopwatch) is wanted to measure time (of some sort). Following is a natural interface for functions creating, destroying and manipulating timer objects:

absviewtype timerObj

fun timerObj_new (): timerObj
fun timerObj_free (x: timerObj): void
fun timerObj_start (x: !timerObj): void
fun timerObj_finish (x: !timerObj): void
fun timerObj_pause (x: !timerObj): void
fun timerObj_resume (x: !timerObj): void
fun timerObj_get_ntick (x: !timerObj): uint
fun timerObj_reset (x: !timerObj): void

The (flat) record type timer_struct is defined as follows to represent the state of a timer object:

typedef
timer_struct = @{
  started= bool // the timer has started
, running= bool // the timer is running
  // the tick number recorded
, ntick_beg= uint // when the timer was turned on the last time
, ntick_acc= uint // the number of accumulated ticks
} // end of [timer_struct]

The abstract viewtype timerObj can then be mapped to sobjptr(timer_struct):

assume timerObj = sobjptr (timer_struct)

The functions timerObj_new and timerObj_free can now be given the following implementation:

implement
timerObj_new () = let
  typedef T = timer_struct
  fn f (
    x: &T? >> T
  ) : void = {
    val () = x.started := false
    val () = x.running := false
    val () = x.ntick_beg := 0u // unsigned
    val () = x.ntick_acc := 0u // unsigned
  } // end of [f]
  val pobj = sobjptr_new<T> ()
in
  sobjptr_init {T} (pobj, f); pobj
end // end of [timerObj_new]

implement
timerObj_free (pobj) = sobjptr_free (pobj)

For brevity, I omit the code implementing the other functions on timer objects, which the interested reader can find on-line together with some additional testing code.