Lambda the Ultimate

If you take a prescriptive typing view, variance annotations are also unnecessary.

What you're saying is not so much that variance isn't needed, but that it can be derived in many cases. This is trivially true for all cases where a type declaration is concrete, i.e. has a definition. OCaml does that for type aliases, for example.

In general, however, types can be abstract, and if you have higher-kinded abstract types then you need to look at their uses, i.e. do real variance inference. Just consider (using Scalaish syntax):

f[C[_]](x : C[Dog], y : C[Cat]) : List[C[Animal]] = [x, y]

You need to infer from the list expression [x, y] that C has to be covariant -- and this is still a simple case. I don't remember any work that explores this (but I haven't looked).

Another problem with inferring variance, at least in the case of classes, might be brittleness and/or exposure of implementation details. That is, a class might be variant unintentionally, and users might start relying on that, and then you cannot extend the class anymore (or modify its implementation) in ways you may have intended. Not sure how much of a practical problem that would be, but it's always better if you can make all parts of a typing contract explicit, at least as an option.

I'm not proposing to infer variance for non concrete types, or to remove variance, just that declaration site variance seems to be unnecessary (plus a simple way to implement use-site variance, but since I know nothing about the existing approaches that may be well known).

As written, that function f looks to me like it should just be a type error. You'd have to write that function as follows:

f[C[_]](x : C[Dog], y : C[Cat]) : List[C[out Animal]] = [x, y]

To make sure that only the outputting methods of C are accessible for the elements in the list.

If you really want to avoid implicit variance of a concrete class, you could always add an extra dummy method that makes it invariant. Note that the variance of a generic class isn't dependent on its implementation, only on its type signatures. I agree that it may be undesirable that existing code ceases to type check if you add an extra method to a class, but I don't think that this would be a big problem in practice. Arguably, it's only natural that changing a type signature may cause type errors in code that uses that type. Other constructs already have the exact same situation. For instance if you have object literals that can implement interfaces, then if you add a method to that interface then existing code will signal type errors.

Andreas mentioned that it would be implicit that C was covariant. So he's thinking the inferred type would quantify only over covariant C. You seem to be thinking that each type functor has covariant and contravariant parts, as in your proposed translation above, so that you quantify over all functors C and then can ask for the covariant part. That seems like it's going to have a problem with higher rank types.

In any event, trying to sort through these issues seems like a good exercise to require of anyone contemplating rampant subtyping constraints for their new language.

Hm, okay, I guess I never felt very comfortable with use-site variance, and find this way of writing the example rather unintuitive. But YMMV.

I'm not sure how your variance splitting translation for generic parameters can be sufficient. Wouldn't you also need to split every class itself into a co- and contravariant version? If you think of nominal types (like classes) as a contrived form of (globally bound) existential type variables, then that would be a natural consequence. That is, shouldn't

class Bar { Bar f(Bar) }

become

class Bar_in { Bar_in f(Bar_out) }
class Bar_out { Bar_out f(Bar_in) }

Otherwise, I don't see how you could instantiate a generic with a class correctly.

A related question is how your scheme would deal with invariant uses. Wouldn't you actually need to split everything into three versions for that?

I'm not sure I follow what you're saying in the second paragraph. If there is no def-site variance, then the notion of "variance of a generic class" does not even exist, right? OTOH, if you do have def-site variance, then the variance of a generic class can depend on its implementation, because that may make certain assumptions about it, say, inside a method that self-references the class type internally.

The type system is unsound, due to the covariance of generic types. This is a deliberate choice (and undoubtedly controversial). Experience has shown that sound type rules for generics fly in the face of programmer intuition. It is easy for tools to provide a sound type analysis if they choose, which may be useful for tasks like refactoring.
Gilad Bracha, Google's Dart announced, (emphasis mine)

Warning: controversial rant ahead.

Design is about solving problems; design solutions should be presented to the community so that we can critique and build on each others solutions. Rigorous empirical, scientific, theoretical evaluations are nice to have, but not always possible nor very useful.

