ParaSail Universal types in Annotations

As explained in the prior entry, ParaSail has four universal types, Univ_Integer, Univ_Real, Univ_Character, and Univ_String, with corresponding literals.  The universal numeric types have the usual arithmetic operators, and the universal character and string types have the usual operations for concatenation and indexing.  In some ways values of the universal types may be thought of as abstract mathematical objects, while the values of "normal" types are the typical concrete representations of such mathematical objects, with attendant limitations in range or precision.  To connect a normal, concrete type to a corresponding universal type, the type defines the operator "from_univ" to convert from the universal type to the concrete type, and "to_univ" to convert back to the universal type.

In the prior entry, we learned that by defining "from_univ" a type can use the corresponding literal notation.  For example, imagine an Integer interface:

interface Integer<First, Last : Univ_Integer> is
    operator "from_univ"
      (Univ : Univ_Integer {Univ in First .. Last})
      -> Integer;
    operator "to_univ"(Int : Integer)
      -> Result : Univ_Integer {Result in First .. Last};
    operator "+"(Left, Right : Integer) -> Integer;
    operator "-"(Left, Right : Integer) -> Integer;
    ...
end interface Integer;

Because the "from_univ" operator is defined from Univ_Integer, integer literals are effectively overloaded on any type produced by instantiating the Integer interface.  So what about the "to_univ" operator?  If "to_univ" is provided, then ParaSail allows the use of a special convert-to-universal notation "[[...]]", which would typically be used in annotations, such as:

{ [[Left]] + [[Right]] in First .. Last }

This is equivalent to:

{ "to_univ"(Left) + "to_univ"(Right) in First .. Last }

This notation is intended to be a nod to the double bracket notation used in denotational semantics to represent the denotation or abstract meaning of a program expression. Using this notation we can give a more complete definition of the semantics of the Integer interface:

interface Integer<First, Last : Univ_Integer> is
    operator "from_univ"
      (Univ : Univ_Integer {Univ in First .. Last})
      -> Integer;
    operator "to_univ"(Int : Integer)
      -> Result : Univ_Integer {Result in First .. Last};
    operator "+"(Left, Right : Integer 
          {[[Left]] + [[Right]] in First .. Last}) 
      -> Result : Integer 
          {[[Result]] == [[Left]] + [[Right]]};
    operator "-"(Left, Right : Integer 
          {[[Left]] - [[Right]] in First .. Last}) 
      -> Result : Integer 
          {[[Result]] == [[Left]] - [[Right]]};
    ...
end interface Integer;

Here we are defining the pre- and postconditions for the various operators by expressing them in terms of corresponding universal values, analogous to the way that denotational semantics defines the meaning of a program by defining a transformation from the concrete program notations to corresponding abstract mathematical objects.

ParaSail character, string, and numeric literals

Almost all programming languages these days have special syntax for character literals (generally using single quotes), string literals (generally using double quotes), and numeric literals (digits, plus a decimal point for floating point, and optionally some sort of radix indicator for octal, hex, etc.).  Languages differ in how they distinguish among multiple string, character, or numeric types in the syntax for literals.  ParaSail adopts the usual syntax for these literals, but treats them each as being of a particular universal type.  Other "normal" types can provide conversions to and from these universal types, and thereby gain use of the corresponding literal notation.

The four basic kinds of literals in ParaSail, and their corresponding universal types, are as follows:

kind of literal	example	universal type
string literal	"this is a string literal"	Univ_String
character literal	'c'	Univ_Character
integer literal	42	Univ_Integer
real literal	3.14159	Univ_Real

The universal types can be used at run-time, but they are primarily intended for use with literals and in annotations.  Univ_String corresponds to UTF-32, which is a sequence of 32-bit characters based on the ISO-10646/Unicode standard.  Univ_Character corresponds to a single 32-bit ISO-10646/Unicode character (actually, only 31 bits are used).  Univ_Integer is an "infinite" precision signed integer type.  Univ_Real is an "infinite" precision signed rational type, with signed zeroes and signed infinities.

The universal numeric types have the normal four arithmetic operators, "+", "-", "*", "/".  They both also have an exponentiation operator "**", with signed Univ_Integer exponents for Univ_Real and non-negative Univ_Integer exponents for Univ_Integer.  Univ_Integer also has "mod" and "rem", corresponding to remainder operations, with "rem" being the remainder for "normal" truncate-toward-zero division, and "mod" being the remainder for truncate-toward-negative-infinity division.

Bitwise operators "and", "or", and "xor" are defined for non-negative Univ_Integers.  "<<" and ">>" are for shifting Univ_Integers, with "<<" defined as equivalent to multiplying by the corresponding power of two, and ">>" defined as equivalent to dividing by the corresponding power of two, but with truncation toward negative infinity.

By providing conversions to and from a universal type, a "normal" type can support the use of the corresponding literal.  These special conversion operations are declared as follows (these provide for integer literals):

operator "from_univ"(Univ : Univ_Integer) 
  -> My_Integer_Type;
operator "to_univ"(Int : My_Integer_Type) 
  -> Univ_Integer;

If an interface provides the operator "from_univ" converting from a given universal type to the type defined by the interface, then the corresponding literal is effectively overloaded on that type.  The complementary operator "to_univ" is optional, but is useful in annotations to connect operations on a user-defined type back to the predefined operators on the universal types.

Annotations may be provided on the conversion operators to indicate the range of values that the conversion operators accept. So for a 32-bit integer type we might see the following:

interface Integer_32<> is
    operator "from_univ"
     (Univ : Univ_Integer {Univ in -2**31 .. +2**31-1}) 
      -> Integer_32;
    operator "to_univ"(Int : Integer_32) 
      -> Result: Univ_Integer {Result in -2**31 .. +2**31-1};
    ...
end interface Integer_32;

With these annotations it would be an error to write an integer literal in a context expecting an Integer_32 if it were outside the specified range.

Bridge-crossing with Clojure

Solving puzzles has become popular among colleagues at the end of this year. One of these was the popular Bridge and torch problem. To summarize: four men have to cross a bridge in the dark with a torch, which can only light the way for two persons. These guys can cross the bridge in 1, 2, 5 and 10 minutes, respectively. When two people cross the bridge, it takes the time needed for the slower one to pass.

I'm not going to explain the optimal solution, but I wanted to show how this is a graph-traversal problem, which is amenable to solving using Dijkstra's algorithm. I also noticed that some clever guy has solved the puzzle using Prolog. So an idea was formed: generate the tree of solutions using a language, which I'm not really comfortable with (so I can practice and learn it better). I settled on Clojure, because I wanted to learn it this year (and the year is almost over).

