Lambda the Ultimate

Maybe I just don't know the magic words to type in, but I was curious if there are any languages which are designed to specifically operate on or describe trees.

Of course, I'm aware of XSLT, but I can't help but think there's more. Unfortunately thats all it seems I can find that comes close. I would really like to know what alternate approaches there are, and as always, any good theoretical justification for the constructs would be nice too.

Subcontinuations. Robert Hieb, R. Kent Dybvig, Claude W. Anderson. Lisp and Symbolic Computation 1993.

...traditional continuations are not useful in the presence of concurrency, because the notion of the rest of the computation represented by a continuation does not in general make sense...

Subcontinuations may be used to control tree-structured concurrency by allowing nonlocal exits to arbitrary points in a process tree and allowing the capture of a subtree of a computation as a composable continuation for later use.

Strangely enough this paper wasn't discussed here, even though it was mentioned in the discussion group a long time ago. Now's the time to rectify this omission.

(via Daily Python URL)

Candygram is a Python implementation of Erlang concurrency primitives. Erlang is widely respected for its elegant built-in facilities for concurrent programming. This package attempts to emulate those facilities as closely as possible in Python. With Candygram, developers can send and receive messages between threads using semantics nearly identical to those in the Erlang language.

(via Phil Windley)

This Dr. Dobbs article describes how tuplespaces can serve as an alternative to web-service message passing APIs.

A nice explantion of the Linda programming model.

Does any programming language (including those embedded in statistical analysis packages) let you specify the domain of trig functions, or restrict them by default to a single cycle (eg 0-360 degrees)? I was reading this (please ignore the politics and point-scoring involved unless you enjoy that kind of thing) and wondered how common such errors were - I've certainly done similarly stupid things.

