Predicates and shapes

The predicates geo.contains, geo.within and geo.intersects answer yes-or-no questions about where things are, and geo.centroid and geo.bounding_box give a shape a place for its label and a view that shows it. Here the bakery uses them on its delivery patches, its pins on a map and its shops:

example

type Delivers = Bool {}type InView = Bool {}type WalkingReach = Length {    min: 0metre}/// Whether a customer is inside one of the bakery's patches.function delivers_to(patches: List<Polygon>, customer: Point) -> Delivers {    return Delivers(list.any(patches, patch -> geo.contains(patch, customer)))}/// Whether a van's round passes through a patch.function passes_through(van_round: LineString, patch: Polygon) -> Delivers {    return Delivers(geo.intersects(van_round, patch))}/// Whether a shop's pin is inside the map a person is looking at.function in_view(shop_pin: Point, view: BoundingBox) -> InView {    return InView(geo.within(shop_pin, view))}/// Whether two shops are near enough to walk between.function walkable(from: Point, to: Point, walking_distance: WalkingReach) -> InView {    return InView(geo.within(from, to, distance: walking_distance))}/// Where a patch's name goes on the map.function label_at(patch: Polygon) -> Point {    return geo.centroid(patch)}/// The view that shows a whole patch.function view_of(patch: Polygon) -> BoundingBox {    return geo.bounding_box(patch)}

A customer on a patch's edge is inside it. The patch's northern edge is a great circle, so it bows north past 51.54° N between its corners. A box's sides are parallels and meridians, so the box that shows the whole patch reaches a little further north than its corners:

example

test "a customer on a patch's edge is delivered to" {    var patch: Polygon = Polygon {        outer: [            Point {                latitude: 51.49                longitude: -0.2                altitude: none            },            Point {                latitude: 51.49                longitude: -0.05                altitude: none            },            Point {                latitude: 51.54                longitude: -0.05                altitude: none            },            Point {                latitude: 51.54                longitude: -0.2                altitude: none            },            Point {                latitude: 51.49                longitude: -0.2                altitude: none            }        ]        holes: []    }    var big_ben: Point = Point {        latitude: 51.5007        longitude: -0.1246        altitude: none    }    var on_the_edge: Point = Point {        latitude: 51.5        longitude: -0.2        altitude: none    }    var eiffel_tower: Point = Point {        latitude: 48.8566        longitude: 2.3522        altitude: none    }    assert delivers_to([patch], big_ben)    assert delivers_to([patch], on_the_edge)    assert not delivers_to([patch], eiffel_tower)    assert in_view(big_ben, view_of(patch))    assert not in_view(eiffel_tower, view_of(patch))    assert walkable(big_ben, on_the_edge, 6km)    assert not walkable(big_ben, on_the_edge, 5km)}test "a patch's label and the view that shows it" {    var patch: Polygon = Polygon {        outer: [            Point {                latitude: 51.49                longitude: -0.2                altitude: none            },            Point {                latitude: 51.49                longitude: -0.05                altitude: none            },            Point {                latitude: 51.54                longitude: -0.05                altitude: none            },            Point {                latitude: 51.54                longitude: -0.2                altitude: none            },            Point {                latitude: 51.49                longitude: -0.2                altitude: none            }        ]        holes: []    }    assert label_at(patch).latitude == 51.51501933808094    assert label_at(patch).longitude == -0.12499999998684845    assert view_of(patch).north == 51.54002390691161    assert view_of(patch).south == 51.49}

Polygons are valid when built

Jadpo checks every polygon when it is built or read, so no operation, query or other system ever meets one whose edges cross. A Polygon is valid when, on the sphere:

each ring is closed, with four points or more;
no ring crosses or touches itself, except where its last point meets its first. A point repeated in a row, or a ring that turns straight back along an edge, touches itself;
each hole lies inside the outer ring, and no two rings cross, overlap or share even one point. The OGC standard lets a hole touch the outer ring at one point; Jadpo doesn't, which also keeps a polygon's inside in one piece without a check of its own;
every edge is shorter than half the globe (180° of arc), so the great circle it follows is the only one;
the polygon covers less than half the globe. PostGIS's geography reads a ring wound either way as the same, smaller area (verified), so a ring meant to enclose the larger side couldn't be stored as meant.

A ring's inside is its smaller side, as PostGIS reads it, whichever way the ring is wound. Jadpo picks the smaller side from the ring's area on the sphere, added up by Van Oosterom and Strackee's formula in its whole numbers. The choice is exact unless the two sides are within about 10⁻³⁵ of each other. A ring that lies exactly on one great circle, so both sides are equal, breaks the rule. A MultiPolygon has no rule of its own: each of its polygons is valid, and they may overlap.

A polygon read from GeoJSON or WKT that isn't valid is refused, format at the ring's place, as the standard library's other checks on reading are (Every boundary through the contract). A polygon built in code that isn't valid breaks a named rule, rings_valid, which you map like any rule across fields (Rules across fields).

