Introduction to Programming in ATS:
Prev	Chapter 13. Introduction to Views and Viewtypes	Next

Viewtypes as a Combination of Views and Types

A linear type in ATS is given the name viewtype, which is chosen to indicate that a linear type consists of two parts: one part for views and the other for types. For instance, given a view V and a type T, then the tuple (V | T) is a viewtype, where the bar symbol (|) is a separator (just like a comma) to separate views from types. What seems a bit surprising is the opposite: For each viewtype VT, we may assume the existence of a view V and a type T such that VT is equivalent to (V | T). Formally, this T can be referred as VT?! in ATS. This somewhat unexpected interpretation of linear types is a striking novelty of ATS, which stresses that the linearity of a viewtype comes entirely from the view part residing within it.

The built-in sorts viewtype and viewt@ype are for static terms representing viewtypes whose type parts are of the sorts type and t@ype, respectively. In other words, the former is assigned to viewtypes for linear values of the size equal to that of a pointer and the latter to viewtypes for linear values of unspecified size. For example, tptr is defined as follows that takes a type and an address to form a viewtype (of the sort viewtype):

vtypedef tptr (a:t@ype, l:addr) = (a @ l | ptr l)

Given a type T and an address L, the viewtype tptr(T, L) is for a pointer to L paired with a linear proof stating that a value of the type T is stored at L. If we think of a counter as a pointer paired with a proof stating that the pointer points to an integer (representing the count), then the following defined function getinc returns the current count of a given counter after increasing it by 1:

fn getinc
  {l:addr}{n:nat}
(
  cnt: !tptr (int(n), l) >> tptr (int(n+1), l)
) : int(n) = n where {
  val n = ptr_get1<int(n)> (cnt.0 | cnt.1)
  val () = ptr_set1<int(n+1)> (cnt.0 | cnt.1, n+1)
} (* end of [getinc] *)

A particularly interesting example of a viewtype is the following one:

vtypedef cloptr
  (a:t@ype, b:t@ype, l:addr) =
  [env:t@ype] (((&env, a) -> b, env) @ l | ptr l)
// end of [cloptr_app]

Given two types A and B, a pointer to some address L where a closure function is stored that takes a value of the type A to return a value of the type B can be given the viewtype cloptr(A, B, L). Note that a closure function is just an envless function paired with an environment containing bindings for variables in the body of the closure function that are introduced from outside. In the function type (&env, a) -> b, the symbol & indicates that the corresponding function argument is passed by reference, that is, the argument is required to be a left-value and what is actually passed at run-time is the address of the left-value. I will cover the issue of call-by-reference elsewhere in more details. The following piece of code demonstrates a pointer to a closure function being called on a given argument:

fun{
a:t@ype}{b:t@ype
} cloptr_app {l:addr}
(
  pclo: !cloptr (a, b, l), x: a
) : b = let
  val p = pclo.1
(*
//
// taking out pf: ((&env, a) -> b, env) @ l
//
  prval pf = pclo.0
//
*)
  val res = !p.0 (!p.1, x)
(*
  prval () = pclo.0 := pf // putting the proof pf back
*)
in
  res
end // end of [cloptr]

Note that the linear proof in pclo is first taken out so that the code for dereferencing p (denoted by the syntax !p) can pass typechecking, and it is then returned so that the type of pclo is restored to its original one. This process of taking out a linear proof from a record and then putting it back into the record can be automatically performed by the typechecker of ATS.

The very ability to explain within ATS programming features such as closure function is a convincing indication of the expressiveness of the type system of ATS.

Prev	Home	Next
Introduction to Views and Viewtypes	Up	Left-Values and Call-by-Reference