ExpandCollapse

+ 1 Abstract Types in Felix

Felix supports type abstraction with the special operator {_repr_} and constructor {_make_*} where {*} is the type name.

  open module X {
    type pair = new int * int;                                 //public type
    ctor pair(x:int, y:int)=>_make_pair (x,y);                // constructor
    fun first(xy:pair)=>(_repr_ xy).0;                        // projections
    fun second(xy:pair)=>(_repr_ xy).1;
  
    // as string
    fun str(xy:pair)=> 
       "[" + str ((_repr_ xy).0) + "," + str ((_repr_ xy).1)+"]"
    ; 
  }
  
  var xy = pair (1,2);
  println$ str xy, first xy, second xy;

It is more conventional to use a private {struct} for the representation:

  open module X {
    private struct pair_rep { a: int; b: int; };              // private representation
    type pair = new pair_rep;                                 // public type
    ctor pair(x:int, y:int)=>_make_pair (pair_rep (x,y));     // constructor
    fun first(xy:pair)=>(_repr_ xy).a;                        // projections
    fun second(xy:pair)=>(_repr_ xy).b;
  
    // as string
    fun str(xy:pair)=> 
       "[" + str ((_repr_ xy).a) + "," + str ((_repr_ xy).b)+"]"
    ; 
  }
  
  var xy = pair (1,2);
  println$ str xy, first xy, second xy;

The formula for making abstract types is always the same.

The type {pair_rep} is declared private so it is not visible outside the module {X}.

Then the public type {pair} is defined to have that representation using the {type = new} construction.

Now we can define the public functions on the abstract type.

We use {_make_pair} operator to convert the representation {pair_rep} to the abstract type {pair}.

We use the {_repr_} operator to convert the abstract type to its representation {pair_rep}.

The two operators converting between the abstraction and its representation can only be used in the module in which the representation is defined. Outside the module only the public functions accessing the abstraction can be used.

Note that even if the representation is a public type, the conversions still can't be done.