| I don't think that ML-style type systems address the fundamental problem that Sussman is trying to articulate in this note. I'll try to explain. Your definitions of Ring and PolynomialRing are incomplete because neither specifies the appropriate set of axioms. Because you do not specify those axioms, your type signature is underspecified. As Sussman puts it, "It is probably impossible to prove very much about [the] program" (at least, without inspecting the implementation itself). To give a concrete example, the type signatures of Ring and CommutativeRing are the same in System F. And as Sussman puts it, "a program that depends on the commutativity of numerical multiplication will certainly not work correctly for matrices." Now, this doesn't so much matter for human-written code, because us humans will implicitly fill in the details and never pass a mere Ring into an algorithm that expects a CommutativeRing, even if the two types are structurally identical. However, this does matter a lot if you want to use the structures of types (or their programs) to direct automated program mutation/construction. And automated program mutation/construction is exactly the sort of thing that this note is about ("The most robust systems are evolvable"). Of course, there do exist type systems which fix this problem by allowing you to specify the axioms to which a Ring or CommutativeRing must conform. But using those systems is a crap load of work, requires a PhD's worth of effort to become efficient at, and of course now you have to do full-blown theorem proving. Which, IMO, introduce the same "brittleness" that Sussman talks about at the beginning of the essay". Data propagation and decorated values are Sussman's proposed alternative, from what I can tell. So 1) it's true that type theory provides one solution to Sussman's problem. But that type theory is something much more expressive than System F. And 2) given the difficulty of using those systems (eg CIC) in practice, I think Sussman's proposed alternatives are worth seriously considering. |