Lambda the Ultimate

Correct me if I'm wrong, but Magpie's solution requires a whole-program analysis. This is definitely still a useful feature, but most treatments of the expression problem require modular checking, so Magpie isn't solving the quite same problem (unless I misunderstand, of course).

Magpie is semantically squirrely compared to a lot of other languages. I don't think it requires whole program analyis for some definition of "whole program", but it will require executing the top-level definitions before it does the static checking.

It's possible to execute some code (which defines things in global scope), statically check what's there, and then execute some more code which defines even more stuff globally.

but most treatments of the expression problem require modular checking, so Magpie isn't solving the quite same problem

No, I think you're right. Magpie doesn't separately compile (it doesn't compile at all), so it definitely doesn't solve it according to Wadler's strict definition. It addresses the subset of the expression that I care about, though:

• New datatypes can be added, in any place in the program text that you like (i.e. you don't have to edit the one special file that defines your algebraic type).
• New operations can be added, in any place in the program text that you like (i.e. you don't have to edit the one special file that defines a class and all of its methods).
• It will statically check that all datatypes support all required operations.

Dynamic languages tend to give you the first two pretty easily, which is how Magpie does it. It's a bit unusual in that it can also do the last one.

I believe it makes sense. Even in a dynamically typed language, I can make choices between structural pattern-matching vs. passing interfaces (such as records of functions). If I favor the former, it can be difficult to add new structures (since I'd need to tweak every function in every module that matches on the structure). If I favor the latter, it can be difficult to extend the operators in the record in any significant way (since I may need to find constructors scattered throughout code).

Many essential elements of the expression problem still exist. Even though static type safety was mentioned by Philip Wadler when he coined the term, I don't believe that is nearly so essential to the expression problem.

I think static type safety is essential to what makes the expression problem difficult. Wadler coined the term as [1]:

The Expression Problem is a new name for an old problem. The goal is to define a datatype by cases, where one can add new cases to the datatype and new functions over the datatype, without recompiling existing code, and while retaining static type safety (e.g., no casts).

(I think "without recompiling existing code" means modular type checking -- the other thing that makes it a hard problem.)

[1] http://www.daimi.au.dk/~madst/tool/papers/expression.txt

In my own language design, the expression problem is difficult due to my aim to support open modularity, object capability model security, live upgrade, and other interesting properties. I chose, eventually, to not bother solving it and instead to support a few simplistic extensibility properties for data types and recursive functions. Static type safety is not essential to making the expression problem more difficult; it's simply what made the problem a difficult one for Wadler.

Even without those constraints, the expression problem isn't a trivial one. It still requires more than a little thought about how data and operations are expressed and composed in the language.

I don't think static typing is essential to making the expression problem more difficult. It's just that "the expression problem" is defined to require static and modular checking. When someone says they have "a solution to the expression problem", I expect something that fits the definition.

But maybe my being a megafan of static and modular checking has introduced some bias... Is it more common to use term "the expression problem" for just the first part of Wadler's definition (extending the types and operations independently)?

Since you're attempting to pick nits with the definition, I'll point out that Wadler never actually defined the problem. He only stated his goals, mentioned four prior discussions of the problem in order to note that it is an 'old' problem, and intuited the problem with the following:

One can think of cases as rows and functions as columns in a table. In a functional language, the rows are fixed (cases in a datatype declaration) but it is easy to add new columns (functions). In an object-oriented language, the columns are fixed (methods in a class declaration) but it is easy to add new rows (subclasses). We want to make it easy to add either rows or columns.

When someone is talking about 'The Expression Problem', this rows and columns intuition is the essence of what they are discussing.

Static typing and modularity are goals - additional constraints that prohibit some solutions to the problem. And those are just the goals he mentioned. Implicit goals would include decidability and performance of the dispatch mechanism, which are reasons that mechanisms such as predicate dispatch have never succeeded.

This is, at least, how I have always understood the problem. The OP title here suggests I'm not unique in this position.

If you toss static checking out the window (i.e. statically ensuring every cell in each row and column is filled in), doesn't pretty much every dynamic language let you solve this?

In Ruby, I can pass objects of arbitrary types to methods, so adding new datatypes is easy: just make a new class. Likewise, classes are open so I can just add new methods to existing classes. It isn't idiomatic, but Python supports both of those too. Or am I missing something?

Your 'pretty much every dynamic language' seems to be a teeny tiny subset of dynamic languages. The two you mention - Python and Ruby - are pretty much the same language fighting butter battle.

Perhaps try Erlang, E, Oz, Forth...

Pervasive mutability and ambient authority are not implied by dynamic typing. Nor are 'classes' and OO.

Sorry, I should have said "dynamic OOP language". For me, that includes Ruby, Python, Javascript (ECMAScript, ActionScript), Smalltalk, Io, et. al.

It should also include MOO, Lua, E, Newspeak.

In any case, I suppose you could make the 'extend the class' idea work if you have nominative typing, mutable classes, ambient authority to them, the ability to execute code in a module's toplevel, and ability to control namespace collisions. That's true of at least an important subset of OOP languages. I've seen variants on the idea that use declarative extensions for statically typed languages (horizontal subclassing) but I can't actually remember from where.

In Python, Ruby et al, two methods added by different parties that have the same name will clash. That's one of the reasons the technique has earned the moniker "monkey patching". Chris discusses this in his talk.

There are modular solutions to open classes. For example, Jiazzi (OOPSLA 2001) handles the method-by-different parties just fine via automatic renaming. Scheme units, which Jiazzi is based on, also support this, though it doesn't integrate with objects enough to require renaming.

Re: comment-63026.

In Worlds: Controlling the Scope of Side Effects (a VPRI paper), Alan Kay and Alex Warth agree with your sentiment (who wouldn't?):

Monkey-patching is a bad idea: in addition to polluting the interfaces of the objects involved, it makes programs vulnerable to name clashes that are impossible to avoid. Certain module systems, including those of MultiJava and eJava, eliminate these problems by allowing programmers to declare lexically-scoped extension methods. These must be explicitly imported by the parts of an application that wish to use them, and are invisible to the rest of the application.

… worlds can be used to support this kind of modularity …

What are worlds?

The world is a new language construct that reifies the notion of program state. All computation takes place inside a world, which captures all of the side effects — changes to global, local, and instance variables, arrays, etc. — that happen inside it.

A new world can be “sprouted” from an existing world at will. The state of a child world is derived from the state of its parent, but the side effects that happen inside the child do not affect the parent. (This is analogous to the semantics of delegation in prototype-based languages with copy-on-write slots.) At any time, the side effects captured in the child world can be propagated to its parent via a commit operation.

In closing, Kay and also “believe that worlds can greatly simplify the management of state in backtracking programming languages such as Prolog and OMeta.”

Maybe somebody should tell him that this very idea has already been implemented more than 15 years ago, under the name of "computation spaces" -- it is the main mechanism with which the constraint programming language Oz realises programmable search.

Yes, computation spaces are related and they probably should have cited it.

But then again, Tanter probably "should've" cited computation spaces in his Contextual Values proposal.

But Alan is not necessarily shooting for "oh, we'll use computation spaces". He is re-branding things presumably deliberately as part of his FONC project so that he has a marketing pamphlet for his real agenda.

Alan doesn't really have a need to jump on somebody else's hot research buzzword, either, like some have done with topics like "functional reactive programming".

Are Worlds, computation spaces, and first-class environments in something like MIT Scheme variations of the same idea?

⨯-reference to an earlier LtU thread: First-class environments.

A quote from the MIT Scheme Manual:

Environments are first-class objects in MIT/GNU Scheme. An environment consists of some bindings and possibly a parent environment, from which other bindings are inherited. The operations in this section reveal the frame-like structure of environments by permitting you to examine the bindings of a particular environment separately from those of its parent.

Alessandro's 123-page Ph.D. dissertation Experimenting with Programming Languages (a.k.a. VPRI Technical Report TR-2008-003) is an extended version of the worlds paper. It seems to mention neither Oz/computation-spaces nor MIT Scheme.

AFAICT first-class environments are a different story.

Not really. First-class environments are their own topic unto themselves. They weren't invented for backtracking, either. I can see how you drew the analogy though.

I'll point out that Wadler never actually defined the problem.

If Phil could comment on this, I believe that the post often introduced as his first on the expression problem is not actually the first one. I believe he has an earlier post somewhere else where he is in a conversation with someone, a practitioner I think, and the guy is explaining to Phil a modeling problem he has. I believe this was the original inspiration for Phil's java-genericity mailing list posting, but Phil would need to confirm - I could be forgetful.

Edit: Some digging turned up a Kim Bruce paper with a reference to a later posting by Wadler on the Java-Genericity mailing list titled "The expression problem: a retraction". Given the way Wadler names papers, I don't know if this is a play on words or is along the lines of what I was thinking of.

I agree with you that the Expression Problem isn't trivial in dynamically typed languages, but it was also solved long ago with multiple dispatch. I think assuring the safety and consistency of these extensions was always the hardest part, and multiple dispatch didn't meet that criteria until recently.

MD is not a solution for dynamically typed languages in general.

For example, E language and Erlang are dynamically typed, but MD is not be a viable solution for those languages because MD has never been reconciled with the object capability model or distributed programming. (I doubt it ever will be.)

Multiple dispatch is a potential solution, but it simply depends upon your other language constraints. Static assurance of type and memory safety is just one possible language constraint among many that could hinder a solution to the expression problem.

Any suggestions on reading to get started on the relationship between MD and these other things that you doubt it will ever be reconciled with? (I'm interested because, some years back, I had some thoughts on dynamic multiple dispatch, but set them aside to concentrate on fexprs.)

I've not seen any papers on the subject specifically (MD + ocap or MD + distribution).

If you're interested in ocap/distribution and expression problem, I've been focusing my attention more towards plug-in architectures, especially the 'pluggable factory' patterns (John Vlissides [98,99], Timothy Culp [99]).

May be relevant: Prototypes with Multiple Dispatch: An Expressive and Dynamic Object Model.

Re: comment-62959: How does that even make sense in a dynamically typed language like Clojure?

An LtU member much respected in the Clojure community explained how the expression problem pertains to Clojure a year ago:

So, with definterface, deftype, and reify you have a very clean way to specify and implement a subset of the Java/C# polymorphism model, that subset which I find clean and reasonable, with an expectation of portability, and performance exactly equivalent to the same features on the host.

I could have stopped there, and almost did. But there are three aspects of that polymorphism model that aren't sufficient for Clojure:

1. It is insufficiently dynamic. […]
2. […] performance
3. It is ‘closed’ polymorphism, i.e. the set of things a type can do is fixed at the definition time of the type. This results in the ‘expression problem’, in this case the inability to extend types with new capabilities/functions.

We've all experienced the expression problem — sometimes you simply can't request/require that some type implement YourInterface in order to play nicely with your design. You can see this in Clojure's implementation as well — RT.count/seq/get etc all try to use Clojure's abstraction interface first, but then have hand-written clauses for types (e.g. String) that couldn't be retrofitted with the interface.

Multimethods, OTOH, don't suffer from this problem. But it is difficult to get something as generic as Clojure's multimethods to compete with interface dispatch in Java. Also, multimethods are kind of atomic, often you need a set of them to completely specify an abstraction. Finally, multimethods are a good story for the Clojure side of an abstraction, but should you define a valuable abstraction and useful code in Clojure and want to enable extension or interoperation from Java or other JVM langs, what's the recipe?

R. B. Findler and M. Flatt. Modular object-oriented programming with units and mixins. In Proceedings of the third ACM SIGPLAN international conference on Functional programming, pages 94–104. ACM Press, 1998

Findler and Flatt refer to the problem as The Extensibility Problem, whereas Wadler refers to it as The Expression Problem. The solutions are quite different, but they are clearly discussing the same modeling challenge. Findler and Flatt use MzScheme. Classes and objects in MzScheme are dynamically typed.

Also, from ECOOP 1998:

Krishnamurthi, Shriram, Felleisen, Matthias and Friedman, Daniel P. Synthesizing Object-Oriented and Functional Design to Promote Re-Use. In ECOOP’98 — Object-Oriented Programming , Vol. 1445 (1998), pp. 91-113.

which focuses on a more acute issue of an Extensible Visitor pattern, which one would expect the general formulation of the Expression Problem / Extensibility Problem to handle safely. This paper discusses Zodiac, which is basically a front-end for a DrScheme language level. I believe this was the first paper to advocate the usage of OO design patterns in the context of datatype generic programming, making OO design patterns more robust by adding more modeling facilities to them beyond plain vanilla OO.

This is simply based on my reading experience with the literature, going back and reading these old papers. I was 14 when they were published, and read them towards the end of undergrad. I am also a practitioner with not much formal training in programming languages, but I am curious why you preclude dynamic languages from participating in the expression problem challenge?

Wadler's original -

I know of no widely-used language that solves The Expression Problem while satisfying the constraints of independent compilation and static typing.

- implies that the expression problem and the static typing constraints are two different things.

Note that neither Chris nor I claim any novelty for Clojure's approach. But it is a concern for dynamic languages, as many of them do not provide a viable solution.

Yeah, I saw that sentence after taking a closer look at his full message. The first paragraph make me think he defined the problem to include independent compilation and static typing, while the sentence quoted above implies differently.

IIRC, you have objects, generic functions and multimethods. Doesn't that just flat-out solve the expression problem for you? The only problem that I can think of is that generic functions in CLOS or Dylan kind of live in a big unstructured soup, but didn't you put in protocols to structure interfaces?

(I have only read about Clojure, but never programmed with it, so apologies if my questions are naive.)

Fast dispatch on just class for protocols and multi-methods as the more general polymorphic solution?

here, where he quotes Rich Hickey coyly as "an LtU member".

It's not Clojure concern specifically, but one dynamic language users in general should consider.

IIRC, you have objects, generic functions and multimethods. Doesn't that just flat-out solve the expression problem for you?

Yes, definitely. Protocols just structure interfaces as you say, circumscribe dispatch in a way that makes them easier to optimize, and provide a bridge to the host - i.e. Java authors looking to participate in a Clojure protocol can simply implement its mirror (Java) interface (subject to the type intrusion that involves, to which they are inured). Finally, a protocol implementation can be supplied as a simple map data structure, and thus they support inheritance-free implementation mixin and composition using ordinary runtime code.

Wadler's original [...] implies that the expression problem and the static typing constraints are two different things.

I think I figured out why Martin Odersky is objecting here. I dug up a paper written by Zenger and him that kind of redefined the expression problem to mean the definition he gave here in this LtU thread.

See: Zenger, M. and Odersky, M. Independently Extensible Solutions to the Expression Problem

For this paper, we paraphrase the problem in the following way: Suppose we have a datatype which is defined by a set of cases and we have processors which operate on this datatype. There are primarily two directions along which we can extend such a system:

• The extension of the datatype with new data variants,
• The addition of new processors.

We require that processors handle only a finite number of data variants and thus do not provide defaults which could handle arbitrary cases of future extensions. The challenge is now to find an implementation technique which satisfies the following list of requirements:

• Extensibility in both dimensions: It should be possible to add new data variants and adapt existing operations accordingly. Furthermore, it should be possible to introduce new processors.
• Strong static type safety: It should be impossible to apply a processor to a data variant which it cannot handle.
• No modification or duplication: Existing code should neither be modified nor duplicated.
• Separate compilation: Compiling datatype extensions or adding new processors should not encompass retypechecking the original datatype or existing processors.

We add to this list the following criterion:

• Independent extensibility: It should be possible to combine independently developed extensions so that they can be used jointly [21].

So there you have it. What Martin was really saying was go read his tech report (and probably others he has written on the same subject)! It is a good paper, so I find nothing wrong with this implicit suggestion. However, I think he is projecting his own (good set of) criteria on top of the expression problem.

Finally, I take the comment "we require that processors handle only a finite number of data variants and thus do not provide defaults which could handle arbitrary cases of future extensions" to rule out the use of reflective towers and meta-object protocols.

No I'm only referring to what Phil Wadler wrote. My own paper goes further than this in the demand for independent extensions, but I did not want to bring that up here. I maintain that Wadler wrote quite clearly that static, modular type checking is a necessary criterion for the expressiveness problem. When he refers to "independent compilation" he means modular cheching, which implicitly assumes static checking.

That said, I do not doubt that the problem of independent extensions is a real one also in dynamically typed languages. But we should call it something else.

Note that if we do not need to reject missing combinations statically, a Scala solution to the "extensibility problem" becomes much simpler than the solutions we presented back then: Just use pattern matches with default clauses and chain them with trait composition.

So, the expression problem is the problem of solving another, unnamed problem, while satisfying the constraints of static typing? It seems a not very useful term then, and implies that every problem will need two names - the name for the actual problem and the name for the problem of solving that problem while satisfying type system constraints. Bleh.

The problem is one of modular reasoning: given everything that I should know about the context (everything that is not encapsulated), can I know what will work and not work in that context. An example of a technique that promotes modular reasoning in a dynamic language are hygienic macros. Of course the expression problem can occur...problems with monkey patching are definitely in the same genre as problems with separate type checking in a static language; the phase is just different. Our inability to connect the problems is just a lack of familiarity with the other side of the fence.

I agree that the original name is not ideal; other people have argued that already. But the core (i.e., the hard part) of Wadler's ``expression problem'' (or whatever you choose to name it) was to exclude unhandled combinations of operations and data variants. And do that at compile-time, of course, because otherwise the problem is trivial: just throw a "MethodNotFound" exception.

So I would argue that this particular problem does not have a straightforward translation to DLs.

After looking at the presentation, I am not sure Clojure can be called a dynamic language anymore. An enormous proportion of the talk seemed to be dealing with the intricacies of the JVM (and essentially Java) semantics of the language.

To me, it seemed you need to be a Java expert, and have most of the semantics of that language in your head, to use Clojure. For me, that took away a lot of the appeal of it. At least Lisp is clear in being Lisp, and Java is clear in being Java, not sure I would like to use a hybrid like this.

To me, the feeling the talk left behind is that they just inherited the expression problem from the strongly typed semantics of Java.

as much as i love Scala and Clojure and Gosu and et. al., it really pains me to see how terribly leaky the abstractions really are. please, LLVM, save us all!

The expression problem is indeed easily solved with multimethods or predicate dispatch in a dynamic language. The problem Clojure is dealing with is a bit harder though: they don't just want to extend their own stuff, but also existing Java stuff. Granted, that's not really the traditional expression problem anymore.

I'm mystified. The expression problem is about adding data variants and operations to a system while statically ensuring that all operations can deal with all variants. How does that even make sense in a dynamically typed language like Clojure?

The way I look at it, every interesting problem about static analysis of programs is likely to be of interest in the context of dynamically typed languages. It's directly of interest as part of a more general problem of broad interest:

Given any static language, S, and dynamic language, D, we can ask whether there is a trivial translation of S programs into D with a proof-preserving property. For example, if it can be statically proved that the type of a certain expression in S is T, the question is does D make it possible to prove the translated expression S' has type T'?

There are practical reasons we care about that. For example, if an S into D program translation is proof preserving, then the D compiler can use an S compiler to compile the subset of D which is in the range of the translation function.

Conversely, it is a weakness of the design of D (vis a vis a general purpose language) if programs in S *can not* reasonably be translated to D in a proof-preserving way. All popular dynamic languages that I know of suffer from this weakness but to varying degrees as a practical matter.

The context of a dynamic language makes problems of static analysis harder - not less important:

In the first place, the problems are harder because the language D must permit some easy proof-preserving translation from S. That's hard enough but it gets worse:

A program translated from S to D must not merely be proof-preserving but also must "fit in nicely" alongside other D code that isn't translated from S. I don't know how to define "fit in nicely" but I know its absence when I see it.

The Clojure talk describes expression problem solutions which work in Clojure and interact with other Java code in interesting ways. Statically checked Java code interacts soundly with dynamically constructed classes and protocols, especially. The talk observes that semantically, from the Clojure-side, classes and protocols are essentially a redundant form of a subset of multi-methods -- but they are handy because of how they interact with Java the language and [some] JIT compilers.

So, in terms of the dynamic vs. static question:

The static language S is Java.

In the case of Clojure, for this analysis, we could just define D to be "Java + Clojure". Then every S program translates trivially (by identity) to a D program.

To that, Clojure first adds multi-methods and (to some extent) solves the extension problem in a very general way. There are two drawbacks, though. First, dispatch is not as fast as one might sometimes like. Second, the new functions and types don't interact very interestingly with code in the "S" sub-language.

Thus, Clojure adds "protocols" based on Java classes. Statically compiled, type-checked code can do more interesting things with protocol-based interfaces. To a limited extent (in a somewhat common case) a JIT (the talk says) can use the assumptions from static type checking to heavily optimize Clojure protocol use -- and JITs could likely do better on other cases with minor changes.

The talk makes a "fits in well" case for both multi-methods and protocols along the way.

The property you describe is called full abstraction, and is formalised in terms of program equivalences. Specifically, a translation or embedding T from a language A into another language B is fully abstract if it is equivalence-preserving (if a1 ~ a2 in A then T(a1) ~ T(a2) in B), and also equivalence-reflecting (if T(a1) ~ T(a2) in B then a1 ~ a2 in A). Where ~ denotes observational equivalence under all possible program context of the respective language.

Note that this property is entirely orthogonal to any typed/untyped distinction. However, in contrast to what you said, it is actually harder to achieve and prove full abstraction for typed languages, because of the stronger invariants and abstraction properties that the type system induces in the source language (and which have to be maintained by the translation).

Also, it is well-known that the translation from Java into the JVM is not fully abstract (which arguably means that Java is broken). Whether the "evil" contexts are produced by hand or other compilers is irrelevant.

I'm afraid I don't follow what all this has to do with the expression problem, though. Likewise, I would be very surprised if the compilation of Clojure actually was fully abstract, protocols and other interop features notwithstanding.

No, "full abstraction" is a far stronger relation than I am talking about. Given program a1 in static language S, I identify some finite and context-specific set of proofs about program a1. Those proofs are the essence of why I like the static constraints of S: they help the compiler optimize; they give good error messages for certain kinds of bug....

For T(a1), I *only* want a simple translation of those particular proofs. I don't care about other proofs. I don't care about the details of S that aren't part of how S's type system is of value to me. So, "observational equivalence" is far too strong a demand.

This has to do with the Clojure discussion because someone asked how the expression problem (in the static type checking form) could possibly be of non-trivial interest to a dynamic language like clojure. In the couple of messages here, I explained how (in my view, which I think in this instance is at least ok.).

Hm, OK, I think I understand what you have in mind. However, lack of full abstraction often means that you can break basic semantic properties of the source language. In the face of that, I doubt that you will typically find many interesting properties that still carry over.

Re: comment-63086

What would be a good introduction to this? Protection in Programming-Language Translations by Martín Abadi or some such?

My introduction was Securing the .NET Programming Model, and Joe-E. The references in those papers should suffice, though I do believe you've identified the original paper.

The concept of full abstraction originally came up in denotational semantics, and AFAIK, a 1975 paper by Plotkin would be the original source. But probably not the best introduction...

Curien's Definability and Full Abstraction may be more approchable if you focus on section 2 and gloss over the bits about the historical quest for a fully abstract PCF model.

AFAIC, I found the Full Abstraction Factory's short introduction pretty useful as well, before learning more on it in the context of the May Testing semantics, for instance.

Definitely tangent but I hope not totally off-topic:

Re: this kind of statement for instance (that I don't disagree with, but I'm more interested in the relation with its ontological foundations, rather than just it's truth or falsehood):

Note that this [full abstraction] property is entirely orthogonal to any typed/untyped distinction. However, in contrast to what you said, it is actually harder to achieve and prove full abstraction for typed languages, because of the stronger invariants and abstraction properties that the type system induces in the source language (and which have to be maintained by the translation).
Also, it is well-known that the translation from Java into the JVM is not fully abstract (which arguably means that Java is broken). Whether the "evil" contexts are produced by hand or other compilers is irrelevant.

(emphasis mine)

I intend to develop/define more rigorously my own formalism (I've alluded to, before, though slightly differently) to help my reflections on this type of ideas (proofs, compiled or interpreted program executions, human reasoning over T.Ms or over alike formal systems, persisted program compilations, etc).

More specifically, how that relates to the design processes (occurring in our brains) we follow when building upon legacy Turing complete languages or programs/models translations via other programs (translators) expressed in Turing complete languages, again.

I am still working (in my way too rare spare time) on devising a practical enough ontology I want as a source and target (but that I already suspect will likely include such notions as "intent" and "purpose") even before I attempt to define further the well-formedness rules, of course.

Here's a raw primer of my intuition:

   ?    "T-0"    *             ?      T      !
          T      ?      T      !      1        (T : an arbitrary formal system/theory)
                        1

   ?    "T-0"    *             ?      T      *
          T      ?      T      *      0
                        0

   ?   "ZFC-0"   *             ?    ZFC/G    *
          G      ?      G      *      x        (G : Godel's)
                        1

   ?    "N-0"    *             ?    N/ZFC    *
         ZFC     ?    ZFC/G    *      x        (ZFC : Zermelo Fraenkel + Choice)
                        1

   ?   "T.M-0"   *             ?    T.M/N    *
          N      ?    N/ZFC    *      x        (N : an artifact of ZFC set theory, e.g.,
                        1                       the natural numbers,
                                                constructed from ZFC's empty set alone)

   ?  ["x86-0"]  *             ?  ["x86"/N]  *
          N      ?    N/ZFC    *      x
                        1

   ?  ["I L-0"]  *             ? ["I L"/x86] *
         x86     ?    x86/N    *      x
                        1

   ?  ["n=>n!"]  *             ?["n=>n!"/I L]* (n=>n! is just the factorial example)
         I L     ?   I L/x86   *      x
                        1

   ?  ["n=>n!"]  *             ?  ["n=>n!"]  *
         C #     ?   C #/x86   *     I L
                        1

   ?    ["5"]    *             ?   ["120"]   *
          N      ?  n=>n!/I L  *      N
                        1

etc, etc, along with the usual T-diagram "algebra" and
its basic "bootstrapping operator":

"[fact.cs](leg lang.) => [csc.exe] ( ?(input) )"

allowing, if denoted by "(...)", e.g.:

? [fact.exe] * =  ?(input) [csc.exe] * ( ? [fact.cs] * )
      x86                   x86             C #(leg lang.)

Where:

* the inspiration comes from the Tombstone diagrams, if only regarding the role of the leg of the "T";

* enclosing double quotes denote some serialized/serializable representation, be it on paper, or in a computer byte stream, etc ("given" phrases, in the leg's formalism/language);

* (given/input) axiomatics of new formal system being designed or pre-existing written programs being considered (as the "given") appear on the left;

* legacy formal systems (assumed incomplete but consistent) or translators/machines appear in the middle;

* (built/outcome) newly constructed formal systems' potential or obtained/reproductible theorems from them appear on the right (or also, programs execution results);

* the square brackets denote tangible things, input or output of computation (e.g., can be wired in "hardware" or have a persistent or transient electronical representation in "software", or etc), otherwise their absence denotes ideas¹ inception, or computation² (or "result"), or a pure function/rewriting system³ (or "translator"), anyway accessible at least to the human brain when it makes Godel's theorems the minimal meta-mathematical hypothesis (beforehand of any further formal construction, in this intended transition from the left to the right, precisely);

* "x"s denotes undecidable termination of a machine (or unknown existence of proof), "1"s denote known termination (or existence of proof, by constructing it), and "0"s known non-termination or exhibited formal inconsistency;

* "?" denotes the arbitrary of the "intent" of using a pre-existing "given", as input of the translation function in the middle;

* "*" denotes the arbitrary of the "purpose" of using the pre-existing "given" on the left, w.r.t to the outcome (possibly, not forcibly) obtained on the right;

The first two diagrams give two options possible representation of Godel's incompleteness theorems (my guess is I'll probably stick to the second, which doesn't need introducing "!" as another symbol with its would-be-adhoc semantics).

¹ (if in left-hand side)
² (if in right-hand side)
³ (if in the middle)

Doesn't a proof that the compiler from S to D is correct combined with the proof for S automatically give a proof for D?

Doesn't a proof that the compiler from S to D is correct combined with the proof for S automatically give a proof for D?

No. Well, how do you define "correct"?

For example, suppose I translate integer f(integer a, integer b) { return a + b; } into (define (f2 a b) (+ a b)). The trivial proof that f has an integer value does not hold for f2.

Correct is that the compiled program has the same runtime behavior.
The statement about f is "Given two integers it returns an integer". Doesn't the same hold for f2?

If f is called in a larger program that is type correct, then that means that f2 will only be called on integers in the translation of that program? So there is a proof that proves that f2 always returns an integer.

Doesn't a proof that the compiler from S to D is correct combined with the proof for S automatically give a proof for D?

With dynamic typing you don't have to worry about the type system raining on your parade but the underlying correctness issues are the same in both situations. Dynamic typing really just postpones the consequences of type errors so the problem is still an important one in the context of dynamically typed languages.

Dynamic typing really just postpones the consequences of type errors

but it seems like the delaying of possible type errors is supposed to open up more flexibility somehow?

Robb Nebbe: With dynamic typing you don't have to worry about the type system raining on your parade but the underlying correctness issues are the same in both situations.

That's false: the point of static typing is to disallow a set of incorrect programs at compile time rather than waiting to find out that they're incorrect until runtime. In the limit (which would mean strongly specifying your entire program in something like Coq and then extracting it to running code), you can eliminate all defects this way.

raould: it seems like the delaying of possible type errors is supposed to open up more flexibility somehow?

Yes, that's the trade-off: static typing is necessarily conservative, meaning that the type system necessarily rejects some correct, but ill-typed in the given type system, programs. The "richer" the type system, the less of an issue this is (cf. strongly-specified software in Coq), but the weaker/less coherent the type system is, the more so (cf. Java, C, C++...)

the type system necessarily rejects some correct, but ill-typed in the given type system, programs. The "richer" the type system, the less of an issue this is (cf. strongly-specified software in Coq)

I don't think this is necessarily true. There is always a trade-off between how "strong" a type system is, and how "flexible". Just observe how recursion is restricted in a language like Coq. It allows the type system to check termination, but it also forces you to jump through hoops occasionally, because the `natural' formulation of some algorithm is not type-correct (and in fact, some algorithms cannot be implemented at all).

There is always a trade-off between how "strong" a type system is, and how "flexible".

I don't think this is true. You can have a type system that can track types of varying "strength."

(and in fact, some algorithms cannot be implemented at all)

Only if you require your type system to enforce some minimal set of properties (like termination).

Andreas Rossberg: Just observe how recursion is restricted in a language like Coq. It allows the type system to check termination, but it also forces you to jump through hoops occasionally, because the `natural' formulation of some algorithm is not type-correct (and in fact, some algorithms cannot be implemented at all).

These are good points about what you can do if you wish to treat Gallina as a programming language, i.e. you wish to write and run software within Coq itself. However, I'm talking about using Gallina as a meta-language and then extracting OCaml, Scheme, or Haskell code. A lot of effort has been put into making that practical; see Bedrock and Ynot for the state of the art here.

Now I must be missing something. What is "meta" about that? You are still using it as a programming language, in a way no less direct than, say, programming with monads in Haskell. Practically speaking, Ynot is just an extension to Coq's Gallina, and the "extraction" to Haskell or OCaml is merely a form of compilation.

It's true that with Ynot you can express general recursion - but only inside the ST monad. You are trading one restriction for another. Don't get me wrong, I think this is a good solution. But there is no magic, it remains a trade-off.

There is always a trade-off between how "strong" a type system is, and how "flexible".

Are you you simply not considering the many type systems out there that, through poor design or limited foresight, manage poorly in both strength and flexibility? If you need it, I'm creative enough to produce a type system that is both weaker and less flexible than state-of-the-art, in order to contradict your statement.

Given history, I'm skeptical that we have reached local or global maxima for flexibility and strength in even the more academic type systems. That is, there likely still exist means to increase strength without sacrificing flexibility, or vice versa. For type systems in common use by developers, we're even further from those maxima.

The notion that there is 'always a trade-off' seems to be a dangerous one, in this field and so many others - it may blind us to possibilities that don't involve a trade-off. (Fight zero sum bias.)

Just to be clear on the trade-off here:

the point of static typing is to disallow a set of incorrect programs at compile time rather than waiting to find out that they're incorrect until runtime. In the limit (which would mean strongly specifying your entire program in something like Coq and then extracting it to running code), you can eliminate all defects this way.

You can indeed eliminate all defects this way; there's a whole spectrum of ways to do so, with the following extremes at opposite ends of that spectrum. Please note, I am truly not trying to be flippant or dismissive; I'm simply pointing out that these are the extremes between which all other possibilities are placed.

• As the set of defects your type system addresses, choose the empty set. Your type system then eliminates all programs that contain defects of the sort you're trying to eliminate, because you're not trying to eliminate any.
• As the set of defects your type system addresses, choose the set of all possible program defects. Choose your type system so that it rejects all programs. Your type system then eliminates all programs that contain defects of the sort you're trying to eliminate, because it eliminates all programs.

Anywhere between these extremes, there will certainly be some defects that your type system does not address. A more interesting question is whether it is possible for a serious nontrivial static type system to avoid eliminating any programs that aren't defective. My instinct is that it isn't possible; you'll always end up both admitting some incorrect programs and excluding some correct ones.

My instinct is that it isn't possible; you'll always end up both admitting some incorrect programs and excluding some correct ones.

I'd say this is pretty much a direct consequence of the Halting Problem and the Incompleteness Theorems.

The latter half is true - you'll always exclude some correct programs (with the usual qualih). Why should we have to admit incorrect programs, though. I'll buy it if you change "both/and" to "either/or" (maybe that's what you thought it said?)

No matter how much stuff your type system catches, I suggest there will always be something else that one might imagine a type system catching. Hence some "incorrect" programs are still being admitted.

I was a bit sloppy, in my earlier post, by failing to explicitly distinguish between the set of defects addressed by a type system, and the set of program properties that a program ought not to have. The latter are things that one might contemplate some type system addressing.

I'd say this is pretty much a direct consequence of the Halting Problem and the Incompleteness Theorems.

Proponents of dynamic typing are likely to agree with you, but it really depends on the unavoidably subjective question of what one considers to be a "defect". Which is why I hedged.

Assuming we can all agree that certain classes of primitive acts at runtime are defects, a program that would do any of those things at runtime is defective. If we choose just those runtime acts as our defects to address, then it is formally undecidable at compile time whether an arbitrary program is defective.

But suppose I write a function (procedure, method, whatever you call it) that performs a certain kind of operation on arguments of a certain type, and I claim that my function will perform correctly on all arguments of that type, but I do not make any claim about its behavior if its arguments aren't of that type. Is a program "defective" if it asks my function to handle arguments of another type, even if in fact my function would still work on those arguments? Proponents of strong typing are likely to answer "yes", and they may then honestly maintain that their type system does not eliminate any correct programs — because they really do consider all eliminated programs to be incorrect.

This all really gets interesting when you realize that making a type system more flexible means making it more complicated — and the above justification for static typing intrinsically requires that I, as the author of my function, make a claim about when it will work right, forcing me to contend with the type system, however complicated it is. Whenever I move from working in a statically typed language to working in a dynamically typed one, I'm sorry to be giving up the automated sanity check on details of my coding, but greatly relieved that I can just tell the program what to do without struggling to come up with inventive ways to contort my overall program design so it will line up with the structure of a static type system.

I disagree.

It is possible to design type systems that never allow incorrect (with respect to the guarantees provided by the system) programs, or systems that always accept correct programs. What is considered impossible is ensuring both at the same time.

A type system such as ML, for example, ensures that the program will not "get stuck" due to incorrectly typed executions (such as adding an integer and a boolean). When a type system is proved correct, you prove that all typed program are free of type errors : no incorrect (ill-typed) program is accepted.
Of course, this does not mean that the program is free of other kind of errors, but this is obvious : the type system doesn't say *anything* about other kind of errors. So this is correctness relative to correctness properties ensured by the type system.

One may therefore argue that the "admitting incorrect programs" bit comes from the fact that no type system can express all the correctness properties one have in mind. I'm not sure this is true, as proof-based type systems such as Coq's can express arbitrary formal properties, so you could probably express any correctness correction in Coq type system. That does not mean that all Coq program are correct in all things : you never get more than what you specified. You can choose to only prove the termination of your program, but may give arbitrarily more useful specifications --- if you accept to pay the cost of proving harder things.

The two theorem you mention (which are rather two sides of the same idea) are only incompleteness theorems : some correct programs are excluded. They don't say that incorrect programs are admitted.

In the other directions, one may design systems that accept all correct programs, but (hopefully) reject some incorrect programs. Those systems only reject the program when they *know* it has an error, instead of when they *cannot prove* there is no error. Unit testing is an instance of such systems. Incomplete analysis for languages with a semantic ugly as hell, such as most dynamic languages, are often of this kind (soft typing, etc.). Of course, those systems necessarily admit some incorrect programs.

I once heard an teacher in mathematical analysis say that "Upper bounds, lower bounds, approximations; this is what analysis is about.". Formal methods for programs are no different.

I said that you can express "arbitrary correctness properties" in Coq. But there are facts that you cannot *prove* in Coq (termination of the Coq type system), so there are programs that you cannot write directly (a Coq evaluator). What does a specification that you cannot express look like ?

Matt M alluded to an even more powerful class of provers, where the proofs may not terminate, but are arbitrarily expressive.

I'm not aware of any main stream languages that require type systems that are "powerful" enough to express the arithmetic operations required for the incompleteness theorem or that are themselves Turing complete.

Re-read John Shutt's comments, then Andreas Rossberg's reply.

As for your comments, I think you simply misunderstood the conversation.

John was not talking at all about "main stream languages". He was defining the problem in terms of two extremes, so as to highlight the tradeoffs in an abstract way. How meaningful that is will be questionable, since there are type systems where counter-examples are supposed to exist for certain properties e.g. halting, but haven't been found. Mathematics has a lot of these funny cases, and mathematicians don't know yet exactly what to make of the properties of problems that make them practically tractable. Moshe Vardi gave an example of SAT solving technology in this month's Communications of the ACM, asking why SAT solving technology has been so effective and so few problems encountered despite what the laws of nature tell us about SAT solving in general.

I would say nailing down pragmatics has proven elusive for academics, and would welcome anyone who knows of papers that discuss these pragmatics well.

The point I wanted to make is that I don't know of any support for John's intuition that there is some kind of implicit trade-off that would prevent a type system from being both sound and complete. First-order logic is more than sufficient for any type system I recall looking at and both the halting problem and the incompleteness theorem are completely irrelevant in the context of first-order logic.

I'm not sure I understand what you mean, because the incompleteness theorems of Gödel are usually formulated in first-order logic.

Regarding your first comment about type system not powerful enough to express "arithmetical operations", I think you got the level wrong : it is not the type system that needs to do computation, but the term-level language which is checked by the type system. What we're discussing is if the type system can reject some well-typed program, and Andreas referred to the incompleteness theorem, which in essence says that in a given formal system (type system) proving facts about arithmetic (term-level language), there is a statement that is true (a program that is correct) that cannot be proved (you cannot give a type for it accepted by the type system).

More precisely, the formal property of type system we've been referring to in that thread is that, for most solid theoretical type systems of lambda-calculus, we have a "termination" property which says that the pure lambda terms accepted by this type system always terminate. This is true in particular of all the lambda-cube calculi : simply-typed lambda calculus, System F (and its restriction ML), System Fω, Coq...

If a language (the set of pure terms typable in a given type system ensuring termination) is total, the computational counterpart of the incompleteness theorem says that there are programs that cannot be expressed in the language. The strength of this programming-language interpretation is that the counter-examples (countrarily to Gödel constructions) are eminently practical : you cannot write in the language an interpreter for (an encoding of) the language itself.

Of course, to come back at your comment, there are also termination issues at the type level : as the type system grows more and more powerful, they may themselves approach Turing-completeness. Coq is on the very edge of it, and even more expressive type systems are Turing-complete, so that type-checking a given term may not terminate. This is independent of the question of soundess and completeness of the type system wrt. the term language.

There are many consistent deductive systems for first-order logic that are both sound and complete. This doesn't contradict the incompleteness theorem because the incompleteness theorem only applies to systems that effectively implement the arithmetic required for the "Gödelization" technique used in the proof of the incompleteness theorem, i.e. the incompleteness theorem doesn't apply to first-order logic. In fact Gödel came up with the completeness theorem for first-order logic a couple of years before he came up with the incompleteness theorem. It is also worth pointing out that the two notions of completeness are not quite the same.

I expressed doubt that there is necessarily a trade-off between the expressiveness and safety of a type system. (earlier in this discussion people were talking about the "strength" and "flexibility" where the trade-off seems implicit in their chosen metaphore.) My experience is that first-order logic is more than sufficient for expressing type systems of programming languages so it should be possible for a type system to be both sound and complete. I'm not doubting that someone could define a type system that is Turing complete and thus subject to the incompleteness theorem by virtue of implementing arithmetic but I do doubt the wisdom and benefits of doing so. In particular if this was a big win then someone should have done it already.

You're focusing on whether a type system is sound and complete, which is relative to what the type system is trying to do. But this is about what the type system should be trying to do. That's got a rich blend of subjective and objective factors in it.

Suppose you want a type system to address concurrency errors — deadlocks and race conditions and whatnot. The one such system I recall hearing of (in a talk a few years ago) mixed static and dynamic elements. Suppose your system imposes some static constraints, and you find these constraints are not onerous and make it easier to write programs without concurrency errors, but there exist programs that violate the constraints yet cannot ever have concurrency errors. One reasonable person may say that all programs should obey the constraints because they make errors less likely, therefore any program violating the constraints is automatically defective (even if it can't actually have errors). Another reasonable person may say that a program isn't defective if it can't have errors. And these reasonable people will disagree about whether the constraints eliminate any defective programs. They may also disagree about whether the question I originally posed is trivial, or deep and subtle (to wit: is it possible for a serious static type system to avoid eliminating any non-defective programs).

The other question, whether or not there are "incorrect" programs not eliminated, I don't find nearly as interesting, because once you're willing to contemplate a type system to address behavioral quirks as subtle as deadlocks and race conditions, it seems pretty clear to me that there will always be more stuff you might want to check, but aren't checking yet.

The other question, whether or not there are "incorrect" programs not eliminated, I don't find nearly as interesting, because once you're willing to contemplate a type system to address behavioral quirks as subtle as deadlocks and race conditions, it seems pretty clear to me that there will always be more stuff you might want to check, but aren't checking yet.

There would seem to be a few ways to interpret what you've written here:

1. There is no formal system powerful enough to prove the correctness of various properties we wish to state about our programs. I believe this to be practically false. Something as powerful as ZFC with some number of inaccessible cardinals is enough to prove all kinds of practical mathematical and meta-mathematical results. Even Godel's result that you cannot prove the correctness of a self interpreter has loopholes (writing this up is one of my back burner projects).

2. There is no formal system that comes equipped with sufficient formalization of "the real world" for all practical problems.
The problem with proving that "deadlock" doesn't happen is that you first have to define what "deadlock" is. If you don't already have one, that entails building a model that correctly describes the communication in your system. You can use your formal system to prove sanity checks about your model, but your formal system can never establish the correctness of the definitions you've given it. Even if you already have a model of communication, you still have to define "deadlock" correctly.

The hope here would be that as new domains are introduced, domain experts can model the pertinent elements of the domain and develop type systems and abstractions that help programmers create programs with the desired properties.

3. There is no general and automated system to derive arbitrary program properties. Even if you can state the formal property you want in a program, there is no general procedure for inferring that property in arbitrary programs. This is certainly true, though there may be meta-abstractions that can help.

As I understood it, John's claim regarded expressiveness (which 'defects' you can describe and target for elimination) vs. tractability (ability to make a decision in an amount of time suitable for a "serious nontrivial static type system"), as opposed to soundness vs. completeness.

At the upper end for 'expressiveness', we have contracts with preconditions and postconditions, declared invariants and constraints, dependent structural typing, and so on. We can say a lot about how the program should and should not behave. The question is whether we can usefully say these things in the type system vs. whether we can only say them in some sort of external requirements, comments, documentation.

Sure, we can have type systems that are sound and complete and catch a variety of important defects. But 'completeness' is achieved most easily by reducing expressiveness, such that every remaining expression is decidable. Chances are, your sound and complete type system cannot even express many of the defects that a developer might wish to catch - a sort of hear no evil, speak no evil, see no evil deal.

My own bet is on pluggable type systems. Such systems sacrifice typeful programming - that is, the semantics for a program fragment must not depend upon the type context (e.g. no type-indexed polymorphic dispatch; you'll need to explicitly pass a function). But the secondary benefits include better engineering control for the sliding scale between expressiveness and tractability. (For me, the primary benefits of pluggable type systems relate to modularity and sharding of applications.)

Completeness and tractability are certainly related. Incomplete type system allows us to express conditions that would take forever to prove. But I have often wondered whether semi-decidability and a timeout could do the job... especially for interactive programming environments. If we don't limit ourselves to complete type systems, we have one less constraint for achieving expressiveness for the subprograms where it is most important.

When we add Modularity to the mix (Expressiveness vs. Tractability vs. Modularity) then things get more interesting. I would expect that modularity, too, is required for a "serious nontrivial static type system".

AFAIC, I'd bet on the same, too:

My own bet is on pluggable type systems. Such systems sacrifice typeful programming - that is, the semantics for a program fragment must not depend upon the type context [...] But the secondary benefits include better engineering control for the sliding scale between expressiveness and tractability.

and where I'd tend to agree, too, that is: if I can take it that your (broken, btw) link probably wanted to refer to Gilad's Pluggable Type Systems(?)

Anyway, I found very interesting that Gilad (four years earlier than I did, unsurprisingly) had actually thought of the same kind of possible paths of further investigation as I thought of, eventually (i.e., before I read this paper of his, recently) — quoting:

[...]3 Toward Pluggable Types

[...] This is easier said than done. How do we integrate multiple type systems into a language? This area needs research. One approach would leverage off of the growing support for user-defined annotations (often referred to as metadata) in programmming languages. Both C# and Java support some form of annotations added onto the program’s abstract syntax tree. In this approach, one takes the view that types are just a kind of metadata. Tools can then choose which metadata to display and how to display and use it.

Challenges remain with this approach however. [...] Issues of namespace and version management need to be handled well. In short, it’s a long way to a proven, robust and usable system that supports pluggable types, but the potential is clear.

Unlike Gilad maybe, though, I suspect the problems that the pluggable type systems idea wants to address (among which certainly is this OP's expression problem, to some interesting enough extent) may not be sufficiently described and resolved by a mere design and implementation of one language (or class thereof), but may also require support at some scalable infrastructure-level — where resource types, and instances, and their identifiers, should be able to embrace (at will, whenever the programmer is aware of and sees fit) provably correct verifiers, source-to-source translators, etc.

I suspect, also, that the "metadata" Gilad alludes to may not be held practically enough at the "traditional" type system-level (i.e., the one we usually know of in today's languages: expressed in the syntax, in source languages' phrase fragments, then reified and queryable in some way at runtime, e.g., as strings, objects, or whatever). Instead, I'm thinking of a possible critical correlation with the intrinsic properties of those languages' syntaxes themselves — thus, requiring support for speaking about "meta linguistic" properties of the phrases, even before attempting/allowing the aforementioned type system "plug-ins" to appear and be taken care of (at compile- and/or at run-time).

Hence my interest in this (from John) and that (from David) on this dear LtU, too, for instance. Oh, and munificient's.

But yes, as Gilad wrote in his paper, this is very likely a long way left to go one has to have in mind (well, I have, anyway).

Actually it is correct: There is a possibility of a type system eliminating a "correct" program at compile time. That is what I would consider the type system "raining on your parade". It is unclear what you are actually disagreeing with since you say much the same thing at the end of your post.

Having correct programs rejected is often a fear of people used to dynamic typing trying to program in a language with static typing. This is analogous to the fear people used to static typing have that a huge number of type errors are going to make it into production code in a dynamic language. My experience is that these issues are much more interesting in theory than they are in practice.

The question this begs is how much code you've written in a language with a rich enough type system to make the difference really large: an OCaml, Haskell, Scala, or one of the proof assistants. People in commercial endeavors using one of the above often report a defect rate cut by orders of magnitude, which would seem to counter your claim. OTOH, if your example of static typing is C, C++, Java... then your claim isn't surprising at all. :-)

I believe many people have written something like "w = \x -> x x" or "y = (\f x-> f (x x)) (\f x-> f (x x))" in Haskell or ML, and the compiler rejected it. Well, perhaps a more powerful system can solve them, but I don't think it can solve all problems. Richer type system less likely to reject correct programs, but once it get in your way, it is harder to work around or pass through.

People used to dynamic typing don't want to fight with the static type checker. It is extra work. Type checker should be a tool to help problem solving, not problem making.

Some people just take the touble from the static type systems for the benefits, but some people don't.

It is a common misconception that these would be difficult to type. Witness:

> ocaml -rectypes
        Objective Caml version 3.11.2
# fun x -> x x;;
- : ('a -> 'b as 'a) -> 'b = <fun>
# (fun f x -> f (x x)) (fun f x -> f (x x));;
- : ('a -> '_b -> '_c as 'a) -> ('d -> '_b as 'd) -> '_c = <fun>

As you see, even type inference is easy - with Hindley/Milner, just drop the occurs check from your unification algorithm.

But! People who complain about these examples fail to understand the pragmatics of type checking. This relaxation makes almost every program well-typed — which is bad! You want the type system to catch what is likely an error, and types like the above come up accidentally much more often than intentionally. Very early Ocaml had -rectypes as the default, and users complained because it made the type system much less useful.

Some people just take the touble from the static type systems for the benefits, but some people don't.

\rant It is my suspicion that the latter class of people rarely has to work on huge code bases written, and constantly modified, by lots of different people.

Interesting. Can you give an example of a program that you'd like to reject that is well typed with cyclic types?

See e.g. the bottom of this page.

(Admittedly, saying "almost every program" was a bit too strong, "many erroneous functions" perhaps is more accurate. However, it makes literally every program well-typed in the plain lambda calculus.)