I am skeptical of the topology of the diagram provided. In particular, what of the dependently-typed languages? They require type annotations, a sort of syntactic ceremony, in many situations. It is tempting to imagine Idris, Agda, and Coq as being to the far right of the diagram, but I think that they are actually in an orthogonal dimension entirely, because there are similar dependently-typed ceremonies in dynamically-typed languages too.

I will ignore the deliberately poor encoding of consume, and instead go directly to showing off levels of type-like ceremony within a single dynamically-typed language. In Monte:

def consume(xs, i) { return xs.slice(i, xs.size()) }

Minimal ceremony. Uses def sugar to give a name to an object with a single "run" method taking two arguments. How would we ensure that i is a valid slice index? With a type annotation:

def consume(xs, i :Int) { return xs.slice(i, xs.size()) }

Not valid enough; slice indices ought to be non-negative.

def consume(xs, i :(Int >= 0)) { return xs.slice(i, xs.size()) }

We can now sacrifice some polymorphism. First, let’s limit ourselves only to lists, and not to other sliceable sequence types like strings. We’ll also add a return type.

def consume(xs :List, i :(Int >= 0)) :List { return xs.slice(i, xs.size()) }

And finally we’ll pretend to have a Dreaded Monomorphism Restriction and require lists of integers:

def consume(xs :List[Int], i :(Int >= 0)) :List[Int] { return xs.slice(i, xs.size()) }

This is where Monte stops; we aren’t able to do such fun things as guess the type of the input list in a way that would allow us to write out the List[G] guard generically. We could certainly ask our caller to choose a guard; or, even better, have two callers, one who chooses the guard and one who fulfills its requirements:

def makeConsume(G :DeepFrozen):
    def lg := List[G]
    return def consume(xs :lg, i :(Int >= 0)) :lg { return xs.slice(i, xs.size()) }

On a closing note, the author chose F♯ and Haskell, which are both MLs, to talk about lack of ceremony. I think that the common feature of MLs being lauded here is implicit type inference.