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:
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.
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.
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:
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.
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.
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:Minimal ceremony. Uses
def
sugar to give a name to an object with a single"run"
method taking two arguments. How would we ensure thati
is a valid slice index? With a type annotation:Not valid enough; slice indices ought to be non-negative.
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.
And finally we’ll pretend to have a Dreaded Monomorphism Restriction and require lists of integers:
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: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.
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.