A Circle Package

type CircleWRT2[CircleRep, PointRep] =
  {pointPackage: PointWRT[PointRep],
   mkcircle: (PointRep x Real) $->$ CircleRep,
   center: CircleRep $->$ PointRep, ...}
type CircleWRT1[PointRep] =
   exists CircleRep. CircleWRT2[CircleRep, PointRep]
type Circle = exists PointRep. CircleWRT1[PointRep]
value circleModule: CircleModule =
all[PointRep]
   fun(p: PointWRT[PointRep])
      pack[CircleRep = PointRep x Real
         in CircleWRT2[CircleRep,PointRep]]
     {pointPackage = p,
      mkcircle = fun(m: PointRep, r: Real)(m, r) ...}
value cartesianCirclePackage =
   openCartesianPointPackage as p[Rep] in
      pack[PointRep = Rep in CircleWRT1[PointRep]]
         circleModule[Rep](p)
open cartesian CirclePackage as c[PointRep][CircleRep]
in ...c.mkcircle(c.pointPackage.mkpoint(3, 4), 5) ...