ParaSail enumeration types

We haven't talked about enumeration types in ParaSail yet.  One challenge is how to define an enumeration type by using the normal syntax for instantiating a module, which is the normal way a type is defined in ParaSail.  Generally languages resort to having special syntax for defining an enumeration type (Haskell being an interesting exception).  But that seems somewhat unsatisfying, given that we can fit essentially all other kinds of type definitions into the model of instantiating a module.  Another challenge with enumeration types is the representation of their literal values.  In many languages, enumeration literals look like other names, and are considered equivalent to a named constant, or in some cases a parameterless function or constructor.  Overloading of enumeration literals (that is using the same name for a literal in two different enumeration types declared in the same scope) may or may not be supported.

In ParaSail we propose the following model: We define a special syntax for enumerals (enumeration literals), of the form #name (e.g. #true, #false, #red, #green). We define a universal type for enumerals, Univ_Enumeration.  We allow a type to provide conversion routines from/to Univ_Enumeration, identified by operator "from_univ" and operator "to_univ".  If a type has a from_univ operator that converts from Univ_Enumeration, then that type is effectively an enumeration type, analogous to the notion that a type that has a from_univ that converts from Univ_Integer is essentially an integer type.  As with other types, double-bracket notation applied to a value of an enumeration type, e.g. [[enumval]], is equivalent to a call on to_univ(enumval), and produces a result of Univ_Enumeration type.  An additional special Boolean "in" operator which takes one Univ_Enumeration parameter determines which enumerals are values of the type.  The notation "X in T" is equivalent to a call on the operator T::"in"(X).  The precondition on from_univ would generally be {univ in Enum_Type}.

Here is an example:

interface Enum<Enumerals : Vector<Univ_Enumeration>> is
  operator "in"(Univ_Enumeration) -> Boolean<>; 
  operator "from_univ"
    (Univ : Univ_Enumeration {Univ in Enum}) -> Enum;
  operator "to_univ"(Val : Enum) 
    -> Result: Univ_Enumeration { Result in Enum };
  ...
end interface Enum;
...

type Color is Enum<[#red,#green,#blue]>;
var X : Color := #red;  // implicit call on from_univ

Here we presume the class associated with the Enum interface implements "in", "from_univ", and "to_univ" by using the Enumerals vector to create a mapping from Univ_Enumeration to the appropriate value of the Enum type, presuming the enumerals map to sequential integers starting at zero. A more complex interface for creating enumeration types might take such a mapping directly, allowing the associated values to be other than the sequential integers starting at zero. The built-in type Boolean is presumed to be essentially Enum<[#false,#true]>.

So why this model?  One is that it fits nicely with the way that other types with literals are defined in ParaSail, by using from_univ/to_univ.  Secondly, it naturally allows overloading of enumeration literals, in the same way that the types of numeric literals are determined by context.  Finally, it makes a strong lexical distinction between enumeration literals and other names.  This could be considered a bug, but on balance we believe it is useful for literals to stand out from, and not conflict with, normal names of objects, types, operations, and modules.  Note that this model is reminiscent of what is done in Lisp with the quote operator applied to names, e.g. 'foo.  It also borrows from the notation in Scheme of #f and #t for the literals representing false and true.