Go backward to Hidden Data Structures
Go up to Top
Go forward to Combining Universal and Existential Quantification

Hidden Data Types

package point2
   type Point is private;
   function makepoint(x: Real, y: Real) return Point;
   ...
   private
   - - hidden local definition of type Point
end point2;

type Point2 =
   exists Point.
      {makepoint: (Real x Real) -> Point,
         ...}
type Point2WRT[Point] =
      {makepoint: (Real x Real) -> Point,
         ...}
value point2: Point2 = pack[Point = (Real x Real) in
   Point2WRT[Point]] point1


Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: understand.tex,v 1.1 1996/06/12 09:38:21 schreine Exp schreine

Prev Up Next