The solution has a lot to do with sets. The state of each of the banks (which I'll call left and right) is a set of people, which are identified by their crossing speed. If we generate the list of possible combinations between the persons for each next move and recurse into them, then we'll have the tree of all solutions. In order to avoid indefinitely long (and stupid) solutions, we assume that going forward always takes two men, and going back takes only one.

The necessary libraries are set, combinatorics and str-utils. That's where I start:

(use '[clojure.contrib.combinatorics])
(use '[clojure.set])
(use '[clojure.contrib.str-utils])
(use '[clojure.contrib.pprint])

Here are the initial data structures: the two river banks are sets, the right one is empty:

(def left #{1, 2, 5, 10})
(def right #{})

And here's a first version of the solution:

(defn forward [left right steps minutes]
        (map #(back
                (difference left %)
                (union right (set %))
                (cons % steps)
                (+ minutes (reduce max %)) )
            (combinations left 2)) )

(defn back [left right steps minutes]
    (if (empty? left)
        (list steps minutes)
        (map #(forward
                (union left (set %))
                (difference right %)
                (cons % steps)
                (+ minutes (reduce max %)) )
            (combinations right 1)) ) )

(pprint (forward left right nil 0))

This prints some semblance of a tree, constructed by nested lists (hey, that's what Lisp is good for, remember?). What I didn't like about this is that there is too much repetition. There are many parts of these functions, which look the same. In order to evolve the solution, I wanted to extract the common parts in a single function:

(defn solve [from to steps minutes group]
    (if (and (empty? to) (not group))
        (list steps minutes)
        (mapcat #(solve
                (union to (set %))
                (difference from %)
                (cons % steps)
                (+ minutes (reduce max %))
                (not group) )
            (combinations from (if group 2 1))) ) )

(pprint (solve left right nil 0 true))

The function behaves differently depending on whether the group of people crossing consists of two or just one person. Also, the tree is now flattened, so the optimal solution can be easily found like this:

(print (reduce #(if (< (second %1) (second %2)) %1 %2) (apply hash-map (solve left right nil 0 true))))

Next step, I want to be able to collect a lot more data about each state, so I need to stop messing around with lists of lists and use something more organized like a hashmap. There's a reason Clojure includes the function second, but not third or, heaven forbid, fourth. Naming each part of your ad-hoc data structure plays a major role in readability.

(defn solve [from to steps minutes group]
    (if (and (empty? to) (not group))
        {:steps steps, :from from, :time minutes}
        {:steps steps, :from from, :time minutes,
            :solutions (map #(solve
                    (union to (set %))
                    (difference from %)
                    (cons % steps)
                    (+ minutes (reduce max %))
                    (not group) )
                (combinations from (if group 2 1)))} ) )

So now the interesting part can begin- rendering the tree in a nice graphical form using GraphViz. Watch this:

(defn printgraph [solution_tree]
    (let [steps (solution_tree :steps)
        nodename (if (nil? steps) "root" steps)
        from (solution_tree :from)
        label (if (= (count from) (count left)) (solution_tree :time) from)]
        (str "\"" nodename "\" [label=\"" label "\"];\n"
            (if (contains? :solutions solution_tree)
                ""
                (str-join ""
                    (map #(str "\"" nodename "\" -> "
                            "\"" (:steps %) "\""
                            " [label=\"" (intersection from (:from %)) "\"];\n"
                            (printgraph %))
                        (solution_tree :solutions)) ) ) ) ) )

And now you can output the recursive stuff wrapped with the header and footer like this:

(println "digraph G {")
(print (printgraph (solve left right nil 0 true)))
(println "}")

This graph shows each node as the state of alternating river banks, and the edges show the people crossing the bridge. The leaves display the number of minutes which it took for this particular combination of crossings.

I also wanted to generate a mind map for FreeMind, but since it doesn't support edge labels, I used the persons crossing for the nodes:

(defn mindmap [solution_tree]
    (str-join "\n"
        (map #(str
                "<node text=\"" (intersection (:from solution_tree) (:from %)) "\">"
                (mindmap %)
                "</node>")
            (solution_tree :solutions)) ) )

Now generating the complete file according to the FreeMind format:

(println "<map><node text=\"root\">\n")
(print (mindmap (solve left right nil 0 true)))
(println "</node></map>\n")

Finally, finding the optimal solution is just a wee bit more involved, because it requires traversing the tree recursively, but that's no problem for us anymore:

(defn optimal [tree]
    (if (contains? tree :solutions)
        (reduce #(if (< (second %1) (second %2)) %1 %2) (map optimal (tree :solutions)))
        (list (tree :steps) (tree :time)) ) )

(print (optimal (solve left right nil 0 true)))

In conclusion, I knew that one can write very compact code in Clojure (and any Lisp, in general), and this was certainly true here. I didn't use the Clojure-specific concurrency primitives or the lazy sequences, so my example would probably look similar in another Lisp. I did try to make it as functional as possible and Clojure does encourage that.

Some of the difficulties I had could be solved by static type checking, but I guess I'm spoiled by Scala. I've ran into small problems like renaming a variable and forgetting to rename (or misspelling) some instance of it in my code. I also tend to mix up which of the arguments to contains? comes first, and which second. This is probably because you can exchange a symbol as a key in a hashmap, and the hashmap without changing the meaning, e.g. (:from solution_tree) and (solution_tree :from). Of course, this is a problem with dynamic typing, not of Clojure in particular (and could probably be interpreted as a problem of using the language inappropriately).

Whatever the small hurdles, the problem was solved. Having fun? Check. Generating nice graphs and mind maps to impress colleagues? Check. Learning a bit of Lispy Clojure in the process? Check. Mission accomplished.

ParaSail module details

ParaSail has two kinds of modules, interface modules and class modules.  Every class module has a corresponding interface module.  Every non-abstract interface module has at least one class module implementing it.  All modules are effectively generic templates, in that they have formal module parameters which typically represent the types on which the module operates, or other module characteristics, represented by simple values.  A type is produced by instantiating a module, which means specifying actual module parameters for each of the formal module parameters, or relying on the defaults associated with the formal parameters.

As indicated above, the typical formal module parameter is that of a type.  Such a formal module parameter is of the form:

• [type_identifier is] interface_name '<' actual_parameter_list '>'

for example:

• Element is Assignable<>

or

• String<>

If a type_name is omitted, then within the module, the interface_name is treated as a type name.  If actual parameters are omitted, then any instance of the named interface is acceptable as the actual type.  If one or more actual parameters are specified, then the actual type ultimately provided must have matching actual parameters, for those that are specified.  Any actual parameters not specified are unrestricted.

Another kind of formal module parameter is a simple value:

• value_identifier : type_name

or

• value_identifier : interface_name '<' actual_parameter_list '>'  
  [ '{' constraint '}' ]
  

Simple values can be used to control selection among multiple classes that implement the same interface.  A class may specify a constraint on one of its value parameters which is more restrictive than the constraint on the corresponding parameter for its interface.  This class will only be used as the implementation if the actual value satisfies the given constraint.  If the actual values given satisfy multiple classes implementing the same interface, then the class with the highest preference value is chosen.  For example, an interface for a numeric type might have value parameters that specify the range or precision of numeric values that are to be represented by the numeric type.  Generally the class that uses a faster or more compact representation would be preferred, so long as the specified range or precision is satisfied:

interface Float 
  <First : Univ_Real; Last : Univ_Real; 
   Digits : Univ_Integer := 6> 
is
    operator "+"(Left, Right : Float) -> Float;
    operator "-"(Left, Right : Float) -> Float;
    operator "=?"(Left, Right : Float) -> Ordering;
    ...
end interface Float;  

Note that here we are presuming that Univ_Real and Univ_Integer are predefined, infinite precision numeric types, and Ordering is the predefined enumeration type returned by the comparison operator "=?" (see the blog entry on "Using the "=?" operator" for details).

The final kind of parameter is a function or procedure. This is intended to be a short-hand for constructing an interface with a single function or procedure in it, and then using that as a formal parameter.  It might be used to specify a special comparison function to be used for sorting, when the desired sort should not use the normal comparison operator of the type.  A parameter that represents a function or a procedure follows one of the following general patterns:

• function function_identifier '(' formal_parameter_list ')' '->' formal_result
  
• procedure procedure_identifier '(' formal_parameter_list ')'
• operator operator_string '(' formal_parameter_list ')' [ '->' formal_result ]
  

Here is an example Sorting interface that has a formal module parameter that is a comparison function:

interface Sorting
   <Sortable is Array<>;
   operator "=?"(Left, Right : Sortable::Element) 
      -> Ordering>
is 
     procedure Sort(Arr : ref var Sortable);
     procedure Reverse_Sort(Arr : ref var Sortable);
end interface Sorting;

ParaSail end-of-scope operator

When an object goes out of scope in ParaSail it may require some amount of cleanup.  For example, if the object provided access to some external resource, then when the object goes away, some release action on the external resource might be required.  This is provided by the "end" operator.  Here is an example of an interface for a Handle type, which will automatically release the associated resource at end of scope:

interface Handle<Filesystem<>> is
    function Create_Handle(
      FS : ref var Filesystem;
      Name : String) -> Handle;
    operator "end"(Obj : ref var Handle);
    ...
end interface Handle;

The compiler inserts a call on the "end" operator automatically at the end of the scope of an object.  The compiler ensures that "end" is called no matter how the scope comes to an end.  If an object is allocated from a region, then the "end" operator is invoked on the object immediately prior to deallocating the region. If an object has a value and is then assigned a completely new value, the "end" operator, if any, for its type is applied to the object prior to assigning it the new value.

In a composite object, the "end" operator is invoked on the enclosing object before invoking it on the component objects, so that the "end" operator of the enclosing object may safely refer to its components.

String interpolation in Scala

When I tried Scala for the first time, one of the first missing language features I noticed was string interpolation (you guessed it, I was using Ruby at the time). Of course, this is a small convenience rather than a major language feature and usually String.format and java.util.Formatter are pretty good substitutes. Still, string interpolation comes now and then in Scala discussions and one has to wonder if Scala's powerful language extension facilities can emulate a feature like this.

It turns out you can get reasonably close:

trait InterpolationContext {
  class InterpolatedString(val s: String) {

    def i = interpolate(s)
  }

  implicit def str2interp(s: String) = new InterpolatedString(s)

  def interpolate(s: String) = {
    val sb = new StringBuilder
    var prev = 0
    for (m <- "\\$\\{.+?\\}".r.findAllIn(s).matchData) {
      sb.append(s.substring(prev, m.start))
      val matchString = m.matched
      var identifier = matchString.substring(2, matchString.length - 1)
      try {
        val method = this.getClass.getMethod(identifier)
        sb.append(method.invoke(this))
      } catch {
        case _: NoSuchMethodException =>
        sb.append(matchString)
      }
      prev = m.end
    }
    sb.append(s.substring(prev, s.length))
    sb.toString
  }
}

object Test extends InterpolationContext {
  val a = "3"
  def main(args: Array[String]) {
    println("expanded: ${a}; not expanded: ${b}; more text".i)
  }
}

How does this work? If you call the i method on a String, it will force implicit conversion to a InterpolatedString, similar to how the r method works for converting to a Regex. The interpolate method uses reflection to find a method with the name equal to the identifier delimited by "${" and "}". This works both for vals and defs due to Scala's adhering to the uniform access principle. If the delimited string is not a valid identifier or a parameterless method with this name doesn't exist, it is not substituted, but stays as it is.

How do you use it? Just extend or mix in the InterpolationContext trait in the class where you want this to work, and then call i on the Strings where you want interpolation to work. The InterpolationContext trait serves two purposes- first of all, it imports the implicit conversion to the interpolated string, and second it provides access to the methods of the current object via reflection.

The limitations of this method are that interpolation only works on member vals and defs of the current object only. I rather like this, because you know you can't accidentally construct a String from user input in an html form like "Name: ${System.exec(\"echo echo pwned >> .bashrc\")}". Also, interpolation doesn't work for private members as well as local variables. Finally, you have to both mix in or extend the trait and call a method on every String (even though it's a one-letter method). This is not too bad, because you can control the scope where interpolation works and therefore avoid and debug nasty surprises easier.

I don't see this as a pattern, which can be used in real-life projects, and I don't see the use of implicits here worthy of emulation. Nevertheless, trying to copy features from other languages is instructive about the limitations of your current language of choice and the tradeoffs you get for these features. Last but not least- even if it's a gimmick feature, implementing it was fun.

Error detection with pattern matching

Scala's pattern matching is one of the most powerful features in the language. It not only helps write concise and very readable code, but also helps prevent trivial errors.

Let's say you want to save a line or two of code when comparing for some empty data structure like a List. You decide to use comparison for equality:

val items = Nil
if (items == Nil) println("No items")

Then you decide to refactor and turn the items collection into a Set. The Scala compiler is clever and should give you a warning, right? Well, not quite:

val items = Set()
if (items == Nil) println("No items")

This results in nothing printed, as the expression evaluates to false. Of course, given the types it's perfectly clear at compile-time that this will never be true. Can't the compiler give you a hint? Indeed, it will if you use pattern matching:

items match {
  case Nil => println("No items")
  case _ =>
}

This will result in the following error message:

error: pattern type is incompatible with expected type;
 found   : object Nil
 required: scala.collection.immutable.Set[Nothing]
         case Nil => println("No items")
              ^

The examples are contrived (unparameterized Nil and Set?), but you get the point. Yes, Nil can never be a value of the Set type. You might think this is fairly obvious, but pattern matching can be a life saver when implicit conversions are involved. Consider this:

"heh".reverse == "heh"

What does this evaluate to? This should be obvious, right? But the value is false! If you used pattern matching, you would easily see why:

"heh".reverse match {
  case "heh" => "obvious?"
}

This will make the compiler very nervous, and this is the reason why:

error: type mismatch;
 found   : java.lang.String("heh")
 required: scala.runtime.RichString
         case "heh" => "obvious?"
              ^

So reverse converts the String to the wrapper RichString, which is not the same type as String.

I have had similar problems detecting a bug where I was checking for equality with None a variable which was of type net.liftweb.common.Box (a type very similar conceptually to Scala's built-in Option).

This made me adopt a general rule to prefer pattern matching rather than equality comparison. The bugs it catches are sometimes subtle and hard to see, and that's exactly what Scala's rich static type checker tries to avoid. Use it to your advantage.

Since we're talking about bugs caught by pattern matching, there's one subtle bug, which is often (though not always) caught by the compiler (another contrived example follows):

val items = Set()
Set() match {
  case items => println("empty")
  case _ => println("full")
}

This will result in an error, which looks a little bit unusual to the newbie:

error: unreachable code
         case _ => println("full")
                   ^

This error is usually crying out loud: hey, you're inadvertently using variable binding instead of constant matching! The newly bound variable items shadows the existing variable with the same name and all other cases after it will never match.

One way to fix it is to use backticks to prevent the name to be bound to a new variable:

Set() match {
  case `items` => println("empty")
  case _ => println("full")
}

As a rule of thumb it is advised to use CapitalLetters for case classes and constants which you intend to pattern match.

This error wouldn't have occurred if you used equality comparison in the first place, but even in mildly complex cases pattern matching trumps plain equality checking in readability and detecting errors. Apparently, there are cases where pattern matching fails (for instance, matching structural types), so there's still no reason to deprecate good old "==". But there are many more errors, which pattern matching catches, like checking if the match is exhaustive. So there's no point in saving a couple of characters but lose the type safety you expect from Scala.

Best Android Apps by Category

Social Networking

• Twidroid (Twitter client)
• Facebook
  

Podcasts

• DoggCatcher
• Easy control over when podcasts downloaded

Desktop Music Syncing Software

• Salling Media Sync
• Allows you to sync iTunes with your Android phone
  

Music Listening

• Built-in Music App

Language Learning

• Anki
• Flashcard app
  
• Does not sync with Anki Online

Productivity

• Remember the Milk (Todo list w/ online sync)
• Movies by Flixster
• FeedR News Reader

Utilities

• WiFi OnOff
• Barcode Scanner
• Astro (File Browser)

ParaSail concurrent interfaces

A ParaSail interface can be marked as concurrent, meaning that an object of a type produced by instantiating such a concurrent interface can be accessed concurrently by multiple parallel threads.  We use the term concurrent type for a type produced by instantiating a concurrent interface, and concurrent object for an object of a concurrent type.

Both lock-based and lock-free synchronization techniques can be used to coordinate access to a concurrent object.  In addition, operation queues are provided to hold operation requests that cannot be serviced until the concurrent object attains a desired state, as specified by the dequeue condition.  When a thread initiates an operation request, if it can't be performed immediately because the condition is False, the thread is blocked until the request gets dequeued and the associated operation is completed, or the operation request is canceled for some reason, such as a timeout.   In general, multiple operation requests may be queued simultaneously on behalf of a single thread, with the first one to be dequeued causing the automatic cancellation of the others.

With a lock-based concurrent interface, one of the operands of a procedure or function of the interface, if the operand is of the type defined by the interface, can be marked indicating it should be locked upon call. When calling the operation,  the operand's lock will be acquired automatically upon entry to the operation, and the lock will be released upon return.  Alternatively, one operand of a concurrent interface operation may be marked queued, meaning that the dequeue condition must be true before the operation will be performed, and when it is performed it will be locked automatically as well.

Within the concurrent class implementing a lock-based concurrent interface, the components of an operand marked locked or queued may be referenced directly, knowing that the access is single-threaded at that point.  If there are other (non-locked/queued) operands of the associated concurrent type, their non-concurrent components may not be referenced by the operation.  An operation with a queued operand has the further assurance that at the point when the operation starts, the dequeue condition is True.  The dequeue condition for a given operation may depend on the values of the non-concurrent parameters, plus the internal state of the (concurrent) operand marked queued.

Within the concurrent class implementing a lock-free concurrent interface, all data components must themselves be concurrent objects, since no locking is performed on entry to the operations of the class.  Typically these components will be of low-level concurrent types, such as a single memory cell that supports atomic load, atomic store, and atomic compare-and-swap (CAS), or a somewhat higher-level concurrent type that supports multi-word-compare-and-swap (MCAS).  The ParaSail standard library provides a small number of such lower-level concurrent types to support implementing lock-free concurrent interfaces.  The higher level queued operations are implemented using a lower-level race-free and lock-free concurrent type similar to a private semaphore, which can be used directly if desired.

Here is an example of a concurrent interface and corresponding concurrent class for implementing a simple bounded buffer:

concurrent interface Bounded_Buffer
  <Element_Type is Assignable<>;
   Index_Type is Integer<>> is
    function Create_Buffer(
      Max_In_Buffer : Index_Type {Max_In_Buffer > 0})
      -> Result : Bounded_Buffer;
      // Create buffer of given capacity

    procedure Put(Buffer : queued Bounded_Buffer; 
      Element : Element_Type);
      // Add element to bounded buffer; 
      // remain queued until there is room
      // in the buffer.

    function Get(Buffer : queued Bounded_Buffer)
      -> Element_Type;
      // Retrieve next element from bounded buffer;
      // remain queued until there is an element.
end interface Bounded_Buffer; 

concurrent class Bounded_Buffer
  <Element_Type is Assignable<>;
   Index_Type is Integer<>> is
    const Max_In_Buffer : Index_Type {Max_In_Buffer > 0};
    var Data : Array<Element_Type, Index_Type> := 
      Create_Array(1, Max_In_Buffer);
    var Next_Add : Index_Type 
      {Next_Add in 1..Max_In_Buffer} := 1;
    var Num_In_Buffer : Index_Type 
      {Num_In_Buffer in 0..Max_In_Buffer} := 0;
  exports
    function Create_Buffer(
      Max_In_Buffer : Index_Type {Max_In_Buffer > 0}) 
      -> Bounded_Buffer
      // Create buffer of given capacity
    is
        return (Max_In_Buffer => Max_In_Buffer);
    end function Create_Buffer;

    procedure Put(Buffer : queued Bounded_Buffer; 
      Element : Element_Type)  
      queued until 
        Buffer.Num_In_Buffer < Buffer.Max_In_Buffer 
      // Add element to bounded buffer;
      // remain queued until there is room
      // in the buffer.
    is
        Buffer.Data[Buffer.Next_Add] := Element; 
        // Advance to next element, cyclically.
        Buffer.Next_Add := 
         (Buffer.Next_Add mod Buffer.Max_In_Buffer) + 1;
        Buffer.Num_In_Buffer += 1;
    end procedure Put;

    function Get(Buffer : queued Bounded_Buffer)
      -> Element_Type
      queued until Buffer.Num_In_Buffer > 0 
      // Retrieve next element from bounded buffer;
      // remain queued until there is an element.
    is
         return Buffer.Data[
           ((Buffer.Next_Add - Buffer.Num_In_Buffer - 1)
             mod Buffer.Max_In_Buffer) + 1];
    end function Get;
end class Bounded_Buffer; 

This concurrent interface has one constructor, plus two queued operations, Put and Get.  The dequeue conditions are provided as part of the implementation of an operation with a queued operand.  Here the dequeue conditions are Buffer.Num_In_Buffer < Buffer.Max_In_Buffer for Put, and Buffer.Num_In_Buffer > 0 for Get.  These dequeue conditions ensure that when the operations are performed, they can proceed without an error.

An example of a lock-free concurrent interface will be given in a later post.

ParaSail region-based storage management

In ParaSail, heap storage is broken up into regions which are generally deallocated as a whole, rather than one element at a time.  The concept of region-based storage management originated a decade or more ago, and was at the heart of the Cyclone programming language.  The region-based storage management in ParaSail is a bit different, but is certainly inspired by all this earlier work. 

To prevent dangling references, regions in ParaSail are reference counted.  The reference counting is done at the region level rather than at the individual object level, since deallocation happens at the region-as-a-whole level.  For a similar reason, rather than counting each individual pointer into the region, we (effectively) just keep track of the number of other regions that might contain objects pointing into the given region.  Before storing a pointer from an object in region A to an object in region B, a check is made that region B is reachable from region A via one or more region-to-region "handles."  The region-to-region handles form a reachability graph.

The programmer decides when to create a region-to-region handle, in anticipation of creating one or more object-to-object pointers.  The operation for creating a region-to-region handle is "Allow_Reference(From_Region, To_Region)." After invoking this operation, objects in From_Region are allowed to point at objects in To_Region, or in other words, To_Region is reachable from From_Region.  This cannot be revoked -- the region-to-region handles once created are immutable, until the From_Region goes away as a whole.  Reachability is transitive, so after this call, anything reachable from the "To_Region" is now also reachable from the "From_Region."

Allow_Reference can create a loop in the reachability graph.  Because the region-to-region handles are immutable, once such a loop is created, all regions in the strongly connected subgraph containing From_Region and To_Region will necessarily be deallocated simultaneously (their lifetimes will end at the same moment).  From a reference-counting perspective, this means that the reference counting is really best done at the strongly-connected-subgraph level, and the possibly-cyclic region graph can be collapsed into a directed acyclic graph (DAG) between strongly-connected subgraphs of the original region graph.

In addition to region-to-region handles, there are also scope-to-region handles associated with local scopes of the program.  To prevent pointers in local variables from ending up as dangling references, a pointer from a local variable to a region is only permitted if the region is reachable from the immediately enclosing program scope:  A region is (directly) reachable from a given program scope if there is a scope-to-region handle in that scope targeting that region.  Also, a region is reachable from a given scope if it is reachable from an enclosing scope.  The transitivity of reachability completes the picture in the usual way, so that if region A is reachable from region B, and region B is reachable from the current scope, the region A is reachable from the current scope.

As with region-to-region handles, scope-to-region handles are immutable, so that once a region is reachable from a given scope, it will remain so until the scope is exited.  The fundamental safety rule is that a region must not be deallocated if it is reachable from any still active scope of the program. Coupled with the requirement that local pointers may only point into reachable regions, this ensures that no local pointer can become a dangling reference.  Similarly, a pointer in a region A that is reachable from an active scope, cannot become a dangling reference because it can only point at an object in a region B if B is reachable from A and, transitively, from the same active scope.  

An alternative way of describing this notion of scope-to-region handles is that each scope has its own local region, and scope-to-region handles are actually region-to-region, the difference being that they go from a local region to a non-local, reference-counted region.  Note that local regions would never be reference counted, since upon leaving the scope, they are always deallocated.  For similar reasons, one would never allow a handle, nor a pointer from a non-local region to a local region, nor from the local region of an enclosing scope to a local region of a nested scope.  So all in all, calling each scope a  region may not actually simplify the model very much -- local regions would still have a number of special rules.

In addition to the two kinds of region handles we have described, there are two additional kinds of references that affect region lifetime -- strong references and weak references.   Both of these are internally a pair of a region handle and a pointer to an individual object.  The pointed-to object is guaranteed to be in a region reachable from the one designated by the handle. 

The region handle in a strong reference is reference counted, meaning that as long as the strong reference exists, the designated region and any region reachable from it will not be deallocated.  The big difference between the region handle in a strong reference and a normal region handle is that it is not immutable.  A strong reference can be a variable, and may be reassigned to point at a different region/object.  A normal region handle is immutable because it is "protecting" an arbitrary number of pointers that depend on it to prevent dangling references.  By contrast, the handle in a strong reference is only "protecting" the single pointer with which it is bound, so there is no problem allowing it to be reassigned in conjunction with reassigning the pointer.  To actually use a strong reference, the reference must be split into its constituent parts, producing a scope-to-region handle at the point of the use, along with a pointer protected by the scope-to-region handle in a local variable.  Once the strong reference has been split out, the strong reference could then be reassigned to point elsewhere, or to point nowhere (i.e. set to null).

A weak reference is similar to a strong reference, except that it does not prevent the designated region from being deallocated.  Whether the designated region has been deallocated is determined when the weak reference is split out.  If the result of splitting the weak reference is a null region handle and a null pointer, then the designated region has at some point been deallocated, presumably due to the underlying storage manager running low on overall available storage. 

A weak reference is useful for caching, by pointing to data that can be reconstructed when needed, but where reconstructing it is somewhat expensive -- for example, data coming from a file or a separate database, or data that is the result of a complex calculation.  The weak reference can be put in a cache for recently used results, which is checked first when a result is needed.  If a weak reference exists for the needed result, and after splitting turns out to be non-null, then the expense of reconstructing the result can be avoided.  If is is null, then the data must be reconstructed.

More on regions in a later posting...

Embedded Scala interpreter

The Scala interpreter is proof that a statically typed language can have features most people only expect from a dynamically-typed language. One of the cool uses of an interpreter is embedding it within your application. This allows you to conveniently experiment with Scala and probably even interact with object instances in your running system. I won't explain how the interpreter works here, but I will try to show you a simple way of embedding the interpreter.

As it usually happens, someone beat me to it. Josh Suereth explains in great detail how to embed an interpreter, but he has done so many customizations that his solution would probably fit on several pages.

I wanted a simpler solution which one could understand at a glance. The code for Lord of the REPLs is much shorter although it doesn't customize much of what the standard interpreter offers.

I tried to come up with the shortest working version you could possibly get away with. Provided I create the settings properly, this is what I could muster:

val out = new java.io.StringWriter()
val interpreter = new scala.tools.nsc.Interpreter(settings, new PrintWriter(out))
interpreter.interpret(code)

Not too much code, is it? (Half of it is probably due to the full package names). Now you could collect your output from the "out" stream and probably convert to String if you need using "out.toString".

Not so fast, though. I said this works if I have the appropriate settings:

val settings = new scala.tools.nsc.Settings()

The problem here is that the interpreter doesn't find two of the crucial jars needed for its proper functioning: scala-compiler.jar and scala-library.jar. When it doesn't it spits out the following error:

scala.tools.nsc.FatalError: object scala not found.

Thanks to the following discussion by Eric Torreborre (author of Specs) I managed to find out that one needs to add to the bootclasspath of the settings object:

val origBootclasspath = settings.bootclasspath.value
val pathList = List(jarPathOfClass(compilerPath),
                         jarPathOfClass(libPath))
settings.bootclasspath.value = (origBootclasspath :: pathList).mkString(java.io.File.separator)

One could hardcode the path to these two jars, but that's not too flexible. If we want to do it right, we might create a function which discovers the path to the jar from the name of a class that's in it:

def jarPathOfClass(className: String) = {
  Class.forName(className).getProtectionDomain.getCodeSource.getLocation
}

Now you could find the paths to these jars like this:

val compilerPath = jarPathOfClass("scala.tools.nsc.Interpreter")
val libPath = jarPathOfClass("scala.ScalaObject")

I've read that getProtectionDomain.getCodeSource returns null in some classloaders and might have problems specifically with OSGi. In that case, one might need to resort to the following hack:

def jarPathOfClass(className: String) = {
  val resource = className.split('.').mkString("/", "/", ".class")
  val path = getClass.getResource(resource).getPath
  val indexOfFile = path.indexOf("file:")
  val indexOfSeparator = path.lastIndexOf('!')
  path.substring(indexOfFile, indexOfSeparator)
}

With the last ugly piece of code creating an interpreter is not so concise anymore, but sometimes you can't be both robust and concise.

If you want to see the above snippets assembled in one piece you can check out Apache ESME's source code for the ScalaInterpreter action.

Warning: interpreting code directly in your application is a huge security risk and might not always be a good idea.

Using "=?" in ParaSail to implement "==", "!=", "<=", ">=", etc.

Here is a simple ParaSail feature.  It is often the case that a user-defined type will have its own definition for equality and comparison.  However, it is always a bit of an issue to make sure that "==" and "!=" are complements, and similarly for "<" and ">=", ">" and "<=".  ParaSail skirts this issue by requiring the user to define only one operator, "=?", which returns a value from the enumeration Less, Equal, Greater, Unordered.  The comparison and equality operators are defined in terms of "=?" (which is pronounced "compare"), in the natural way:

• "==" -- Result of "=?" is Equal
  
• "!="  -- Result of "=?" is not Equal
  
• "<"   -- Result of "=?" is Less
  
• ">"   -- Result of "=?" is Greater
  
• "<=" -- Result of "=?" is Less or Equal
  
• ">=" -- Result of "=?" is Greater or Equal
  

"Unordered" is used for types with only a partial ordering (or no ordering at all).  "Ordered" is defined as the subtype containing only the values "Equal," "Less," and "Greater."  The typical generic "Sort" operation would expect a "=?" operator whose result is guaranteed (via a postcondition) to be within the "Ordered" subtype.

The "=?" operator can be used explicitly if desired, which is often convenient when searching a binary tree:

    case Desired_Key =? Node.Key of
        Equal :   return Node;
        Less :    return Search(Node.Left, Desired_Key);
        Greater : return Search(Node.Right, Desired_Key);
    end case;

This would be another situation where the "=?" would be required to return an Ordered result, since we don't have an alternative that handles "Unordered."

ParaSail's implicit parallelism

As mentioned in the original overview of ParaSail, implicit parallelism is at the heart of ParaSail (and of its name!).  Every procedure/function call with multiple parameters involves implicit parallelism, in that all of the parameters are evaluated in parallel.  Handoff semantics is used for writable parameters, meaning that a (non-concurrent) object that is writable by one parameter evaluation, isn't available to any other parameter evaluation.  Operations on concurrent objects are not ordered.

Furthermore, in a sequence of statements, the only default limitation on parallelism is that imposed by operations on non-concurrent objects.  Parallelism can be inhibited by using ";;" instead of merely ";" to separate two statements.  This forces sequencing for operations on concurrent objects, which would otherwise not have any specified order.  By contrast, "||" can be used to indicate that parallelism is expected, and it is an error if there are conflicting operations on non-concurrent objects in the statements on either side of the "||".  That is, two statements separated by "||" are executed effectively in parallel, just as though there were embedded within two different parameter evaluations to a single procedure or function call.

For example:

    X := F(A, B);
    Y := G(B, C);;
    Z := H(R, S) || Z2 := Q(R, T);

As implied above by the formatting, "||" has highest precedence (binds most tightly), ";" next, and ";;" lowest (binds least tightly).  So in the above, the assignments to X and Y are ordered only if that would be required by the shared use of B (at least one of them has B as a writable parameter).  The assignments to Z and Z2 occur in parallel, and it would be an error if the shared use of R is unsafe (e.g. because R is writable by one or both, and is not a concurrent object).  The assignments to X and Y will complete before beginning the assignments to Z and Z2 (though of course, a "very intelligent" compiler might still find parts that can be executed in parallel because they can't possibly affect one another).  In all cases the evaluations of the parameters to a single procedure/function call happen in parallel.

Parentheses can be used to override the precedence for the statement separators:

    (M := N(A, B) ;; P := T(A, X)) ||
      (J := K(X, Y); M2 := N2(Y, Z));

In the above the assignment to M completes before the assignment to P starts.  The assignments to J and M2 occur in parallel unless the shared use of Y makes that unsafe.  And the assignments to M and P occur in parallel with the assignments to J and M2, and it is an error if there are conflicts due to shared use of X.

Note that ";" is both a statement separator and a statement terminator.  On the other hand, ";;" and "||" are only meaningful as statement separators.

Implicit parallelism also shows up in ParaSail loops.  The iterations of a for loop in ParaSail are executed as though each iteration were separated from the next by a ";", but with no particular ordering on the iterations.  A particular ordering may be specified by using the forward or reverse keyword, which effectively puts a ";;" between the iterations. Alternatively, the concurrent keyword may be used to indicate that the iterations should be effectively separated by "||", in which case it is an error if there are any conflicts due to operations on a non-concurrent variable.  For example:

    // compute sum of array A 
    for I in 1..10 loop
        Sum += A[I];
    end loop;

    // find last element equal to Z
    for I in 1..10 reverse loop
        if A[I] == Z then
             Last_Z := I;
             exit loop;
        end if;
    end loop;

    // sum the arrays B and C to produce A
    for I in 1..10 concurrent loop
        A[I] := B[I] + C[I];
    end loop;

Not too surprisingly, an exit loop statement is only permitted in a forward or reverse loop.

As illustrated above, parallelism is the default in ParaSail.  It is our belief that that is the only way that programmers will learn to take full advantage of the multicore world.  That is, in ParaSail, it is more work to create non-parallel algorithms than to create parallel ones, so programmers, being fundamentally a lazy lot, will end up writing mostly parallel algorithms in ParaSail.

We will cover ParaSail's structured synchronization mechanism (concurrent interfaces) in another post.

Scala closures as poor man's mocks

Groovy has this feature that you can use a closure whenever you need an interface with one method only. A class implementing the interface is automatically created, and the closure provides the implementation of this single method. This process is called closure coercion and is particularly convenient to make tests readable and concise.

I'm not yet sure about the relative advantages of such code everywhere, since there might be ambiguities or the intent might be obscured. Tests usually contain a lot of boilerplate, though, so I'm all for making them more concise. Except for readability, people would be more likely to write a test if it doesn't take much effort to create yet another trivial mock.

Who tests your tests though? You don't need to answer. Still, the page about implementing interfaces in Groovy warns of this trap: "Be careful that you don't accidentally define the map with { }". Type safety could help sometimes when writing tests. Or at least that's a very good excuse to try to emulate this Groovy feature in Scala.

In Scala there are implicit conversions, which help define a controlled way to coerce a value to a different type. We cannot automatically convert all closures to all possible single-method interfaces in scope, but we can choose several we are using especially often (as it happens in tests). For instance, if we want to use a mock of java.lang.Readable often enough, we could define the following implicit conversion:

import java.nio.CharBuffer

implicit def fun2readable(f: Function1[CharBuffer,Int]): Readable =
  new Readable { def read(cb: CharBuffer) = f(cb) }

So now everywhere we need a Readable, we might just drop in the appropriate closure instead (technically, this is not a mock, but a stub):

val readable: Readable = {cb: CharBuffer => cb.put("12 34"); 5}
val s = new java.util.Scanner(readable)
assert (s.nextInt == 12)

Compare this with the Groovy version:

def readable = { it.put("12 34"); 5 } as Readable
def s = new Scanner(readable)
assert s.nextInt() == 12

In the Scala version, we are explicitly defining the type of the variable in order to force the implicit conversion. In methods, where Readable is expected as an argument, explicitly naming the type will not be necessary, whereas in Groovy you always need to coerce using "as Readable":

val s = new java.util.Scanner({cb: CharBuffer => cb.put("12 34"); 5})

So in Scala you're trading some verbosity up front for some conciseness in all of the code where the implicit conversion is visible. Furthermore, the type checker guarantees that only closures with the correct signature are converted to the interface in question (i.e. with an input of CharBuffer and output of Int) and will flag a compile-time error otherwise.

The reader might be tempted to also emulate map coercion, but beware of an unexpected difficulty: it's not easy to define both a closure (with one argument) and map coercion. Since a Map in scala is a function and due to type erasure, the compiler won't know whether to substitute the Map or the Function!

Can you generate these implicits automatically without defining them? Maybe with a Scala compiler plugin, but then you lose some of the transparency of knowing which implicits you've defined.

ParaSail has no global variables

ParaSail has no global variables.  So how does that work?  Global variables have long been recognized as trouble makers in the software world, and they get much worse in a language with lots of parallelism.  But can we eliminate global variables completely?  ParaSail tries to do that by eliminating any notion of statically allocated variables.  In C or C++, global variables are those marked static or extern, or in a language with modules/packages like Ada, global variables are those declared at the module level.  Although their declaration might be hidden, such variables still represent global, variable state, and still create trouble.

In ParaSail, interface modules are generic types, and class modules implement interfaces.  That is, after providing generic parameters to an interface, you end up with a type.  Any variable declared in a class is what is often called an instance variable, that is, there is one per object of the type defined by the class.  There is nothing corresponding to what are called class variables.  In other words, the variables declared in a class will always be effectively fields/components of some enclosing object.  You can of course also have local variables inside the body of a procedure or function, but these are never statically allocated; they are stack-resident variables only (automatic in C parlance).

So what do we have instead?  In many cases, we simply substitute local variables declared in some relatively high-level procedure or function body, which are then passed (by reference) to other operations as parameters.  In ParaSail, passing a variable as a parameter generally has handoff semantics, meaning that it can't be simultaneously passed to multiple operations that might execute in parallel, nor can it be passed twice to the same operation as two different parameters (thereby eliminating certain kinds of aliasing problems).

When it is necessary to have a data structure that can be accessible to multiple operations running in parallel, the data structure must be explicitly designed for concurrent access.  In other words it must be a concurrent data structure.  In ParaSail, an interface may be specified as a concurrent interface, and then all objects of a type defined by the interface support concurrent access.

Containers represent a kind of middle ground, where the enclosing container might be designed for concurrent access, but the individual elements might not be, and so handoff semantics would again apply to the individual elements.

There may be some concurrent interfaces that typically have exactly one object; that is they are typically singleton interfaces.  For example, the file system, or the database manager, or the system clock.  ParaSail provides a conceptual global singleton Context interface for these, whose singleton object has one component for each such singleton interface, identified using the name of the interface.  The Context must appear as a parameter for operations that ultimately need access to one of these singleton interfaces, signifying that the operation has potential side effects on these singleton objects.  It would always be preferable to pass in the actual singleton objects needed, but as a convenience, the Context pseudo-object is available. 

The Context pseudo-object is provided as a parameter to the main entry point of a ParaSail application, so that it can gain access to these singletons and pass them on to callers.  If an operation has a Context parameter, and its caller also has a Context parameter, then the caller's parameter is passed automatically to the operation if not specified explicitly.  The Context parameter may be read-only ("in") or read-write ("in-out"/"var").  Not surprisingly, the actual Context parameter must be read-write if the formal is read-write.

ParaSail Topics to come

The prior entries gave an overview of ParaSail.  Over the next few weeks I hope to write additional entries about:

• ParaSail has no global variables, so how does that work?
• how iterators, streams and for-loops are interrelated in ParaSail;
• using a single compare primitive ("=?") in ParaSail to implement "==", "!=", "<=", ">=", etc.
  
• ParaSail's implicit parallelism and structured synchronization;
• ParaSail private interfaces and interface namespace hierarchy; 
• ParaSail's use of region-based storage management rather than object-at-a-time garbage collection;
  
• ParaSail's use of compile-time checks (mostly), run-time checks (goal is to never need them), and exceptions (only when complexity or race-conditions make them necessary);
  
• how attributes like taintedness (i.e. might this data come from a malicious source?) or physical units (e.g. meters/second, years, ...) can be "layered" onto existing types, along with appropriate pre- and postconditions, to provide additional security, safety, or correctness checking.  Add-on attributes can also be associated with statements or other ParaSail constructs, such as an attribute indicating whether a given statement or operation is potentially blocking (that is, it might wait indefinitely on some queue or some other synchronization structure), or the total amount of stack space required by a given statement or operation.
  

So stay tuned.  If you as a reader have other topics you would be interested in seeing further elaborated, please post a comment to that effect.

ParaSail pass-by-reference

In ParaSail, operations like array indexing generally take and return a ref.  What exactly is a ref?  The intent is that it is roughly an address, but we would also like to use them as representing an arbitrary place in a more general container-like structure (such as a hash table).  And we might want to use them to query whether an object is present, without actually inserting into the container as a side-effect.  So it might be useful to think of a ref as a special kind of object with three operations:

• fetch contents
• store contents
• check if present/exists/is-initialized

One could define the "Ref" interface roughly as follows:

  abstract interface Ref<Target_Type is Any<>> 
  is
      function Exists(R : Ref) -> Boolean;
      function Fetch(R : Ref {Exists(R)}) -> Target_Type;
      procedure Store(R : Ref; 
        New_Contents : Target_Type) {Exists(R)};
  end interface Ref;

A ref is sort of a place-holder, or perhaps a prescription for where to store an object, without necessarily making room for the object until it is actually stored.  For a hash-table like container, a ref to one of its elements might be the key value, which isn't actually inserted into the hash-table until the Store occurs.  One could imagine a hashed-mapping or a sparse array where you specify a "default" value for elements that have never been stored, and for such a structure, Exists would always return True, and Fetch would return the default value if no prior Store into the same ref had occurred.  And conceivably Store would be a no-op if the default value is being stored and no prior non-default value had been stored.

Another characteristic of a ref is whether the target object can be written, or only read.  That is, a read-only Ref would not have the Store operation.  It is desirable if the read-only-ness of a ref automatically flows through a function that takes the ref as a parameter.  That is, if the parameter to a function is a read-only ref, then clearly if the function returns a ref, then that returned ref should also be considered read-only.

This flow-through is common in many programming languages, where if an array is a constant, then so are its elements.  It is desirable not to have to define two versions of operator "[]", one for read-only refs, and one for writable refs, since presumably they will have an essentially identical implementation.  This argues for using ref as a parameter only when this flow-through semantics is desired, and presumably there will be an output that is also a ref.  The read-only-ness of the result ref would be determined from that of the ref parameter(s), and only if all of the ref parameters are writable would the result ref be writable.

If we don't want this flow-through, and instead really want to specify that a parameter be writable, then we might as well use something more explicit such as "var" or "in out" for such a parameter mode.

Rather than building in the flow-through rule, we could instead add another query into our hypothetical Ref interface, namely Is_Writable, and then use appropriate pre- and postconditions to constrain how writability flows through.  E.g. the postcondition for operator "[]" would be {Is_Writable(Result) = Is_Writable(Arr)}.  Clearly also the precondition of the Store procedure would be {Is_Writable(R)}.  This approach sounds more flexible, but it may be that we want the above flow-through rules as the default in the absence of some other specification.

Finally, we might want some default rules about whether Exists() should be True for a given ref parameter or result.  One would think that in general one would expect Exists(X) to be true if X is an incoming ref parameter, but one would not necessarily expect Exists(Result) to be true if Result is a ref result of an operation like "[]".  That is, the container should exist if you are indexing into it, but the selected element of the container doesn't necessarily exist just because you have used its key to index into the container.

Note that this general notion of Ref as an object in its own right would support object persistence fairly naturally, in that the Ref could be some kind of disk address, and not until you actually invoked Fetch or Store would you actually need to be sure that the relevant page of data is in memory.  These Refs are analogous to the "smart pointers" of C++, but they have the added advantage that they automatically have limited lifetimes (like "regular" C++ references), so they won't outlive the container into which they refer.

When inside a function, the non-ref result(s) of the function are in fact probably represented as refs provided by the callers, indicating where the results should be stored.  Such a ref would want to carry information about what region (in the region-based-storage-management sense) the result should be stored/built, so region can be thought of as another thing that is associated with a ref.  These are sort of write-only refs, or at least ones where the function wouldn't want to presume that Fetch is well-defined before performing at least one Store via the ref.  That is, Exists() would quite likely be False on entry to the function for each of the refs representing its results (aka "out" parameters).

Note that a general Ref object could also be used to represent an element of a packed array, where Fetch and Store would do the right thing in terms of unpacking/packing.  Of course this is getting dangerously close to pass-by-name of Algol 60 fame, and clearly sounds like it would require a thunk or equivalent.  But a (static or dynamic) polymorphic object and a thunk are not that much different anyway.  The expectation would be that the types of these Ref objects would often be statically known, so a compiler could choose to inline as appropriate to achieve the desired level of performance.

We might want to generalize Ref objects further by adding Create_Referenced_Object and Delete_Referenced_Object operations, since we already have an operation for testing whether the referenced object Exists.  This would make sense for a Ref to an element of a hash table, for example.  Essentially for any Ref where Exists might return False, it might make sense to be able to Create or Delete the referenced object.  In the above discussion, "Store" is presumed to create the referenced object if necessary, which is perhaps adequate for our purposes.  But Delete would be useful as a way to restore the original state where Exists is False.  This would only make sense for Refs where Exists can return False.