In my opinion, the problem is that the PL community, and the OOPSLA community specifically, has drifted away from their earlier focus on solving problems into some sort of scientific navel gazing. A focus on scientific evaluation has led to a plethora of low quality publications that fit the rigor requirement and have crowded out design papers that actually solve problems! So OOPSLA might accept 60 (!!) papers this year, but most of them will be uninteresting because...science!

It gets much worse than that: our publication venues are preventing us from being innovative and inventive, it is too difficult to do something new and get recognized for it. Instead, we have fallen into the trap of small incremental refinements that can take advantage of lots of previous rigor. None of the new languages coming out these days are really new at all.

Yes, interesting work can still be presented in more innovative venues like Onward and The StrangeLoop, but why? Where are we going as a community?

Rigorous empirical, scientific, theoretical evaluations are nice to have, but not always possible nor very useful.

As an analogy, cheap genetic sequencing caused a methodology revolution in bio (and a ton of lessons), but wasn't practical for a long time. I don't know how many Ph.D.s have been devoted to verification techniques -- what if we similarly invest in empiricism? That should bring down the cost of application, so my questions have been more about when they'd be worth it and what's the route.

I agree that dominant academic schools of thought are severely boxing in design research, but you already know that ;-) However, punishing empiricism sounds like barking up the wrong tree. E.g., empiricists have a poor showing at R1 institutions, and I can only think of one guy who might make the jump any time soon.

My attack on empiricism has nothing to do with the true empiricists, but with many's misguided notion that empiricism is a real solution to our design research problems. We do not need to replicate the well known problems of HCI in PL!

Truly useful empirical research takes a lot of time, planning, resources, and has limited applicability even when performed correctly.

My attack on empiricism has nothing to do with the true empiricists, but with many's misguided notion that empiricism is a real solution to our design research problems.

It weeds out incorrect theories through testing and heralds new ones by revealing phenomena, so I have to disagree at least based on theory. In terms of expected impact for the next 5-10 years, I'm curious. The internet, source control, mechanical turk, quantitative revolutions in social sciences, etc. have revealed many opportunities.

We do not need to replicate the well known problems of HCI in PL!

Counting on HCI folks to solve PL problems is not a good idea.

Truly useful empirical research takes a lot of time, planning, resources, and has limited applicability even when performed correctly.

Brad Myers writes as much as well. I'm more optimistic in two ways. First, there's probably a lot of useful low-hanging fruit, such as Shriram's experiences with error messages. It shouldn't be so hard to run conceptually simple trials like that, so I suspect proper tooling and automation can take away a lot of the bite -- there are few established norms and techniques here. Second, data driven design is still an emerging concept. E.g., Stackoverflow is now the default tool for documentation and debugging help. I doubt it'll be the last data-driven tool.

The internet, source control, mechanical turk, quantitative revolutions in social sciences, etc. have revealed many opportunities.

There are plenty of new opportunities to know things, its knowing things related to the problem you are trying to solve that is important. If this is your problem, or you can bias the problems you work on based on what you can objectively know or discover, great! But many of us do not have this luxury.

Counting on HCI folks to solve PL problems is not a good idea.

Nor are transplanting disfunctionalities in the HCI community the PL community.

First, there's probably a lot of useful low-hanging fruit, such as Shriram's experiences with error messages. It shouldn't be so hard to run conceptually simple trials like that, so I suspect proper tooling and automation can take away a lot of the bite -- there are few established norms and techniques here.

Low-hanging fruit that is useful for something might not be useful for you. 99% of what UX designers do, however, is not within the realm of the low-hanging HCI fruit, I don't see why this would be any different for PL designers.

Second, data driven design is still an emerging concept. E.g., Stackoverflow is now the default tool for documentation and debugging help. I doubt it'll be the last data-driven tool.

I'm sure data has a big role to play in our future, but say pure data-driven design as practiced in Google...is already known to fail. Data can't replace design, it can only augment it.

