A colourful density plot, with a yellow-red-purple-black gradient for high error --> low error. The plot is reddish in colour (error 10^-10), with wispy purple curves where the integrator does better (for no good reason), and two curves whose vicinity is yellow (corresponding to families of cubic Béziers with a cusp). There are also some half-disk-like yellow areas where the integrator performs worse, due to the derivative of the speed function having non-real roots that are close to the real axis for such Béziers.

Visualisation of arc-length error for Clenshaw–Curtis quadrature across a parameter space of cubic Béziers with control points at (0,0), (1,0), (x,y), (1,1).

The yellow curves correspond to Béziers with cusps; the disks to nearly real complex roots of the derivative of the speed function.

A collection of plots. Each plot is for a specific cubic Bézier curve (straight line, simple Bézier, Bézier with a cusp, Bézier with a near-cusp, degenerate Bézier). Each plot contains coloured histograms, in which different methods for estimating the arc length are displayed with different colours. Above the x-axis, the histograms show computation time, while below the x-axis they show accuracy of the method, on a log scale. Methods compared: poly-line, Romberg's method, Clenshaw-Curtis, tanh-sinh, Gauss-Legendre and Gravesen. The naive chord-length methods (poly-line and Romberg's method) are predictable but start taking a long time to converge for higher accuracy. Gravesen (which does adaptive refinment) is similarly underwhelming. Clenshaw-Curtis, tanh-sinh, Gauss-Legendre all converge with very high accuracy on simple examples, but struggle in the presence of cusps or near cusps, unless one subdivides at cusps first. With subdivision, tanh-sinh seems to do the best at dealing with difficult Béziers.

Comparison of various methods for computing the arc-length of a selection of cubic Bézier curves.

my bad

Sounds similar to the way the GHC typechecker can promote metavariables to the top-level, e.g. when the monomorphism restriction applies. It's then the notion of type variable levels which avoids these promoted metavariables getting unified with skolems from an inner level.

terminal "everything is a dictionary" brain

there being a grammar of patterns, distinct from expressions, was one of the key "woah" moments for me with Haskell; that idea brings so much else into focus

it seems clear he hasn't had that insight (and certainly not experienced pattern matching in a dependently typed language either)