Another (better, since it would catch radians used as degrees, as well as being more general) solution would be physical units within the type system (although angles are dimensionless, so you'd need quite a pedantic system, I would guess).

((Unit) Tests pick up problems like this, of course).

Types and Reflection by Lauri Emil Alanko.
If you're interested in reflection or dynamic loading in statically typed languages, this is worth reading.


One of my favorite parts of this thesis is the dynamic loading section, along with discussion of the strengths and weaknesses of Haskell's Data.Dynamic, Template Haskell, and Don Stewart's hs-plugins.

Personally, I've been trying to figure out how to get elisp quality source evaluation with Haskell, and this thesis goes a long way towards answering my outstanding questions.

The "part II" thread was getting too long, so here beginneth part III. For ease of indexing, the prior two threads are:

• Why type systems are interesting - part II
• Why type systems are interesting

This post is a response to Frank's recent post, "I say we shall have no mo' "latent types"..." (here's the same post in context). The first couple of points below are tangential, but after that comes my defense of the syntactic aspect of latent types that I've been discussing.

Frank Atanassow wrote:

You are conflating dynamic loading of untyped code with dynamic loading of typed code. They are not the same thing, and untyped languages only support the first, and typed languages can easily accomodate dynamic loading of Univ code.

In practice, typed languages are not usually used like this, probably because of convenience and practicality. See next point.

I find it very irritating that people continually bias their arguments for untyped languages in this fashion, as if typed languages need to "catch up" or something.

Are there any typed languages for which highly dynamic IDEs exist, along the lines of those for Smalltalk or Self? If so, I want to play with them! If not, then what I was saying was not biased, since these are examples of "what current realistic implementations are capable of in terms of dynamic loading and so on." (Lauri Alanko's thesis seems relevant here.)

But this relates to the previous point: as long as DT languages ignore their type systems

Untyped languages don't have type systems.

I wrote "DT", you wrote "untyped". That's part of the stacked terminology deck here: I'm quite happy to agree that an untyped lambda calculus has no type system. But DT languages aren't untyped lambda calculi. A simple demonstration of this is the existence of soft type inferencers for languages like Scheme and Erlang.

Does the existence of these soft typers mean that Scheme and Erlang should be considered typed languages? Or are they untyped languages when you don't run the soft typer on their programs, and typed languages when you do? It makes much more sense to say that these languages have latent types, i.e. their programs have types which can be inferred by a soft typer. More importantly, and much more commonly, those types also inferred by the programmer.

Further, the situation is made even less black and white by the fact that an inferencer can't, without any hints, discover all the types - and I mean real, syntactic types - present in these programs. I'm not saying that all of the "program properties" which you referred to are types, but some of them are. An inferencer produces an approximation which can typically be improved by a programmer.

This is something else I find irritating, Anton. I spent many, many hours explaining exactly why and in what sense this is true,

If you have explained in what sense "Untyped languages don't have type systems" is true, then either my points above must fit into your explanation somehow, or one of our positions is erroneous.

and I thought at last that people had started to grasp what a type is, what it is not,

If people have really grasped what a (syntactic) type is, then what I am saying should make sense to them -- that is, even DT programs contain latent type information, as evidenced by the fact that at least some of this information can be mechanically extracted. Further, this information is depended on by programmers when reasoning about their code.

My opening forum post in the prior thread was intended to made the case that type systems were interesting because of their utility when it comes to reasoning about code, and that this kind of reasoning takes place in DT languages as well as in static languages, which is why type systems are relevant even to DT programmers. I still consider that to be true, and I don't think any good evidence has been given to contradict it.

As a nice example of this in action, this LL1 post quotes a claim by Joe Armstrong, talking about a type-checking phase being applied to previously written Erlang programs: "The type system has uncovered no errors. The kernel libraries were written by Erlang 'experts' -- it seems that good programmers don't make type errors."

Joe ignored the fact that even good programmers do make type errors, but that these errors are ultimately caught, even if only at runtime, and corrected. The result of this process is that even DT programs can, and do, end up with consistent type schemes. Of course, to statically prove that, we have to do something like successfully run a type inferencer on the code. However, even if you fall back on some kind of Heisenberg-like effect, e.g. "type systems/schemes don't exist until you formally specify them", the fact remains that human programmers - aided by a debugging process - "somehow" end up creating valid type schemes. I quoted "somehow" because I don't think it's any mystery - they're reasoning about the program's types, albeit along with other program properties, to come up with working programs, which tend to have (or even must have) valid type schemes.

and what the relationship between typed and untyped languages is.

I'm actually not sure what your explanation is in this respect. We've seen that Univ isn't a complete explanation, and I don't think I've seen an alternative explanation of the relationship from you. In your defense, the usual type theory sources don't have much to say about this either. It's fine if you want to say that you prefer to stick to pure syntactic types, where you have formally specified type systems and languages and there's absolutely no ambiguity. It's also fine if you want to say that you're happy to restrict yourself to being able to embed DT programs in statically typed languages using a unitype. But as soon as you extend your claims beyond these very precisely-defined ones, and want to say anything about the nature of DT languages and their relationship to types, then what I've been talking about enters the picture.

Now you are diluting my message with your talk of "latent type systems."

I'm trying to discuss the relationship between syntactic types and DT languages. There obviously is a relationship, and to me it seems quite a bit deeper than most type theory explanations give it credit for. Traditional type theory doesn't seem to offer much to explain the abovementioned Erlang experience, for example.

If this dilutes your message, I suspect it's only because the message needs to be more clearly delineated along the lines I mentioned above, i.e. that you're only talking about types that are fully formally specified. However, you can't claim that types don't exist outside those boundaries, only that our formal descriptions of them are often incomplete, etc.

As far as I can tell, your notion of "latent type" only amounts to program properties which might be extractable with some blue-sky theorem prover, or more realistically a proof assistant being manually operated by a type theorist.

...or with a soft typing system assisted by hints from a programmer, which is much less blue-sky. But I'm not just talking about some theoretical future possibility: I'm saying that DT programs succeed, in part, by virtue of their programmers creating valid latent type schemes for them.

In particular, as a notion of "type system", latent type systems fail the "tractable" and "syntactic" conditions which you yourself quoted from Pierce.

Soft typers seem to contradict this (although their developers might have something to say about tractability). In any case, Pierce characterizes his definition as "one plausible definition". Let's look at what else Pierce says:

Pierce: "this definition identifies type systems as tools for reasoning about programs"

This applies to latent type systems: programmers use them for reasoning about their programs.

Pierce: "Another important element in the above definition is its emphasis on classification of terms -- syntactic phrases -- according to the properties of the values that they will compute when executed."

As I've pointed out, the need to statically classify terms applies to DT programs as well as ST programs. It is impossible, in general, to reliably invoke operations without such classification.

Pierce: "A type system can be regarded as calculating a kind of static approximation to the run-time behaviors of the terms in a program."

The word "approximation" reminds us that not everything needs to be known statically. DT type schemes are certainly likely to be more approximate than ST ones - there are likely to be many more cases in which the exact operation being invoked is only known at runtime. But a programmer can only reliably perform operations with some knowledge of the properties of the values being operated on, even if it's "approximate" (e.g. expecting that an object accepts the "print" message). Do these properties always qualify as types? Presumably not - in some cases, they go well beyond what traditional type systems are capable of - but some of these properties do qualify as types.

Another way in which latent type systems mirror more traditional static type systems is that they're used to reject programs. However, the programmer has more discretion in this case than when rejection is performed mechanically. Rejection nevertheless does occur - there are many ways in which DT programs are designed to make sense from a type perspective, thus effectively rejecting alternative programs which make less sense. As I've previously pointed out, in some circles it's common practice to annotate functions with their type as a comment. Programmers constantly make design decisions which center around consistent usage of types.

I like Lauri Alanko's take on type systems, from his thesis referenced above, section 2.2:

Alanko: "A type system is a method for analyzing a program syntactically to prove the impossibility of certain erroneous conditions. It is based on types, syntactic structures that usually represent the sets of values which expressions can evaluate to. The type system works by assigning types to the expressions and variables of a program, and by checking that expressions are combined properly so that their types are compatible".

That entire description maps very well onto DT languages, with one change: "prove" usually becomes a weaker assurance, more like a theory of the program's types, which represents the best available knowledge at any given time, but may yet be falsified in future, requiring improvements to the theory. These activities are performed by the programmer, instead of mechanically, with assistance from runtime errors based on tagged values. These runtime errors are falsifications of the current theory, and their absence in the face of testing provides reasonable assurances as to the validity of the current theory of the program's types, among other things.

Physics vs. Mathematics

Based on the perspective in the previous paragraph, one can see DT programming as being more like physics, to ST programming's mathematics. Physicists are used to having theories that could be proved wrong at any time, by some previously untested special case. They even use theories that they know are wrong in some respect, that don't perfectly match observations. They put up with this because they have no alternative, because they are modelling "real" phenomena which have characteristics which can't simply be formalized away.

The areas which currently rely heavily on DT languages are rife with such characteristics, often having to do with complex interoperation between disparate systems, such as networks, databases, web servers, operating systems, and other programs. In these environments, the evolving-theory approach to development is often essential, and it's fairly natural that the type system aspect is simply fitted into this approach, even if theoretically better solutions exist.

Responding to one final comment of Frank's:

Instead of jumping on the type bandwagon, why not call your "latent types" "program properties"? Or, if you think they are different, please demonstrate how.

This isn't about jumping on any bandwagon. If the above doesn't explain my position sufficiently clearly, or credibly, tell me what kind of demonstration is wanted, and I'll see what I can do, within reason.