Checking takes time in proportion to about n log n of the points, since it sweeps over the edges: 0.6 ms for 100 points, 6.8 ms for 1,000 and 68 ms for a country's outline of 10,000 (measured natively on an Apple M1 Pro).

Altitudes are all or nothing

Every position in one geometry has an altitude, or none does. WKT can't write a mix, and PostGIS refuses one ("can not mix dimensionality in a geometry", verified), so a geometry that mixed them couldn't be stored or exchanged. A Point has one position, so it always agrees. A multi-geometry's parts must agree with each other.

A mixed geometry read from GeoJSON or WKT is refused, format at the first position of the other size. One built in code breaks a named rule, altitudes_agree, which you map as you map rings_valid.

Reading. GeoJSON is checked once the whole geometry is read, every position in the order written, and refused format at the first of the other size (coordinates.1.0.2). A multi-geometry's parts are checked against each other. WKT's reader refuses a mix at that position too, as malformed, its one condition for text that isn't a geometry.
What a literal decides. altitudes_agree reads each Point written out in a geometry literal, however deep: a line's points, a polygon's rings, a multi-polygon's polygons. An altitude written none is none. One written out, or of a type that can't be none (a distance), is one. Anything else, such as a point or a list held in a variable, is known only when the program runs. If some positions are known to have an altitude and others known to have none, the literal is type.invalid_literal at the part holding the first of the other size, whatever else is unknown. Otherwise the literal is attempted, as it is for rings_valid. So a line from points held in variables is attempted, even when each variable holds a literal: the checker doesn't follow a variable's value, here or for rings_valid.
A polygon's rules in order. rings_valid is checked first, then altitudes_agree, so a literal or a value that breaks both names rings_valid. GeoJSON and WKT likewise check a ring before the positions' sizes.
Nothing later meets a mix. Storage stores every geometry without checking it again, and geo.to_wkt never meets a geometry it can't write. A mixed geometry that somehow got past every check is the runtime's "value of a kind the checker would have refused". The PostgreSQL driver refuses to encode a shape that mixes them, since EWKB's type flag covers the whole geometry. Each geometry's examples under Geospatial types hold every point at a height or none, and its refused examples include a mix.

A polygon built from values known only when the program runs is attempted, and you map both rules:

example

type NotAPatch = Failure {    kind: FailureKind.invalid_value}/// A patch from the corners a planner clicked, back to the first.function patch_from(clicked: List<Point>, first: Point) fails NotAPatch -> Polygon {    return attempt Polygon {        outer: list.append(clicked, first)        holes: []    } {        rings_valid: NotAPatch  // edges that cross, or a corner clicked twice        altitudes_agree: NotAPatch  // corners at a height and on the ground    }}

example

test "a patch whose edges cross isn't one" {    var bow_start: Point = Point {        latitude: 0.0        longitude: 0.0        altitude: none    }    var bow_tie: List<Point> = [        bow_start,        Point {            latitude: 10.0            longitude: 10.0            altitude: none        },        Point {            latitude: 10.0            longitude: 0.0            altitude: none        },        Point {            latitude: 0.0            longitude: 10.0            altitude: none        }    ]    assert patch_from(bow_tie, bow_start) fails NotAPatch}test "a patch with one corner at a height isn't one" {    var corner: Point = Point {        latitude: 0.0        longitude: 0.0        altitude: none    }    var clicked: List<Point> = [        corner,        Point {            latitude: 0.0            longitude: 1.0            altitude: 35metre        },        Point {            latitude: 1.0            longitude: 1.0            altitude: none        }    ]    assert patch_from(clicked, corner) fails NotAPatch}

A polygon written out is checked while compiling:

example

/// The patch a planner drew, its edges crossing.function drawn_patch() -> Polygon {    return Polygon {        outer: [            Point {                latitude: 51.49                longitude: -0.2                altitude: none            },            Point {                latitude: 51.54                longitude: -0.05                altitude: none            },            Point {                latitude: 51.49                longitude: -0.05                altitude: none            },            Point {                latitude: 51.54                longitude: -0.2                altitude: none            },            Point {                latitude: 51.49                longitude: -0.2                altitude: none            }        ]        holes: []    }}

text

error: This `Polygon` breaks its rule `rings_valid` --> main.jadpo:4:16  |4 |         outer: [  |                ^ these rings don't make a valid polygon  reason: A `Polygon`'s rings are closed with four points or more, never cross or meet themselves or each other, keep each hole inside the outer ring, and have every edge shorter than half the globe, so the polygon is the smaller side its outer ring bounds (area 20, "Polygons are valid when built"). A literal is checked while compiling.  next: Close each ring and move its points so no edge meets another, with each hole inside the outer ring (agent)  rule: type.invalid_literal  help: https://jadpo.dev/docs/errors/type.invalid_literalcheck failed: 1 error, 1 file

Polygons are valid when built

Altitudes are all or nothing

Related