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