1. 5

Abstract: “Algorithms for solid modeling, i.e., Computer-Aided Design (CAD) and computer graphics, are often specified on real numbers and then implemented with finite-precision arithmetic, such as floating-point. The result is that these implementations do not soundly compute the results that are expected from their specifications.

We present a new library, StoneWorks, that provides sound and robust solid modeling primitives. We implement StoneWorks in MarshallB, a pure functional programming language for exact real arithmetic in which types denote topological spaces and functions denote continuous maps, ensuring that all programs are sound and robust. We developed MarshallB as an extension of the Marshall language.

We also define a new shape representation, compact representation (K-rep), that enables constructions such as Minkowski sum and analyses such as Hausdorff distance that are not possible with traditional representa- tions. K-rep is a nondeterminism monad for describing all the points in a shape.

With our library, language, and representation together, we show that short StoneWorks programs can specify and execute sound and robust solid modeling algorithms and tasks.”


  2. 4

    In MarshallB, types denote topological spaces and functions denote continuous maps, making MarshallB’s semantics a subcategory of Top, the category of topological spaces. A typical problem when working with Top is that we find it hard to make universal statements about all topological spaces, because there are so many surprisingly distinct forms that topological spaces can take. Therefore, we usually want to find a convenient subcategory to work with instead.

    MarshallB uses the category of presheaves over second-countable locally-compact sober topological spaces. “second-countable” is a limitation on how infinite the spaces can be, “locally-compact” is a kind of convenience condition that gives us our internal lambda calculus, and “sober” ensures that we will find points if we go looking for them.

    However, also, a category of presheaves is actually a topos, and every topos has an internal lambda calculus as well. MarshallB operates in this topos, and can lift computations from the convenient category of topological spaces up into the topos.

    The paper cites the essential paper Compiling to Categories. I think that the paper is implicitly endorsing a systematic approach to construction of domain-specific general-purpose programming languages:

    • Define a nice category whose objects and arrows you wish to study and compute
    • Consider the category of presheaves on the nice category
    • Every category of presheaves is a topos, every topos is Cartesian closed, every Cartesian closed category has an internal lambda calculus
    • Lift objects and arrows of interest to the topos
    1. 1

      It’s too deep for me. Looked useful, though. Thanks for thorough description on it. Bookmarking it.