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) ...