Low-hanging fruit that is useful for something might not be useful for you. 99% of what UX designers do, however, is not within the realm of the low-hanging HCI fruit, I don't see why this would be any different for PL designers.

I think there'll be a bunch of general design and implementation techniques that pop out. Examples include Shriram's error message technique, Stackoverflow, and 'rules of thumbs' that pop out of Andreas Stefvik's work such as how to name a for-loop construct.

It's also a great example of something that developers have little time to do today, so automation would make it scalable.

Whether empiricism belongs at every step of the way, it's easy to say 'no' today. If research continues -- it's not as obvious.

I'm sure data has a big role to play in our future, but say pure data-driven design as practiced in Google...is already known to fail. Data can't replace design, it can only augment it.

Agreed -- I view data as an ingredient for creating new types of designs, and in the case of empiricism, a testing strategy, and more ambitiously, a step along the path towards understanding why designs succeed or fail.

Alot of heuristics involved, and we still aren't sure what the quality of these signals are; worse than nothing is still a possibility.

Agreed -- I view data as an ingredient for creating new types of designs, and in the case of empiricism, a testing strategy, and more ambitiously, a step along the path towards understanding why designs succeed or fail.

Isn't it that some great designs leave a nice tingling aloe feeling in our brain and some horrible ones give us massive headaches? To understand why is to understand self, and I bet we are a long way away from that. Some of it (beyond visuals even) really is aesthetics that we can't even begin to quantify, like a beautiful vs, ugly syntax.

Agreed, I'm not claiming a magic bullet. Instead, I expect several big and many small advances, and can even argue that they already have occurred. Some of the advances can even foster design by providing foundations (e.g., social or cognitive) rather than building on mud.

...you might enjoy Richard P. Gabriel's Onward 2012 paper, The Structure of a Programming Language Revolution. It's basically his personal reflections on how the programming languages field greatly increased the level of mathematical rigor it required, and how this changed the character of the field. While mathematical rigor is of course different from empirical rigor (and I have the ICSE/FSE rejections to prove it), RPG's complaint seemed very similar in spirit to your own.

It's a very interesting read, though I disagree with his assessment of what happened. In my view, what happened is the publication of the Wright/Felleisen methodology for proving syntactic type soundness. It is so easy, and works on so many different languages, that it radically lowered the cost of building sound type systems. So people made a lot more of them! I also think that the type systems gold rush is over (and has been for some time): people are now trying to design languages and prove programs with properties that go well beyond what progress/preservation can say.

This makes me wonder if there were any major empirical successes analogous to the Wright/Felleisen paper which triggered a transformation in the culture of the practically-oriented end of the field. Maybe the appearance of large open-source Java codebases with detailed commit histories?

I went to RPG's talk at Splash, I think the main gist of his essay was about how reality is however we view things today, regardless of past meanings (incommensurability). I don't think this applies to my problem, which is not really about the past, but how those that were provided so much freedom in the past to innovate and invent have imposed a stupid system on the present to prevent us from having the same opportunities.

The paper I'm working on basically tears up all previous type systems work. I'm either being very inventive or I'm chemically imbalanced somehow (I haven't decided yet). I think some of our problem IS that we build too much on the past, and we don't try different paths not taken because we know we can't get published if we do.

it is nice to see good radical thought.

Done.

I'm of the opinion that the field is now looking for the next major theme to focus on advancing. Guys have been working on static type theory now for over a decade, and the low-hanging fruit there (read: the really important, solvable problems) are gone.

So, from the point of view of 'languages are what people can make good programs with', what are the important, solvable problem now?

'languages are what people can make good programs with',

Whether a program is "good" or not is a good question and also a question that's beyond any possible theory of programming languages.

For example, sometimes it might be an ethical question. Suppose that we have a possible programming language feature the main function of which is that it helps enable writing programs for "the cloud". Or maybe instead it helps enable writing programs using 5,000 programmers none of whom really see the big picture of the program.

Making a language to help with those things, or deciding not to, or some other possibility --- these are factors into whether or not language work is helping people to write "good" programs.

