Isn't the premise a bit wrong? Sure Internet scaled, but with a lot of problems over time. Like any system, obviously, just pointing out that all big systems had big hiccups. Most engineering problems have fixed constraints, but in software those constraints are ever changing.
> However, I am considering an even more general scheme, where it is possible to define what is meant by addition, multiplication, etc., for new datatypes unimagined by the language designer
So, um, like this?
signature RING =
sig
type t
val + : t * t -> t
val * : t * t -> t
val ~ : t -> t
end
> Extensible generic operations are not for the faint of heart. The ability to extend operators after the fact gives both extreme flexibility and ways to make whole new classes of bugs!
This is precisely why parametric polymorphism is superior to ad-hoc polymorphism as a way to enable programs to work in previously unanticipated situations. Don't work with concrete use cases, work with the minimum abstract requirements that allow your program to work!
> On the other hand, some mutations will be extremely valuable. For example, it is possible to extend arithmetic to symbolic quantities.
So, for example, like this?
functor PolynomialRing (R : RING) : RING =
struct
type t = R.t list
fun xs + nil = xs
| nil + ys = ys
| (x :: xs) + (y :: ys) = R.+ (x, y) :: xs + ys
(* define multiplication and negation too... *)
end
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.
> 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.
Indeed. Types are not for proving absolutely everything. The rest you have to prove on your own.
> 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.
There isn't much value in those. Types are for programming automation. The human brain is for general-purpose theorem proving. What is a real pity is that it is difficult to annotate programs with handwritten proofs.
> and of course now you have to do full-blown theorem proving.
[0]: https://vimeo.com/151465912
So, um, like this?
> Extensible generic operations are not for the faint of heart. The ability to extend operators after the fact gives both extreme flexibility and ways to make whole new classes of bugs!This is precisely why parametric polymorphism is superior to ad-hoc polymorphism as a way to enable programs to work in previously unanticipated situations. Don't work with concrete use cases, work with the minimum abstract requirements that allow your program to work!
> On the other hand, some mutations will be extremely valuable. For example, it is possible to extend arithmetic to symbolic quantities.
So, for example, like this?
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.
Indeed. Types are not for proving absolutely everything. The rest you have to prove on your own.
> 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.
There isn't much value in those. Types are for programming automation. The human brain is for general-purpose theorem proving. What is a real pity is that it is difficult to annotate programs with handwritten proofs.
> and of course now you have to do full-blown theorem proving.
You would have to do it regardless.