Go backward to Hiding the Representation Go up to Top Go forward to Quantification and Modules

Another Example

type Point =
   exists PointRep.
     {mkPoint: (Real x Real) -> PointRep,
      x-coord: PointRep -> Real,
      y-coord: PointRep -> Real}

type PointWRT[PointRep] =
  {mkPoint: (Real x Real) -> PointRep,
   x-coord: PointRep -> Real,
   y-coord: PointRep -> Real}

type Point = exists PointRep. PointWRT[PointRep]
value cartesianPointOps =
  {mkpoint = fun(x: Real, y: Real) (x,y),
   x-coord = fun(p: Real x Real) fst(p),
   y-coord = fun(p: Real x Real) snd(p)}
value cartesianPointPackage: Point =
   pack[PointRep = Real x Real
      in PointWRT[PointRep]]
   cartesianPointOps