Political economy, such as the expected relations of authority and work splitting among programmers, figure heavily into the choices made by programming language designers and implementers.

One direction to explore, that might contain some "low hanging fruit" of reasonable value, is to build better theoretical understandings of the relationships between programming language constructs, and the kinds of political economy that those constructures support, encourage, or obstruct, and discourage.

Such concerns are latent in a lot of prior work on programming languages. Consider how we talk about various combinations of concepts of "safety", "modularity", and "separate (or independent) development".

Perhaps there is opportunity to better understand those relations. And perhaps, because the questions revolve around political economy, it is an interdisciplinary opportunity.

If we are going to spread bullshit like "Don't be evil." we need a better story about "good".

For example, sometimes it might be an ethical question. Suppose that we have a possible programming language feature the main function of which is that it helps enable writing programs for "the cloud". Or maybe instead it helps enable writing programs using 5,000 programmers none of whom really see the big picture of the program.

Hmmm... If it's unethical to enable writing programs using 5000 programmers none of whom really see the big picture of the program, then wasn't OO methodology unethical in the first place? I mean, making plug-together sub-units that are as independent of each other as possible has been the whole focus of OO.

Hasn't our ideal been that someone who doesn't even hardly know programming can sit down, plug together parts made by hundreds of other people none of whom had any idea that their parts would be used in this program, tie it into some kind of UI generator, and get a program that works the way he wants?

How is that different from employing thousands of programmers who have no idea what programs their parts will be used in?

Ray
Bear

making plug-together sub-units that are as independent of each other as possible has been the whole focus of OO

That's an idealized view of OO. In practice, OOP is not compositional. There is no generic way to combine two objects. OOP has not historically been relevant to mashup designs or application-layer components. I am not aware of any OOP language that even achieves pluggable or composable subprograms, much less focuses on them. The focus of OO (in practice) seems to be inheritance-like relationships - prototyping, subtyping, interfaces.

Regarding models where thousands of programmers can develop systems together without anyone seeing the big picture, you are better off looking at multi-agent systems, topic-based publish-subscribe models, collaborative state models (e.g. tuple spaces, shared document editing, blackboard metaphor), and concurrent constraint models.

Hasn't our ideal been that someone who doesn't even hardly know programming can sit down, plug together parts made by hundreds of other people none of whom had any idea that their parts would be used in this program, tie it into some kind of UI generator, and get a program that works the way he wants? How is that different from employing thousands of programmers who have no idea what programs their parts will be used in?

They are duals. In the former case, the context names a reusable component. In the latter case, the plug-in component names the extensible context. The notions of "reusable component" vs. "extensible system" are not incompatible, but they certainly aren't the same.

There are related concerns for how state is modeled, i.e. is it part of the component or part of the context? What does it mean to have multiple 'instances' of a reusable component?

I respectfully disagree that all the "really important, solvable problems" are gone. I still have no practical way to invest a reasonable effort into proving that the code I write is correct with respect to the specification I can write -- in the cases when I know what such a specification is -- or at least some reassuring properties of this code.

I want to be able to write a specification or some properties along with my code. There would be an interaction loop with the verifier telling me which part it couldn't verify and why, during which I would add hints/annotations/proofs (of reasonable size) to the code, until the full verification completes.

I believe this is really important, and feasible;'Tony Hoare argued as much when he proposed the Verifying Compiler as a Grand Challenge for Computer Science Research (pdf) in 2003.. The ideas of how to proceed have been there for a long time now, but the proof automation technology is constantly improving. So we are "mostly there", but not quite. You need to solve the hard problems, and then you need to integrate the solutions into a mainstream-enough programming environment for people to use it.

So far I don't know of any such efforts having been used outside the research team it originates from. There are known feasible ways to write proved-correct code, but they involve a radical change of programming techniques (eg. writing the program directly in Coq as Compcert). There are also usable partial correctness tools, for eg. SPARK/Ada or static analysis plugins for Java/C#, but to my knowledge they're not meant to specify functional correctness properties. Static contracts technology is coming close, but I'm not aware of realistic non-insider uses.

