1. 16
blog.ploeh.dk
1.

2. 3

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.

1. 2

In particular, what of the dependently-typed languages? They require type annotations, a sort of syntactic ceremony, in many situations.

This is true, but not very many people use or are even aware of dependently-typed languages. Idris, Agda and Coq are all very academic research projects that most programmers who aren’t already fairly deeply interested in advanced type theory and PL design haven’t heard of. Haskell and other ML-like languages are less ceremonious compared to Java and C++, which is what most programmers imagine when they think about statically-typed languages.