Wednesday, December 30, 2009

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.

Monday, December 28, 2009

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
universal type
string literal
"this is a string literal"
character literal
integer literal
real literal

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.

Wednesday, December 16, 2009

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<>
  • 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
  • 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> 
    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>
     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.