I still have no reasonable way to write a specification that is correct with my intended goals. Heck, I have no reasonable way of figuring out what my goals are beyond writing code and experimenting.

Even if this magical verification technology comes out, I have a feeling that we would just get hung up on the specifications, which become more like code themselves. Perhaps we can do away with the specifications and get some assurances on null pointer exceptions and such, but I still don't think my life will be much better than it is now.

Not that I don't think that this field is not worthwhile, surely it is; just that I think the role of safety and security is often overstated against various bogey men to scare funding out of DARPA. The amount of resources consumed by security concerns in PL is quite amazing, that it has been along time since anything related to real productivity increases has been adequately funded. This is another one of my pet peeves.

If you want to prove that the code you write is correct with respect to the specification, what you're talking about is a "specification" language that you program in.

It's been my experience that the people who write specifications rarely produce a self-consistent specification in the first place (ie, a specification for a program which can exist without logical contradiction). Those who do produce a self-consistent specification leave so much ambiguity that there are an infinite number of different programs having vastly different semantics which could trivially be said to "meet" the specification, the vast majority of which would be rejected by the specification writers who will claim that that isn't what they meant. This is because they are trying to put in a "reasonable" effort rather than the amount of effort required to actually program.

The methodology of programming languages (and the specification language you require) is to be able to write down something that has one (or very few) self-consistent specific semantic interpretations. And generally in the case that there is more than one semantics which can result from code, we regard writing code that actually permits a difference in result depending on such ambiguity as "bad style" at the very least, or "a logic error" if we are being less charitable (Well, unless specifically randomizing for simulation or some such purpose).

If you develop a specification language that has only one (or very few) self-consistent specific semantic interpretations, then why bother programming at all? That language is a declarative programming language in the first place. If writing such a precise specification winds up being less work than just coding, then you'll have invented a really *good* programming language. Somebody will then write a compiler for it, turning specifications into programs. Then you'll wonder how to prove that the specifications are correct.

Writing such a detailed, consistent specification cannot be less effort (nor, unfortunately, less error-prone) than writing code, and for exactly the same reasons. The quest for such a specification language is the same as the quest for a better language to program in.

In fact, IIRC, this is how the Lisp language came into existence. McCarthy developed a language for formally reasoning about programs, provability, and semantics, and was as surprised as anybody when somebody wrote a compiler. And people can still write Lisp programs that don't meet specifications, or meet them without meeting actual requirements.

The general difference between a specification language and a programming language is that the latter needs to produce an executable of some sort.

It's been my experience that the people who write specifications rarely produce a self-consistent specification in the first place (ie, a specification for a program which can exist without logical contradiction).

This is precisely what makes specifications so useful. Your compiler can't verify that your axioms align with reality, but it can tell you that they're consistent. With a sufficient level of specification, this will identify the vast majority of bugs (in my estimation).

I know that specifications have problems themselves, they can be impossible to pin down, or be written down incorrectly. However, in my experience a lot of the small bricks of software we compose to build larger (and loosely defined) applications do have a clean interface and specification. Think of the functions of your standard library, the compiler of your language, the small command-line tools of your UNIX userland, etc. Specifying those should already be done, and in practice we are still getting functional errors and security issues from this part of our software base.

Specifying often amounts to writing code; one good example is that the specification of a sorting function, depending on how you define the logical "is a sorted sequence" predicate, often precisely corresponds to an insertion-sort implementation. But note that the actual implementation of the sorting function can be much more complex, low-level, efficient, etc.

The idea that code can serve as specification is well-known, and it is still a net gain if this code is simpler to write, maintain and reason about than the actual code running in production. (Moving the trusted code base from 50K lines of implementation to 1K lines of specification is a win.) This idea is an integral part of the Bedrock project for example:

Bedrock is [...] computational: Many useful functions are specified most effectively by comparing with "reference implementations" in a pure functional language. Bedrock supports that model, backed by the full expressive power of Coq's usual programming language.

It is easy to see cases where specification could have prevented problems, much harder to see many other cases where it couldn't. If I were to talk about standard libraries I used today, what does the formal specification for Canvas look like anyways? How often do I bother sorting something, and how less often do I bother writing a sort function? Real programming often isn't very algorithmic.

How many us would benefit from taking the Bedrock approach, considering the code we wrote today?

So, from the point of view of 'languages are what people can make good programs with', what are the important, solvable problem now?

Productivity, tools, having the computer do more thinking for us, lowering the threshold needed to become a good programmer and spending less time doing tedious crap. Languages are also still poorly designed, inconsistent, unprofessional, and such.

Productivity, tools, having the computer do more thinking for us, lowering the threshold needed to become a good programmer and spending less time doing tedious crap.

Okay, agreed on that.

I've been having some woolly ideas about formalizing the interface requirements between modules in a better way than has been done before which may play into that goal. Sadly, it amounts to more type theory. And I'm bored of type theory. Still, it may be worth explaining, or making a few blog posts about, because it really would make modular design a lot easier.

We've spent a lot of effort forcing subunits of programs (objects, if your style runs that way) to document what interfaces they PROVIDE. But as we plug them together, problem of forcing them to document (and possibly even standardize) what interfaces they REQUIRE has become by degrees just as important. That problem is, as yet, nearly unaddressed.

As matters stand, nearly every "modular" program subunit comes with a forest of specific, non-substitutable dependencies and libraries that cost efficiency and memory and bloat our programs with redundant crap when some other object requires different dependencies and libraries that provide essentially the same services, but with different argument orders and/or minor additional or missing functions.

Simply speaking, you have modularity on the "provides" side - nice for building new stuff on top of - but utter rigidity on the "requires" side, so what supports the functionality is essentially frozen and accumulates efficiency-sucking layers between new code and hardware forever.

We've seen adhoc efforts to do something about this, such as the rise of virtual machine languages and cross-platform libraries. Versions of the same virtual machine or same library implemented to run on different platforms are deliberately substitutable infrastructure. Ditto runtimes for many languages. Access to the screen, for example, may be accomplished in entirely different ways under Linux and on a nook tablet, but the runtime abstracts access and provides a uniform interface.

But this kind of effort toward substitutability - even the effort to *document* requirements so that substitutability could be attempted - rises very rarely into the realm of code written by the people who use these systems. And it has become at least as important as what interface is provided.

Languages are also still poorly designed, inconsistent, unprofessional, and such.

Heh. I think that "unprofessional" means something which, apparently, you don't think it means. Let's face it, hardly anybody gets paid money for building a new language. Academics may get a paper or even a dissertation out of it, but the vast majority of new languages are still implemented "for the fun of it" or "for the hell of it" or "as an experiment" or "because I have pet peeves about programming languages that I want to address" by people who are both unacademic and unprofessional. Nothing is going to stop them, and IMO nothing should.

If you believe that more of them should be paid, or that more of them should be academically recognized, or that more professional and/or academic people *should* develop languages, thats ... well, heck, I'd like that too, but it's unlikely to happen.

Ray

Heh. I think that "unprofessional" means something which, apparently, you don't think it means. Let's face it, hardly anybody gets paid money for building a new language.

Pretend I work for a certain BigCorp where people do get paid to design languages (well, one language) that are used heavily internally by 1000+ people to solve certain problems. But they are not language designers, and the languages are accordingly designed very poorly. Now stop pretending :) There is also a big difference in language design that goes to conferences like OSDI/SOSP and design that goes into our own PL conferences.

What you are talking about is a bit different and not something I'm worried about; people will always scratch itches and it would barely affect me or my work.

Okay, that's maybe three or four people for the design, all at a particular BigCorp whose name we all know. Regardless of your opinion, they are indisputably professional language designers, and therefore the language was in fact designed professionally, whether it's up to your standard or not. About seven new languages, I think, have been built this way in the last twelve years.

I'm betting that hundreds of adacemics will unprofessionally produce scores of languages this year, and have done so every year, during that twelve-year span.

I'd further bet that six times that number people who are neither academic nor professional have unprofessionally produced languages every year during the same period.

We still aren't talking about the same people, but I'm not going to get more detailed than that. BigCorp is a HUGE company and the professionals who actually get paid to design languages are in a different building in a different campus working whose customers are much more external. More than 7 new languages are designed per year at BigCorp, if you are on the outside, you wouldn't know about any of them probably.

... but I have made (and still make) compilers for custom languages as part of my job.

All of this "unprofessional" business and generalizing who makes these things and why sounds kind of snobby to me.

Probably because I'm on the receiving end of your judgement. ;P

I agree. Lay or professional*, makes no difference. I think the Jonathan Meades comment on architecture could be applied here: "the only school is talent." There's plenty of outsider languages being used daily.

(*)I've experience of both and let me tell you that getting paid only made the result more expensive.

I was referring to professional systems designers designing languages without any of the experience that we have, or even an interest in that experience. The result is as expected. At least if your company has professional language designers already, you might want to try and use them. Yet we are like UX designers in this regards, many dont even know we exist, and the job is done by some PM....

(Many language designers are titled as researchers or PMs also, but only because BigCorp doesn't know how to define our role exactly....)

Larry Wall was a professional sysadmin. He was also a pofessional (human languages) linguist, of a particular theory of natural language called Tagmemic Linguistics.

His invention was Perl -- an attempt to create a computer language that uses pronouns, context, etc, in some of the nuanced ways that human languages do. Its semantics were largely inspired by Wall's natural-language work.

Was he a "Professional" programming language designer? No. Did he produce anything elegant and precise like professional programming language designers might have? No. Was his type system sound? Ha!! It was deliberately, intentionally, vague and subverted itself three times before breakfast!

Was he aware of programming language design literature? Maybe. But his goal, aside from making it easy to do the reports his sysadmin job required, was to try and apply natural-language ideas to computer code. He was deliberately trying to produce something that's vague and occasionally even ambiguous but in useful ways like human languages. He wouldn't have cared about the soundness of his type system, any more than we care about the (in)consistency of our pronoun applications, even if he was completely familiar with the type literature.

Whatever. I don't happen to like Perl, because I feel that those same ambiguities and vaguenesses get in my damn way when I'm programming. I also dislike the line-noise syntax, but I could get over that. But hey, pronouns in programming languages were a really neat idea!

My point was that an outsider like Wall can have a completely original idea in programming language design, that comes from a discipline outside programming language design. And doesn't necessarily value the same things that programming language designers do when those are contrary to the design he's trying to complete.

IMO, things like that -- although often they fail -- are valuable experiments and often yield one or two innovations that make the world better even if the overall vision doesn't. He's like a chair designer who thought more about the shape of human butts than the support engineering and what his elegant sculptured form and bold lines would look like in an architecture magazine. So maybe his chairs lack a solid balance, and tip over too easily, and aren't that elegant, but that seat cushion turns out to be a valuable innovation that nobody had been considering as something that might be important for chairs!

Ray

I would like to see more development of functions that can adapt to their context, i.e. representing a search in the function space similar to Coq strategies/tactics. What is normally called a 'function' today would then be a singular strategy. In some ways, this is analogous to a dictionary: a word or phrase can have many potential meanings but a 'best' meaning is chosen based on context of use.

Part of the compilation process would be selecting a concrete function - one that meets type requirements in context, and that optimizes other cost/preference/weighting criteria (which are also provided by the context). The 'search' for a concrete meaning is compile-time rather than runtime (though might be mixed a bit in cases of interpreters or live coding).

Usefully, a single function could have multiple types, and type-checking is valid if at least one of the types is valid.

I believe this sort of adaptive PL could make programming a lot closer to natural language, and namespaces more composable. The cost is separate compilation of libraries, but this could be mitigated by incremental compilation and caching.

[The `par` type, â…‹, from linear logic seems relevant to contextual adaptation.]

This strikes me as a very cool idea, but could you give an example of some namespaces it would make more composable?

For example, 'draw' could have multiple definitions in different libraries - one for artists, another for cowboys, and so on. The correct meaning for 'draw' would be used in context.

Overall, this makes namespaces more compositional... you can sort of dump multiple libraries into one big dictionary, which creates a bunch of ambiguity, but then the ambiguity has its own resolution mechanism based on context. (In cases where ambiguity does remain, a compile-time warning can be issued and developers can simply add a bit more context.)

In practice, this should result in a somewhat more terse language since little disambiguation is needed for namespaces.

I saw Gabriel's talk at SPLASH last year. I thought it was interesting, but very insular and meta with respect to the academic community, and not very applicable to the field at large. Ya, different people in the community have different ideas about what mixins are, but at the end of the day we are just arguing amongst ourselves. Somehow we've gotten ourselves stuck in a academic feedback loop with little input from or output to the "real world."

If we want to reintroduce system design into the scientific process, we have to work on recasting mere experience into some category of knowledge. What needs to happen for that is establishing a common vocabulary and some ground rules by which hypotheses can be formulated (and falsified).

I think Crista Lopes has perhaps a better description of the problem. My primary thought is whether we really should pretend to be doing science at all; the useful outputs of our field are generally in the realm of design, new engineering techniques, and mathematical theory. We can argue if theory is science, it really depends on your definition of the scientific process, but theory is based on absolute truth with respect to a model that may or may not represent the real world, and has little to do with the scientific process (though it often informs on it!).

We are going through an identity crisis: do we keep trying to shoehorn our field into a scientific method that barely seems to fit, and more importantly be useful, or do we go back to our roots of innovating, inventing, and reflecting? This debate is hardly unique to PL or computer science. I personally believe that the recent pushes for rigor have made our field much worse (just look at the noise in recent paper proceedings), not better.

wish there were places for radical experimental thought, that got good support and backup and funding etc., and then places that either refines pre-existing stuff with more rigor, or takes the dope smoking ideas and tries to see what rigor can be applied, to see if it makes things even chocolate+peanut-butter better.

Whatever, just give me papers that are interesting again! Apply rigor where needed and useful, not blindly as an end in itself. We will have to sacrifice rigor bars to increase interesting/relevant/useful bars; basically, we should reset our priorities.

I don't know whether programming language research has become so dominated by rigor/theory/formal systems as you two deplore, but it is also beside the point.

All I said is that you cannot equate industry experience (as is) with science; one needs to at least turn the insights from experience into something that can be communicated, that is reproducible. Call it "hypotheses that are falsifiable".

All over the world people are in fact learning new stuff about languages, about systems, and some of it is general and would be interesting and useful. Somebody needs to find it out and write it up. There may be navel-gazing, also fragmentation in scientific disciplines, but that has not prevented good scientists from appearing and surprising everybody.

Mainstream programming languages and systems maybe do not look like it, but they are all built by people standing on the shoulders of giants. The relative value of a real world system is quite relative, it shifts over time and what is innovation one year is merely considered technical debt next year, but foundations do indeed live on. It is not the phd theses themselves, but the authors' ability to understand what is around them and apply this knowledge.

There could certainly be more direct knowledge transfer in both directions, but to say that there is none at all isn't true. I think it would be a worthwhile effort to document and codify some of the industry experience and engineering practices into some form that allows judgments -- and if these judgments satisfy basic requirements, then I don't think anybody could claim that this wasn't science. Hypotheses may be a lot weaker than "Any design based on X is going to be better than a design based on Y", but they still have to codify knowledge and teach the reader something that they didn't know or couldn't articulate before.

Finally, I think many people (especially my former phd student self) are tempted to place science as somehow morally higher than engineering and industry practices (that Crisa Lopes post has many examples). It may be about solving different kinds of problems, but ultimately it is problem solving all the same. There is no general language of problem solving, but that doesn't mean that we won't see new languages (both terminology and PL) and new results at those intersections.