Lambda the Ultimate

How do modern static type systems deal with imperfect knowledge? For instance, do they require that you declare the type of all values before you can use them?

The most obvious answer to that is to point out that modern static type systems use type inference, so that you don't have to declare the types of all values. In fact, being required to explicitly declare the type of a value is usually the exception, not the rule. If you've never seen this in action, I'll give an example -- in SML, you might define a string length function as follows:

fun strlen s = length (explode s);

val strlen = fn : string -> int

IOW, strlen is a function which accepts a string and returns an integer. SML knows this because it knows that the type of explode is string -> char list, and it knows the type of length is 'a list -> int, where 'a represents a type parameter, i.e. length accepts a homogenous list of any single type of value. Given these two types, it's easy for the system to figure out the type of strlen as string -> int.

Entire programs are typed like this, without necessarily requiring a single explicit type annotation. But they're also checked for consistency, which means if you have imperfect knowledge about the types in your program, by the time you've gotten it to compile successfully under a statically-typed language, your knowledge will be perfect. ;)

Can you change your mind about the type of a value?

Can you disagree with (and override) the type of a value passed to you from someone else's code?

I agree that being able to automatically validate my use of values could be useful at times. But this should be optional.

Do you mean optional to do it statically? After all, even dynamically-typed languages generate type errors if a value is misused at runtime. Type-checking in some form is not optional, in any language. If you're saying it should be optional as to whether it occurs statically, i.e. at compile time, that raises the question of why. Are their cases where you need to perform an operation on a value without knowing for sure that the operation is valid on that value? If you know an operation is valid on a particular value, then you know something about that value's type. You may only know its interface or, in Haskell terms, its typeclass, but that's enough for a type system to go on.

As I mentioned in my earlier post, fully static typesystems, like those in Haskell and ML, do impose constraints: there are programs that will run successfully in a dynamically-typed language, that won't even typecheck statically. That can be a good thing: many poorly designed programs won't typecheck, if they don't use types well. But it can also be a limitation, when you want to do something that confuses a static typechecker.

An interesting area is soft typing, in which programs with few or no type annotations are analyzed, and the types of their terms inferenced. Such systems don't stop you from trying to run the program, but depending on what they find, you may think twice about running it anyway. This gives you a kind of optional typing. PLT Scheme has a couple of systems which support this, MrSpidey and MrFlow. Frank also mentioned a soft typing system for Erlang the other day.

In software systems, it's almost always of benefit to be able to factor systems into naturally separate components, and the type scheme of a program is one such component, which is very naturally orthogonal to the rest of a program's semantics. In a sense, a program's type scheme is the framework within which the program runs, even in DT programs. If you don't have a good language with which to describe the type scheme, think about it, and manipulate it, you're at a disadvantage. That, of course, is why it's common to annotate functions with their types, even if it has to be done in comments in a DT language.

fully static typesystems, like those in Haskell and ML, do impose constraints: there are programs that will run successfully in a dynamically-typed language, that won't even typecheck statically.

If I run a Haskell program through a Scheme compiler, and vice versa, I will almost certainly get a syntax error, so I assume you have some translation in mind. Further, I venture to guess it is a translation which involves mapping lambda to backslash and so on.

But this omits the types, and a Haskell program is not an untyped program, it is a typed program abbreviated by letting the type inferencer reconstruct the types, a process which is deterministic in the sense that each term has a unique principal type. So the types are part and parcel of the program, and we should rather compare the type-annotated version of a Haskell source program with a Scheme program.

How to do this is not obvious. You have at least two choices.

First, you can erase the types. Of course, this amounts to saying that the types are pointless in the first place, so it is inherently biased to the DT assumption that all that matters about a program is what it does at run-time. (If types are used at run-time, as for example in eta-expansion/reduction, it is also wrong.) This is like doing complex arithmetic with a conventional calculator, by ignoring the imaginary part of a number; it only gives you half the answer, and to say otherwise is to disavow the significance of imaginary numbers.

A second option try to preserve the types. This involves finding an embedding of typed programs in untyped programs, and vice versa. Finding an embedding of untyped programs in typed programs is very easy: you just define a universal type, and I have shown several times how to do it. Finding an embedding of typed programs in untyped programs is not easy, and I strongly suspect it is impossible. To get a result, I think one needs to admit a weaker notion of `embedding', and effectively stage the run-time behavior so that there is an early stage corresponding to static checking and a late one corresponding to `actual' run-time. And then what have you got? It's just a typed language again.

So there is no magic in dynamic typing, and no advantage. Furthermore, given the fact that every untyped program is a typed program of a universal type Univ, there are no limitations associated with static typing. In fact, inasmuch as it is harder to design and write a static type checker/inferencer than it is to design and write Univ, static typing saves work.

I've said it before and I will say it again, until people stop repeating the party line and start using their brains.

• Static typing is superior to dynamic typing in every way.
• Static typing imposes no limitations.
• A typed program is not an untyped program.
• In a language without type inference, erasing types erases information.
• A program is not its run-time behavior, and software development activities (designing, analyzing, transforming, refactoring, debugging and optimizing programs) are all static activities.

In isolation what you say is no more satisfying than "all turing-complete languages are the same." In some sense they're the same, and in some sense static types are superior, but in what sense is this meaningful to a programmer?

Would you care to relate those comments to the development of computer programs using currently available tools?

The only tool you need is the one between your ears. Here are some examples.

If your compiler tells you that a value M has type T then you know immediately the operations which can be applied to it.

You also know some, and sometimes, all of the laws that M satisfies. For example, if M has type A * B then in ML you know that:

(#1 M, #2 M) = M

And if M has type 'a -> 'b, then you know (by parametricity) that, for any relation P, if P(x,y) then P(M x, M y).

Furthermore, often you can `guess' the meaning of a value by looking at the type. What do you think M is/does/means if it has one of the following (principal) types?

string -> int
file_descriptor -> string -> unit
('a -> 'b) -> 'a list -> 'b list
'a -> int -> 'a list
('a -> 'a) -> 'a
'a -> 'a
('b -> 'c) * ('a -> 'b) -> ('a -> 'c)

Sure, your guess may be wrong (except the last two—there is only one possibility), but it narrows down the possibilities and tells you what to look for in the code to confirm your guess.

Conversely, if you are writing a program and you have determined that it must have type T then you know immediately the operations which construct it. You know, for example, that if you want to write a term of type A -> B -> C * D then you only need to fill in the blanks in:

fn a => fn b =>
  let val c = ___
      val d = ___
  in (c,d) end

Continuing on with tools, do you claim the IDE should autogenerate

fn a => fn b =>
  let val c = ___
      val d = ___
  in (c,d) end

for you, given A -> B -> C * D? Essentially then, you are proposing a sublanguage which may generate common patterns of code. (And even more information may help things along.) Is this a correct inference, or am I completely mistaken?

Often there is a shorter or more natural way to write a definition. For example if I want to implement add2 : int -> int I can write:

add2 = fn n => n + 2

add2 = twice add1

add2 = fn n => (twice add1) n 

I want the option to be able to write either, and then select an expression, click "eta-expand" or "eta-reduce" and get the other. Similarly for beta-compatibility, and all the other equational axioms. And I want the ability to define "tactics" like fusion, promotion, deforestation and so on by combining axioms into laws. In short, I want to be able to manipulate my program in every way which is sound according to its semantics.

I wouldn't call this "code autogeneration", but rather program transformation.

To see an example of this sort of thing, look at pi-RED/KiR.

There is not only one possible value of the types

  'a -> 'a
  ('b -> 'c) * ('a -> 'b) -> ('a -> 'c)

because ML "functions" are nondeterministic, may have side effects, and do not necessarily terminate.

Yes, you're right. At first I thought to avoid this by choosing a CBV language, but midway through I realized that doesn't help, so imagine them as types of values in a pure terminating language like Charity.

(But I think you are wrong about "nondeterministic". Maybe there is something in the SML Standard Basis and probably in OCaml's standard library which makes functions nondeterministic, but I think I only said "ML", so I was sufficiently vague to cover my ass. :)

Of course they are nondeterministic in ML. All MLs I know of allow I/O, so your computation can be affected by the outside world.

Finding an embedding of untyped programs in typed programs is very easy: you just define a universal type, and I have shown several times how to do it.

if b then 42 else "ha!"

if b then Num 42 else Str "ha!"

...where Num and Str are type constructors for the Univ type. This is kind of ironic, considering that it's the latter language that's supposed to be able to inference types.

You can think of dynamically-typed languages as a shortcut syntax for creating programs which rely on a universal type. This demonstrates that statically-typed languages can be less expressive than dynamically-typed ones.

There's also the issue of late binding which Dominic raised. It's possible to deal with these issues in statically-typed languages, but afaik Haskell and ML don't have good solutions to this. Part of the point I was making was the distinction between what ought to be possible with static type systems in theory, and what actually is possible with existing "mainstream" functional languages.

To elaborate on that a bit, there are a lot of programmers today who mainly have experience with dynamic typing, or who like it best of what they have experience with. When compared to alternatives like Java or C++, it's obvious why they prefer DT. However, they may also look at the ST functional languages and also find they're more restrictive than they're used to. Part of what I'm saying is that it doesn't necessarily have to be that way, or at least not to the extent it is now. There's evidence of this in some other languages, including apparently languages like Boo and perhaps Clean (speaking totally from hearsay).

It's de rigeur here to say that DT fans shouldn't let languages like Java and C++ turn them off static typing. I'm taking that a step further, and saying that to some extent, the same applies to languages like ML and Haskell. These languages are first generation, or perhaps zeroth generation, from the perspective of making type systems friendly.

First, you can erase the types. Of course, this amounts to saying that the types are pointless in the first place

This is like doing complex arithmetic with a conventional calculator, by ignoring the imaginary part of a number; it only gives you half the answer, and to say otherwise is to disavow the significance of imaginary numbers.

You haven't justified why omitting the types would be as bad as that, so the analogy is groundless. A better example might be one Felleisen once gave: it's like doing physics calculations without explicitly writing down the units of the values. You're not (necessarily) disavowing their significance, you're simply recognizing that it's not necessary to be explicit about it in every instance, or require that the units always be inferrable from any expression.

People take shortcuts all the time. That's precisely why type inferencing exists. The reason we're having this discussion is that type inferencing hasn't achieved the same degree of convenience, in all respects, as dynamically typed languages offer.

Furthermore, given the fact that every untyped program is a typed program of a universal type Univ, there are no limitations associated with static typing.

I agree with Luke, this is essentially a Turing equivalence argument which ignores expressivity and convenience, which impacts overall usability, and is important.

The fact that one has to create and use types in situations where no action is required in a dynamically-checked language, is a constraint. In practice, the statically typed languages we're talking about don't provide support for using a Univ type throughout the program (although some languages with less "modern" type systems do do this.) In addition, use of a Univ type leads to having to do things explicitly that are done implicitly for you in dynamic languages. I think the claims of "no limitations" would have more force if there were more statically-typed languages which cater to the more expressive programming styles which dynamically-typed languages enjoy.

In fact, inasmuch as it is harder to design and write a static type checker/inferencer than it is to design and write Univ, static typing saves work.

I've said it before and I will say it again, until people stop repeating the party line and start using their brains.

• Static typing is superior to dynamic typing in every way.

The definition of "superior" here is apparently based on technical considerations that ignore human factors, i.e. it's "superior" if it's Turing-equivalent but has greater information content. This view isn't going to win many converts - remember, programs are written, read and maintained by humans.

Besides, I think the whole nature of the comparison is wrong. You can certainly see dynamic typing as being subsumed by static typing - but in that case, you have to concede that dynamically-typed languages provide a convenient way of generating a certain kind of statically-typed program. Until statically-typed languages are as convenient in this respect, claims of superiority "in every way" are equivalent to saying "the Emperor is fully clothed!" even though his pimply ass is hanging out. ;)

• Static typing imposes no limitations.

• A program is not its run-time behavior, and software development activities (designing, analyzing, transforming, refactoring, debugging and optimizing programs) are all static activities.

I agree - or at least, all these activities have static components - and it's one reason why type systems are interesting and important. However, I think the designers of "modern" static type systems and the languages which use them are in some respects least aware of these issues. They've done a great job of getting the formalisms right, but seem to have expended much less effort on human factors, except where they impact certain target application domains, such as scientific and mathematical applications.

the resulting typed program is - in languages like Haskell and ML - larger, having been annotated with type constructors for the universal type... This is kind of ironic, considering that it's the latter language that's supposed to be able to inference types.

What has it got to do with type inference? Haskell infers correctly that 42 :: Integer and Num 42 :: Univ. And that is because, under a faithful interpretation, the meaning of the Scheme value 42 is not the Haskell value 42, but rather Num 42.

You can think of dynamically-typed languages as a shortcut syntax for creating programs which rely on a universal type. This demonstrates that statically-typed languages can be less expressive than dynamically-typed ones.

It's true that Scheme, Perl, Python, etc. have a more concise syntax for untyped programs, and that the embeddings of untyped programs written in Haskell, ML, C, etc. are longer. But that has nothing intrinsically to do with static typing, but only the syntaxes of those languages, which are, naturally, optimized for typed programs.

The embedding is a computable function; it can be automated. It ought to be a simple matter to implement some syntactic sugar which lets you designate an expression as `untyped', perhaps by quoting it. This would just be expanded to a normal expression, inserting constructors at the appropriate places. It's a completely syntactic (and moreover local) procedure, which could be implemented by a macro system.

Haskell, ML, etc. don't support this, but they could, and perhaps they should, at least for pedagogical reasons.

Let me put it this way. You said, "dynamically-typed languages [provide] a shortcut syntax for creating programs which rely on a universal type," and that is true. They provide such a syntax, because their semantics is not sophisticated enough to express typed programs.

Statically typed languages, on the other hand, possess a semantics which is sophisticated enough to express both untyped and typed programs but, because typed programmers are generally not interested in writing untyped programs, there has been little impetus to provide a convenient syntax for them. It does not follow that static typing itself precludes such a syntax.

Having said that, I think there is an issue to be addressed here, and that is the interface between typed and untyped programs. When a typed function, say, is passed an untyped value, there is nothing one can do but check explicitly that the value has the right type. However, when passing a typed value to an untyped function, say, one ought to be able to insert the required coercion automatically. This is something I would like to be able to address in Arrow. (In terms of the quotation syntax above, this means that if quoted code mentions a variable bound outside the lexical scope of the quotation, if you know its type, you can automatically insert the proper coercion to Univ.)

there's also the issue of late binding which Dominic raised. It's possible to deal with these issues in statically-typed languages, but afaik Haskell and ML don't have good solutions to this.

I didn't grasp what Dominic's message had to with static vs. dynamic typing, or why adapters should be less necessary in an untyped language. Perhaps you or he can explain with a simple example.

Part of the point I was making was the distinction between what ought to be possible with static type systems in theory, and what actually is possible with existing "mainstream" functional languages.

OK, but that is not a distinction I am making. I am talking about static typing itself, and not the extant statically typed languages. OTOH, I don't think I don't think I am claiming anything which is difficult to implement.

It's de rigeur here to say that DT fans shouldn't let languages like Java and C++ turn them off static typing. I'm taking that a step further, and saying that to some extent, the same applies to languages like ML and Haskell. These languages are first generation, or perhaps zeroth generation, from the perspective of making type systems friendly.

Perhaps so.

But if they are unfriendly, part of the reason for that is that so many people regard an ST language as merely an untyped language with a safety net, and then it becomes human nature to ignore the net. My point is that types are not like a safety net; they're more like a skeleton, and values are the flesh that grows around them.

So if typed languages are unfriendly, it's wrong to criticize them by pointing to untyped languages, because 1) untyped languages can't even address the problems which typed languages can, while 2) typed languages address all the problems which untyped languages do.

Maybe the way types are treated can be improved, and maybe not; but if it can't, there is nothing magical about untyped languages which can solve the problems which types address. If you draw a Venn diagram, untyped languages are a circle inside typed languages; they're not just overlapping—one is a proper subset of the other.

Not so. [Erasing types] amounts to saying that it's not always essential to annotate the code with them, or that it be possible to statically infer them.

Right, I was mistaken. But it is a fact that it is impossible to statically infer types for all untyped programs.

Moreover, there is a subtle difference between the types one can infer for untyped programs, which are Curry types, and the types one can infer for typed programs, which are Church types. I cannot quite put my finger on it, but I'll post it later when I can articulate it.

You haven't justified why omitting the types would be as bad as that, so the analogy [real:complex::untyped:typed] is groundless.

A complex number has a real and an imaginary part; a typed program has a static and a dynamic part. A real number has no imaginary part; an untyped program has no static part.

(However, I am starting to think that the issue is not "static" vs. "dynamic"; it is something deeper, Church vs. Curry.)

A better example might be one Felleisen once gave: [erasing types is] like doing physics calculations without explicitly writing down the units of the values.

Ah, nice example! Let me tell you why I disagree with it. (In short, I think doing calculations with units is like dynamic typing.)

When you do a physics calculation like that, you are using numbers to denote some physical quantities. They stand in for those quantities, but are not those quantities. A mass is not a length, though they both have magnitudes which can be expressed as numbers.

When you do a calculation without dimensions (units), you are calculating with those magnitudes, and you have to remember in your head where each number came from to avoid coming up with something meaningless. This is like programming in an unsafe language like assembler. (In fact, in some sense every result computed this way is meaningless; it is only your brain which assigns a meaning to it.)

When you do a calculation with dimensions, every magnitude is tagged with a dimension. (Sound familiar?) You are still doing arithmetic on the magitudes, though; they don't serve any useful purpose except to notify you when you've committed an error. This is like dynamic typing.

Static typing is different. It's like doing arithmetic not on the magnitudes, but on the quantities themselves. So, there is one addition operation for mass, one for time, one for length and so on. And, there is one multiplication operation for each pair of dimensions, and so on. And each sensible composition of such operations is an operation of a certain dimension. (And constants are nullary operations.) In such a system, it is impossible to make a dimensional error. So that is static typing.

In algebraic terms, static type systems regard mass arithmetic and length arithmetic like algebras of the same signature (that is, supporting the same operators), which are unequal but isomorphic. Because they're isomorphic, they can be represented using the same carrier (magnitudes—say, reals).

There is much more to say about this example, but I haven't the time right now...

People take shortcuts all the time. That's precisely why type inferencing exists. The reason we're having this discussion is that type inferencing hasn't achieved the same degree of convenience, in all respects, as dynamically typed languages offer.

Type inferencing is not comparable to dynamic typing. A mass is a mass, no matter how I notate it. A magnitude tagged with a dimension is not a mass; it is a representation of a mass. The dimension marker tags it as a mass, and if I erase it, I've not only forgotten it is a mass: I've really transformed it into a scalar.

Thus the difference in a typed language between 42 and Num 42; type inference cannot recover that tag information because there is no information to recover. This is in contrast to the difference between 42 and 42 :: Integer; here the type annotation is superfluous, because 42 is an Integer with or without it.

The fact that one has to create and use types in situations where no action is required in a dynamically-checked language, is a constraint.

One doesn't. Give an example. I bet that when you write "situations where no action is required" you are comparing two situations which are not actually comparable.

In practice, the statically typed languages we're talking about don't provide support for using a Univ type throughout the program (although some languages with less "modern" type systems do do this.)

What do you mean by "support"?

) In addition, use of a Univ type leads to having to do things explicitly that are done implicitly for you in dynamic languages.

That's just syntax which can be addressed by syntactic sugar as I described.

I think the claims of "no limitations" would have more force if there were more statically-typed languages which cater to the more expressive programming styles which dynamically-typed languages enjoy.

Untyped languages are less expressive than typed languages, since they limit you to only expressing dynamic behavior.

But you are talking about "styles". I do not understand what it means for a language to "enjoy" a programming style. Do you mean styles which are popular in a programmer community? And if so, which, and how are they more expressive (and than what?)?

IIUC, the work you're talking about saving [designing and writing a type checker/inferrer] is the exact same work that's already saved by DT languages.

No, because, for the umpteenth time, a program is not its runtime behavior.

Hiring someone to mow your lawn saves work. Not owning a lawn does not "save work".

The definition of "superior" here is apparently based on technical considerations that ignore human factors, i.e. it's "superior" if it's Turing-equivalent but has greater information content. This view isn't going to win many converts - remember, programs are written, read and maintained by humans.

Ah, here we go again.

I disagree; I believe it is based on technical considerations which address human factors.

Apple is well known as a company that tries to address human factors. They've made a big deal about direct interaction; you move a folder by dragging it, for example. In contrast, in CLI you write down an expression which more indirectly represents that action.

In the same way, it is better and more intuitive to do arithmetic on masses than arithmetic on tagged scalars which only represent masses.

And in the same way, it is better and more intuitive to declare a tree datatype, than to encode trees by representing them as nested s-expressions. And it is better to have a class of values which are integers than a class which only represents integers. (I am overemphasizing "are"; a tree datatype still only "represents" the set of trees, of course, but it does it more precisely than you can in an untyped language.)

Besides, I think the whole nature of the comparison is wrong. You can certainly see dynamic typing as being subsumed by static typing - but in that case, you have to concede that dynamically-typed languages provide a convenient way of generating a certain kind of statically-typed program.

Yeah, I agree with that. Only, that certain kind is not a kind which is no longer of much interest when you acquire the ability to express typed programs.

["Modern" ST language designers]'ve done a great job of getting the formalisms right, but seem to have expended much less effort on human factors, except where they impact certain target application domains, such as scientific and mathematical applications.

I disagree. I think modern static type systems address a sweet spot in human factors that has gotten large returns, whereas untyped languages like Perl, Python and Ruby have just been nibbling at the edges, by permuting and composing syntax, where returns are minimal.

Dim objDoc
objDoc = CreateObject("Word.Application")
objDoc.Open(strFilename)

1. Simulate dynamic dispatch via reflection, or
2. Write adaptor classes for each of the different versions of Word we might find on the target system.

There is a shadowy figure in the background here: COM, which actually does supply some interfaces that all COM objects share - it's a kind of universal adaptor, which is what makes the standard late-binding behaviors of VBScript and VBA work the way they do.

Now wash your hands.

So what gets passed in for the omitted parameters? For each version of Word that requires more than just a filename, there must be a semantics for calls which omit those additional parameters. Or do you just get errors?

There's a special value, called "Missing", that's passed in instead (and typically replaced, at the other end, by some default value).

About VBScript example: how about a static-typed language bundled with library which is equally powerful as VBScript library. So we could type with a few additional keystrokes:

COMObj objDoc = COMObj.create("Word.Application");
objDoc.invoke("Open", new COMData[] { new COMString(strFilename) };

Therefore, when writing pieces of code which merely glues together some external technologies (and certainly over 95% software produced falls into this category), static typing is badly hindered. But if your software really does something on its own, static type system is your friend.

For example, in some project I work on (~100kloc so far) the relevant logic is isolated from external technologies (gui, i/o, db, ...) to the extent that over 75% of source code is so independent that it works well with J2SE as well as .NET (most people cannot imagine it is possible). In that case static typing rules.

With type inference the example would be different. If we had such library* in Haskell it would look like:

create :: String -> IO COMObj
invoke :: String -> [COMData] -> COMObj -> IO COMObj
strFilename :: String
x # f = f x
fun strFilename =
    do {
        objDoc <- create "Word.Application";
        objDoc#invoke "Open" [COMString strFilename];
    }

The only extra typing we have to to do is using the COMString constructor and the square brackets to simulate an arbitrary number of parameters. AFAIK the VBScript example would require an almost equal number of characters. We could make the Haskell code terser using the ">>=" combinator if our goal is to save keystrokes:

fun strFilename = create "Word.Application" >>= invoke "Open" [COMString strFilename]

* I know that Haskell has COM libraries but I never used them so I don't know how they look like.

Frank goes a bridge too far when he says "Static typing is superior to dynamic typing in every way". Indeed it is superior, but only asympotically, for software big enough. For tiny scripts, there is little advantage to justify typing more letters.

Who says you have to type more?

An untyped programming language is a typed programming language with a single type, satisfying some conditions. Ergo, every untyped PL is a typed PL. Hence, for every untyped program there is a typed program. However, there are typed PLs, such as the simply-typed λ-calculus, which are not untyped. Hence there are typed programs for which there is no untyped equivalent. Hence static typing is strictly more expressive than dynamic typing. QED

(How many times do I have to repeat this?)

Update: Added code closing tag to try to stop runaway block in post above...

א₀? א₁...?

More static typing comes with a cost of more keyboard typing (proof by example). Even type inference won't negate that (extra COMString constructor). Every static type system I know has its own idiosyncrasies, forcing to use casts and adapters just to fit in it.

For example, there are two diffrent functions to get size of list and array in ML

List.size : a' list -> a'  
Array.size : a' array -> a'

And if the main task is to call a bunch of SQL queries and print some HTML, such an awkwardness is unneccessary and annoying.

BTW. I found that the "COMData" type in OLE Automation is called simply "Variant" - JACOB project does that.

For example, Scheme is dynamically typed, and has distinct length, string-length, and vector-length procedures. And, on the flip side, there is Haskell, which permits you to define a typeclass and define an overloaded size function, should you so wish.

Marcin Stefaniak: (Perhaps until you realise where your sophism fails.)

But it's not sophism: it's a formal result. Frank merely elided the proof in order to save time and space. It really is the case that non-universally-typed software is more expressive than universally-typed software. It shouldn't take more than an appeal to intuition to see this, IMHO: since types encapsulate constraints on behavior, it follows intuitively that a disjoint set of subtypes of the universal type will allow one to express behavioral constraints that can't be expressed using only the universal type.

Marcin: More static typing comes with a cost of more keyboard typing (proof by example).

I'd love to see this proof. Anecdotally, my own experience programming in shell scripts, Pascal, C, C++, O'Caml, Icon, Perl, 68K and Z-80 assembly language, Common Lisp, and Scheme fails to support this claim. Equally anecdotally, it isn't borne out by <http://alioth.debian.org/projects/shootout> if you change the weights to 0 for CPU, 0 for footprint, and 1 for lines of code. Of course, as various people have pointed out, the "code size" methodology is suspect; a better approach would be to, e.g. bzip2 compress the source code and compare compressed sizes. YMMV. Nevertheless, to a first approximation, the results are suggestive.

Marcin: Even type inference won't negate that (extra COMString constructor). Every static type system I know has its own idiosyncrasies, forcing to use casts and adapters just to fit in it.

To fit in what? Your point here seems to be about the boundary between a rich type system and, e.g. a C API. Such a boundary can indeed be difficult and even frustrating in the absence of a good FFI, but this says nothing about the expressiveness of typed vs. untyped languages. This is why I conclude that your argument isn't really about expressiveness, but about convenience.

Marcin: For example, there are two diffrent functions to get size of list and array in ML

whereas in untyped world one would do that with one function "size".

This is a singularly poorly-chosen example. Here is some perfectly valid O'Caml code:

size foo;;

Quick, is "foo" an array or a list? I confess that it's a trick question; I haven't given you enough information to be able to answer. That is, "foo" could be either an array or a list, because the size function is polymorphic. Type inferencing (in this case, taking advantage of functions not shown here, e.g. the constructor of foo) will determine which size is meant.

Marcin: And if the main task is to call a bunch of SQL queries and print some HTML, such an awkwardness is unneccessary and annoying.

Now I just have a hard time believing that you're serious. Here's the entire "prompt" example from the current postgres-ocaml distribution:

(* A simple replacement for psql *)

open Printf
open Postgresql

let _ =
if Array.length Sys.argv <> 2 then (
eprintf "\n Usage: %s conninfo\n" Sys.argv.(0);
exit 1)

let conninfo = Sys.argv.(1)

let print_conn_info conn =
printf "db = %s\n" conn#db;
printf "user = %s\n" conn#user;
printf "pass = %s\n" conn#pass;
printf "host = %s\n" conn#host;
printf "port = %s\n" conn#port;
printf "tty = %s\n" conn#tty;
printf "option = %s\n" conn#options;
printf "pid = %i\n" conn#backend_pid

let print_res conn res =
match res#status with
| Empty_query -> printf "Empty query\n"
| Command_ok -> printf "Command ok [%s]\n" res#cmd_status
| Tuples_ok ->
printf "Tuples ok\n";
printf "%i tuples with %i fields\n" res#ntuples res#nfields;
print_endline (String.concat ";" res#get_fnames_lst);
for tuple = 0 to res#ntuples - 1 do
for field = 0 to res#nfields - 1 do
printf "%s, " (res#getvalue tuple field)
done;
print_newline ()
done
| Copy_out -> printf "Copy out:\n"; conn#copy_out print_endline
| Copy_in -> printf "Copy in, not handled!\n"; exit 1
| Bad_response -> printf "Bad response: %s\n" res#error; conn#reset
| Nonfatal_error -> printf "Non fatal error: %s\n" res#error
| Fatal_error -> printf "Fatal error: %s\n" res#error

let rec dump_res conn =
match conn#get_result with
| Some res -> print_res conn res; flush stdout; dump_res conn
| None -> ()

let rec dump_notification conn =
match conn#notifies with
| Some (msg, pid) ->
printf "Notication from backend %i: [%s]\n" pid msg;
flush stdout;
dump_notification conn
| None -> ()

let listener conn =
try
while true do
let r, _, _ = Unix.select [conn#socket] [] [] 1. in
conn#consume_input;
dump_notification conn
done
with
| Error e -> prerr_endline (string_of_error e)
| e -> prerr_endline (Printexc.to_string e)

let main () =
let conn = new connection ~conninfo () in
print_conn_info conn;
flush stdout;
conn#set_notice_processor (fun s -> eprintf "postgresql error [%s]\n"
s); let _ = Thread.create listener conn in
try
while true do
print_string "> ";
let s = read_line () in
conn#send_query s;
dump_res conn
done
with End_of_file -> conn#finish

let _ =
try main () with
| Error e -> prerr_endline (string_of_error e)
| e -> prerr_endline (Printexc.to_string e)

For forming arbitrary XHTML: <http://theorie.physik.uni-wuerzburg.de/~ohl/xhtml>, although in the real world you'd want to use <http://wdialog.sourceforge.net> or <http://xcaml.sourceforge.net> to get the full benefits of a web application architecture.

So first I conclude that you're arguing convenience instead of expressiveness, and now I conclude that your convenience argument doesn't hold, either.

Even type inference won't negate that (extra COMString constructor).
Hmmm the constructor isn't something extra, it's because you need to project the string value into your datatype, because in Haskell we have a real String type, not something that is part of the "Univ" datatype. BTW we could solve that in a type system by allowing some form of subtyping.

Every static type system I know has its own idiosyncrasies, forcing to use casts and adapters just to fit in it.
And every dynamic language has its idiosyncrasies, forcing one to use runtime checks because it has no static behaviour.

And if the main task is to call a bunch of SQL queries and print some HTML, such an awkwardness is unneccessary and annoying.
I call this shenanigans. As Linus Torvalds said "Talk is cheap. Show me the code." Propose a problem where the type system and not the encoding used (i.e. used libraries)) "gets in the way".

Below some explanations.

1. I like static typing. I just don't agree with Frank's strict opinion. As a matematician he should be cautious with word "every"
2. Yes, PL expressiveness is not direclty related to source code size nor PL convenience, and that is where Frank's reasoning fails. The convenience is not formal concept, it is rather a psychological one, yet in real life it matters.
3. Code size is only a minor aspect of convenience and is varies greatly over diffrent PLs, I apologize for bringing it in the first time
4. ML example is for ML only. Other type systems are different; no point in examining all of them here
5. Paul: XHTML != HTML. And certainly it can be more convenient to write simple HTML as plain string than to learn an XHTML library
6. Paul: I regret to say the postgres-ocaml example shows no point for me
7. Daniel: I show no more code - the VBScript sample is good enough.
8. Daniel: why should I propose a problem without "used libraries" while I claim that it is linking with external technologies that mostly degrades static typing advantages.

like static typing. I just don't agree with Frank's strict opinion. As a matematician he should be cautious with word "every"

First, I'm a computer scientist, not a mathematician. However, I'm smart enough to see the value in applying mathematics to computer science.

Second, I am not abusing the word "every"; on the contrary, I'm using it fairly rigorously.

I've shown, several times, that every untyped PL is a typed PL. It follows that any property that holds of an untyped PL holds of a typed PL, including your lamentably vague "may be more convenient, especially for small tasks blah blah blah." :) So your claim is nonsensical unless you dispute the universal type translation. Typed PLs are not the complement of untyped PLs; they're a superset. You might as well claim that bleach blondes are less bald than people who are merely blonde.

Yes, PL expressiveness is not direclty related to source code size nor PL convenience, and that is where Frank's reasoning fails. The convenience is not formal concept, it is rather a psychological one, yet in real life it matters.

Yes, by placing the goal of programming outside the realm of formalization, you have demolished my (implicit) argument that static typing is a better means of achieving it. (Sorry, who was it again that accused me of sophism?)

Here is your argument: Money is not directly related to happiness. Happiness is not a quantifiable concept, but rather a psychological one, yet in real life it matters.

I absolutely agree with this sentiment. (Being poor, I have to believe in it. I imagine dynamic typing advocates are in the same boat.) Still...

If, as a stock broker, a client walks into my office, I can try to make them happy in several ways. I might kiss them on the lips and whisper sweet nothings in their ear. I might give them an inspiring lecture on the important things in life. I might give them a frontal lobotomy. However, as a stock broker, it is not my job to make my clients happy except by making them money. Not only that, but people might legitimately claim that I am not qualified to please my customers in any other way—and conversely that only stock brokers are qualified to manage your stock.

Similarly, as a programming language theorist, I can try to make you happy in many ways. I can give you a language which is fun and non-threatening, one that makes you feel good about yourself and validates your sense of self-worth and professional accomplishment. Or I can give you a language which is popular, say another Java or Perl knock-off with classes and built-in hash tables and regular expressions.

Will such languages be convenient for you? Probably. Do they help you write correct, efficient programs quickly? I cannot honestly say yes or no, because I can't prove it.

What I can prove is that programs of more expressive languages are shorter than ones of less expressive languages, that their behavior is more localized, that proofs of correctness are easier, etc.

You are, of course, free to dismiss the connection between such facts and the ultimate goals of programming; I admit they're heuristical. In your quest for convenience, you might instead consider consulting usability experts, psychologists and neurosociologists, or programmers with "over 25 years of experience in the field", or maybe your friendly neighborhood psychic.

All I can say is, I would not hire Dr. Phil to manage my stock portfolio.

Static typing is superior to dynamic typing in every way.

... and ...

Will such languages be convenient for you? Probably. Do they help you write correct, efficient programs quickly? I cannot honestly say yes or no, because I can't prove it.

These seem to be two conflicting statements.

The first statement is about statically typed languages. The second is out of context:

I can give you a language which is fun and non-threatening, one that makes you feel good about yourself and validates your sense of self-worth and professional accomplishment. Or I can give you a language which is popular, say another Java or Perl knock-off with classes and built-in hash tables and regular expressions.

Will such languages be convenient for you? Probably

Mathematical proof is only available within the realm of precisely defined mathematical constructs. Its power beyond those confines depends upon the closeness with which the mathematics models the thing being analyzed. This always includes non-mathematical considerations since if it did not then it would itself fall within the scope of 'mathematical constructs'. Computer languages as used by software programmers clearly fall outside mathematics since they exhibit a whole gamut of attributes (reliablity, readability, execution efficiency, ...) which cannot be mathematically formalized. So, although there are aspects of computer languages which may be closely modelled mathematically (syntax, scoping, typing, reduction, ...), to suggest that one can 'prove' anything about a computer language 'as used' is simply incorrect.

This simple observation reveals (to me at least) a great weakness in that argument that because dynamically typed languages can always be embedded into a statically typed language and the opposite is not true it follows there is genuine benefit for the programmer in static typing and conversely none in dynamic typing. (I hope this is an accurate summary of your position)

I don't know the details of how one might construct an argument to support the formal aspect of this assertion but if I were to attempt such a proof I would start by mapping each possible value in the dynamically typed language to a pair (T,v) in the statically typed language - T representing the value type and v being the value itself. The details are not important and I do trust that such a proof exists.

What any such formalism fails to 'model well' within the context of 'programming languages as used' is that for a significant number of programs possibly very few values originate with types which may be known statically. That is, programs must interact with other programs in ways which cannot be reasoned about statically. Clearly one can overcome this objection formally by reducing program I/O to well defined primitives (streams and bytes say) and have the program reconstitute such primitives into well typed elements of its own language. Of course, this is largely what does happen when two programs interact.

But there are two observations which must be made here. Firstly we have effectively traded static typing for a stream of unstructured data - that is we have lost the benefits of static typing in this scenario. Secondly the authoring of program code which facilitates such marshalling is difficult and in most practical scenarios programmers are wise to avoid it if possible.

Languages which do not rely on statically derived type information alone, but which enmesh values with their types at runtime may have benefits for inter-program communication because marshalling of the sort described above can assign types dynamically in a manner which is consistent with the runtime assignment of other types within a program. In fact languages which are loosely typed* may have even stronger benefits in this arena since program interfaces which are discovered at runtime can be reified as 'first class' values.

Therefore, given the above considerations, one might expect that dynamically-typed languages benefit programs which are intended to operate in multi-program heterogenous environments. Indeed, this seems to be consistent with observations. Languages like VBScript and Perl (the last of which is loosely typed under my definition below) certainly tend to be used for communicating with other programs and system components. Erlang's focus on inter-process communication may have influenced its adoption of dynamic typing.

In summary, I believe there are grounds to assert that, though the arguments casting each dynamically typed language as a weaker dialect of some statically typed language which is provably 'more powerful' are true, the argument that asserts that this always translates to a better 'programming language as used' is predicated on the notion that static typing provides a good model for the program environment which is not provable and might not be supported by fact.

* I'm aware that this expression is reviled. I use it here because I lack the appropriate vocabulary. In this context I specifically define it to mean: a language which stores all of the information pertaining to the operations permitted on a value as part of the value itself.

Mathematical proof is only available within the realm of precisely defined mathematical constructs. Its power beyond those confines depends upon the closeness with which the mathematics models the thing being analyzed.

Yes, a formal model of a real object is an abstraction of the object. Yes, it may fail to account for features of the object which are relevant for certain tasks.

Nevertheless, having a formal model is preferable to lacking one. And in the absence of any alternatives which address the same concerns, a formal model is unbeatable.

And though it might not model all relevant features, it does model some of them, and I think it is not hard to see that many of the things which programmers are concerned about are treated by formal models of programming languages, and moreover are treated better and more fully by such models than by any alternatives like design patterns, testing and dogma.

Formal models explain when a program is right and when it is wrong. They treat efficiency. And whether or not you believe that PL expressiveness is the last word on convenience, it is unquestionably a major component. Furthermore, formal models treat these issues in a precise and unambiguous fashion, which lets us settle questions and debates, and so build upon conclusions, rather than meandering endlessly in the sort of quagmire which one sees programming discussions mired in.

I am not interested in meandering, or repeating myself, or treating every instance of a problem when I can treat the problem itself, once and for all.

If you think the extant formal treatment of programming languages is missing some key element, than it is more useful to suggest a more comprehensive formal treatment, one which does address your concerns, than to reject formality altogether. (And by taking the latter route, you are not doing yourself any favors philosophically.)

What any such formalism fails to 'model well' within the context of 'programming languages as used' is that for a significant number of programs possibly very few values originate with types which may be known statically.

First, you are using the word "type" for something different than I. What you call a "type", I call a "tag" or "constructor". A "type" is, for me, by definition something which is determined at compile-time. Certainly there are many programs where tags are not statically known; that's why tags are useful. However, it's patently false to assert that there are few programs where types (in my sense) are not statically determined—just look at all the programs people write in statically typed languages.

Second, it's actually irrelevant "how many" programs there are of one sort or another. For every "dynamic behavior", there are one or more untyped programs with that behavior, and one or more (non-untyped) typed programs with that behavior. It may well be the case that you like to shove all your values into one type, and so your programs are all untyped. Well, that's fine; I think it's really sloppy, but static typing can accomodate those programs. OTOH, if you are a programmer like me, one who prefers to maximize the amount of statically computable information in a program, then ST languages are your only option; untyped languages are too weak for that purpose.

That is, programs must interact with other programs in ways which cannot be reasoned about statically. Clearly one can overcome this objection formally by reducing program I/O to well defined primitives

I think you are confusing static typing with determinism and dynamic typing with nondeterminism.

Languages which do not rely on statically derived type information alone, but which enmesh values with their types at runtime may have benefits for inter-program communication because marshalling of the sort described above can assign types dynamically in a manner which is consistent with the runtime assignment of other types within a program.

ST languages do not "rely on statically derived type information alone." If that were true, then there would be no need to run a program; its type would already give you the answer. You are, again, confusing types and tags, and imputing a limitation to ST which it does not possess.

Therefore, given the above considerations, one might expect that dynamically-typed languages benefit programs which are intended to operate in multi-program heterogenous environments.

On the contrary.

For two programs to communicate, they must share a protocol, and this protocol is something which must be known statically, that is, when both programs are being written. If you don't believe this, then try writing a program which can communicate with an unknown data source—there's no way to know what a message means, or even where one message packet begins and another ends, just as there is no way to know what program a bit string encodes unless you know architecture it's intended for.

Of course, given a finite set of protocols, you can negotiate one dynamically, but that negotiation itself demands a protocol, which is again static information which must be shared.

For an example of exploiting a type system to encode such protocols, see:

An Implementation of Session Types
Matthias Neubauer and Peter Thiemann.
In Proc. PADL '04.

Finally, you wrote:

Indeed, this seems to be consistent with observations. Languages like VBScript and Perl (the last of which is loosely typed under my definition below) certainly tend to be used for communicating with other programs and system components. Erlang's focus on inter-process communication may have influenced its adoption of dynamic typing.

Here we go again. Is Britney Spears a better musician than Miles Davis because she's more popular?

Putting the same argument over again may be somewhat tedious; reading those restatements helps me understand the argument. Thanks.

Very interesting discussion following the original post, had a great time reading it. I think that compile-time checks can add real security is when the source to the untrusted code is available to the system running it. That rules out a huge percentage of commercial scenarios. Even statically checkable bytecode is a problem - companies that want to protect their code know that bytecode can be more easily reverse engineered than native code.
Patricia from maruchan ramen.

I'd like a clarification on this. Having read the above a couple of times, it seems that you are arguing that (Untyped < Typed) implies that (ST is more expressive than DT). Since dynamically typed isn't (necessarily) untyped, either I have misunderstood what you are saying, or you are making a significant mistake in your reasoning.

dynamically typed isn't (necessarily) untyped

I think "dynamically typed" means "having untyped names" (aka variables). You are right that this does not mean that values signified by these names are untyped themselves, but (I think) Frank never mentioned execution of the programs, just programs themselves (so values do not exist yet).

By the way, are there really statically typed languages? How about taking head of the empty list in Haskell? Anybody with first-hands experience of dependent types?

PS: should I have used &rArr; instead of =>? Looks like a question for site discussion...

By the way, are there really statically typed languages? How about taking head of the empty list in Haskell?

In Haskell the list is a datatype with two constructors ([] and :), each constructor isn't a subtype of the list type. Even if Haskell forced you to write function declarations for all possible combinations of constructors we still could write programs that would type-check but would use the "error" function. And even if "error" was forbidden someone could write a polymorphic value like "undefined :: a" and use it to define the invalid cases.

Now I want to say that I don't like the "error" builtin and that it would be better if we never used the incorrect types in our programs, so if your algorithm doesn't work with empty lists one should create something like this:

data List1 a = Single a | Cons1 a (List1 a)

fromList [] = Nothing
fromList (x:xs) = case fromList xs of
                       Nothing -> Just (Single x)
                       Just xs -> Just (Cons1 x xs)

toList (Single x) = [x]
toList (Cons1 x xs) = x : toList xs

And the (ideal) Haskell compiler should be able to remove layer of indirection in the compiled code. It would also be great if "foldr" was defined in a type-class and list comprehensions where available for any datatype that defined a foldr, but now I'm digressing.

Perhaps we should wait for Arrow to use proper static types ;-)

That isn't a type error

True¹. It's not that Haskell allowed user of head to pass some value that does not correspond to the expected type. The problem is that it does not allow author of head to specify more precisely the expectations.

So calling error does not signify a failure of dynamic type-check, but a failure of dynamic extra-type constraint check. Therefore, I probably should rephrase my question: is there any (practical) PL that does not perform any kinds of dynamic validation of values (because it is able to prove them unnecessary - so C and ilk are out of contest)? Or the other way - how practical can it get without such validations?

¹We could pursue the point that this is a type error, as compiler promised that (xs : List A &rArr; head xs : A), and failed to fulfil that promise.


We still could counter this argument by saying that Haskell uses lifted types, and in fact the compiler promised (xs : List A &rArr; head xs : A^bottom).


If you are interested in this pursuit, let's run it on a fresh thread.

To me "dynamically typed" and "untyped" are synonymous. I've been using the latter because I don't regard what DT programmers call a "type" as a type; for me a "type" is a static entity, and what they refer to is, for me, a "tag" or "constructor".

However, the term "untyped" is also unsatisfactory because an untyped language does have exactly one type. So perhaps I should follow some authors who write "un(i)typed".

Unfortunately there seems to be name collision on how "type" is getting used. Frank, in the terminology you use, how do you distinguish between the "typing" done by a safe language like Lisp, where values are all tagged versus languages like C which are unsafe? I always thought that types fell onto the two-axis static/dynamic::strong/weak typing depending on when checks where done and whether they could be circumvented unsafely. Is there a better mental model I should have? (Other than only statically typed safe languages matter?)

In other words, don't tell us to change our thinking -- convince us!

... but I'll tackle this one anyway.

The easiest way to answer is to refer to Frank's entry "Once more around the track," where he explains quite well how making the distinction between "types" as static compile-time entities and "tags" as dynamic runtime entities lends clarity to issues such as determinism vs. nondeterminism and tackles whether it's true that protocols of interaction among programs cannot be reasoned about statically, which seems as though it should be considered obviously false given the recent spate of languages with rich type systems built around XML schema such as XDuce, CDuce, and Cω.

If that isn't clear, I don't know what to say that Frank hasn't also already said many times: what's popularly called "dynamic typing' means that values are all of a universal type, commonly called "Univ." When all values in a language are of a single type, it's not possible to say anything interesting about them on the basis of their types; you can only talk about what your language does or does not do with certain operations ("Scheme will complain if you try to add a value tagged as an integer to a value tagged as a string; Icon will attempt to cast one of the values to a type that will allow the expression to succeed in its evaluation context and fail if it cannot.")

Since all of these observations are based on formal type theory as described by, e.g. Pierce's "Types and Programming Languages," your comment about "rejecting conventional type theory in favor of this rather extremist version" confuses me: this purportedly extremist version is "conventional type theory" apart from the literature reserving the use of the word "untyped" to refer to a specific, minimalist articulation of the Lambda Calculus. All Frank is doing is observing that Univ is an unavoidable singleton and therefore there's nothing more to say about it when the context of the discussion involves making distinctions. Since the origin of the debate seems to be some people's incorrect belief that "dynamically typed" (a misnomer; I prefer to say "latently-typed") programs are equally or more expressive than statically typed ones, I'm prepared to cut Frank quite a bit of slack in his desire to employ crisp terminology that reveals fine distinctions.

Of course, intellectual honesty mandates full disclosure: I am an old-hand Lisp/Scheme/Smalltalk (all latently-typed!) programmer and am a relative newcomer to the ML world, mostly via O'Caml. I'm still learning about things like modules, phantom types, dependent types, and so on, but I can already see that static typing plus type inference of a rich type system helps me write correct, concise software (the "once I get it to compile, it just works" phenomenon). Having also made a living slinging Java for many years, and continuing to make a living slinging C++, I can utterly sympathize with the argument that "static typing" as found in these languages often causes more problems than it solves (you have to type more keystrokes, the type systems are weak, and at least in C++'s case the language is still radically unsafe). So if you remain unpersuaded, let me please recommend—if you have not already—that you download and install O'Caml and take it for a spin. I think you'll be pleasantly surprised.

But since you took the time to answer for him, I might as well reply to some of your statements.

The easiest way to answer is to refer to Frank's entry "Once more around the track,"

I read this, and it doesn't answer my question, namely why we should accept his definitions.

I don't know what to say that Frank hasn't also already said many times: what's popularly called "dynamic typing' means that values are all of a universal type, commonly called "Univ."

Saying something a lot of times doesn't make it true. If the analysis you are using is incapable of handling dynamic typing other than as a single universal type, then either your analysis isn't expressive enough, or your analysis operates under severe constraints, such as only handling static typing.

Since all of these observations are based on formal type theory as described by, e.g. Pierce's "Types and Programming Languages," your comment about "rejecting conventional type theory in favor of this rather extremist version" confuses me:

Of course I should have avoided the word "conventional", since convention is subjective. Maybe "broad" type theory would have been a better choice of words: what I am referring to is type theory unconstrained by issues such as static/dynamic typing. Anyway, Pierce's writings are AFAIK limited to the static subset of type systems and can't really be used to make statements on types in general.

In any case, mr Atanassow didn't state that his reasoning was based on Pierce or anyone else: he explicitly stated that those were his personal views.

(the "once I get it to compile, it just works" phenomenon).

Yes, that phenomenon. Does it really occur in non-trivial programs? I am reminded of Knuth's famous remark "beware of bugs in the above code. I have only proved it to be correct, not tested it."

I fully agree with your sentiments on static/weakly typed languages. I think ML is very impressive and inspiring. One of my students attempted to get me hooked on Haskell, but I found it far to rarified to be interesting. As for O'Caml, I tried it out a while ago: in my view it has lots of good ideas but isn't really an improvement on SML.

Peter Lewerin: Some day he will have to defend a Ph.D. thesis, and then he won't get away with "this is true because I believe it to be true".

IIRC, what Frank actually said was "I use this word to mean X and that word to mean Y," and then provided examples of distinctions supported by that terminology. That's a bit stronger than "This is true because I believe it to be true."

Peter: But since you took the time to answer for him, I might as well reply to some of your statements.

Excellent.

Peter: I read this, and it doesn't answer my question, namely why we should accept his definitions.

Because they are, in fact, consistent with Type Theory. More about that later.

Peter: Saying something a lot of times doesn't make it true.

Of course not. But a reasonable question to ask of someone who repeats their assertions is what their sources are.

Peter: If the analysis you are using is incapable of handling dynamic typing other than as a single universal type, then either your analysis isn't expressive enough, or your analysis operates under severe constraints, such as only handling static typing.

I gather from this that you aren't familiar with Type Theory. Type Theory's been around for a while—it actually predates electronic computers, coming to us from the mathematical logical tradition that gave us the Church-Turing Thesis, the Curry-Howard isomorphism, Russell and Whitehead's Principia Mathematica, and Gödel's Incompleteness Theorem. Again, more about this in a moment.

Peter: Of course I should have avoided the word "conventional", since convention is subjective. Maybe "broad" type theory would have been a better choice of words: what I am referring to is type theory unconstrained by issues such as static/dynamic typing. Anyway, Pierce's writings are AFAIK limited to the static subset of type systems and can't really be used to make statements on types in general.

This is where you're mistaken, by which I mean that you don't get to take a discipline whose definition has been well-defined for over a century and define it in some other way. There is no such thing as "type theory unconstrained by issues such as static/dynamic typing." When you talk about values at runtime and how operations upon them might be constrained by how they are tagged, you aren't talking about types. I didn't make that rule; Frank didn't make that rule; Benjamin Pierce didn't make that rule. If anyone did, you could say that Russell and Whitehead did, since one of the pressing goals at the time was to avoid Russell's paradox.

In any case, mr Atanassow didn't state that his reasoning was based on Pierce or anyone else: he explicitly stated that those were his personal views.

He said that he reserves the word "type" to mean "known statically at compile time" and "tag" to mean "providing a categorization at runtime." While it's true that that's Frank's opinion, it's also held very nearly universally throughout the Type Theory community, and if you've been following Frank's posts for any amount of time, you know that Frank knows this, so when he calls it his opinion, he's actually acknowledging the fact that others have differing definitions without allowing those definitions to alter the definition of Type Theory. And while there's certainly value in discussing how different languages interpret tags (cf. my Scheme vs. Icon example), doing so does not constitute an exercise in Type Theory. My sense (and Frank can obviously correct me if I'm mistaken) is that Frank gets frustrated when people seem very insistent about blurring distinctions and fuzzying definitions that Mathematical Logic and Computer Science have spent 100 years and more clarifying.

Peter: Yes, that phenomenon. Does it really occur in non-trivial programs? I am reminded of Knuth's famous remark "beware of bugs in the above code. I have only proved it to be correct, not tested it."

But of course Knuth was programming in Pascal at the time, so that was a reasonable disclaimer. ;-) I'm always leery of the "non-trivial program" question because it's so vague: somehow it seems like the goalposts always get moved.

Having said that, <http://caml.inria.fr/users_programs-eng.html> seems like a good start, as does <http://caml.inria.fr/humps/caml_latest.html>. Things that impress me are systems like CIL and CCured, Ensemble, MetaPRL, sumo, and the like. Of course, not having developed them myself, I'm not in a position to make strong claims regarding the trade-offs encountered in their development. I can only observe anecdotally my experience with the combination of interactive development, which many people who enjoy latently-typed languages seem to think of as their exclusive domain, and a rich static type system with type inference. I do find this combination extraordinarily productive.

Peter: I fully agree with your sentiments on static/weakly typed languages. I think ML is very impressive and inspiring. One of my students attempted to get me hooked on Haskell, but I found it far to rarified to be interesting.

In Haskell's case I have to agree: having to wrap my head around monads just to do I/O or get anything resembling assignment was just too much for me.

Peter: As for O'Caml, I tried it out a while ago: in my view it has lots of good ideas but isn't really an improvement on SML.

Certainly if you don't use objects I would agree with respect to the language per se. In my opinion, the benefits of O'Caml are the quality of the native compiler (AFAICT, only MLton approaches it on the SML side), the combination of toploop/bytecode compiler/native compiler with time-travel debugger and profiler (that is, real-world-focused toolchain), and the large number of existing libraries and external interfaces (the sociological aspect of tool adoption).

So if I may ask, since it seems you're familar with SML, has it not been your experience that static typing with a richer type system than, e.g. C++'s or Java's coupled with Hindley-Milner type inferencing is obviously beneficial? I'm always intrigued when people have actually gone so far as to try O'Caml or Haskell or SML and nevertheless prefer Python or Ruby or Perl or even Common Lisp or Scheme or Smalltalk. Clearly there's some aspect of their use that I'm missing, even, at least in Common Lisp and Scheme's case, after decades of use.

I gather from this that you aren't familiar with Type Theory.

I am familiar with type theory, but there seems to be a very large terminological gap between us here. What you refer to as "conventional type theory" I view as a relatively new (1980'ies and onwards; specifically, the works of Milner et al) extension to type theory. I am not all that familiar with this branch of type theory because I find it of limited utility and increasingly convoluted and esoteric as paper gets stacked on paper (e.g. I recently saw a paper by Benjamin Pierce that had me laughing out loud -- but possibly it was supposed to be a joke, and I just didn't get it).

My sense (and Frank can obviously correct me if I'm mistaken) is that Frank gets frustrated

It is my sense too that mr Atanassow gets very frustrated, but he could refrain from being rude and condescending.

But of course Knuth was programming in Pascal at the time, so that was a reasonable disclaimer. ;-)

It's just as applicable today, even with ML-style languages.

Regarding the examples you linked to: I certainly didn't mean to question the existence of working and useful O'Caml programs. I do not believe, however, that the software mentioned was written, compiled, and then "just worked". Rather, these programs were most likely produced in a write-test-rewrite cycle just like any other programs. My point is that this isn't embarrasing or problematic: write-test-rewrite is a good way to produce software. The "once I get it to compile, it just works" mentality is IMHO detrimental.

has it not been your experience that static typing with a richer type system than, e.g. C++'s or Java's coupled with Hindley-Milner type inferencing is obviously beneficial?

Ouch, I wish you hadn't used that exact word. I'd say obviously superior in many ways (I still stand by my assessment of SML as being impressive and inspiring). But I can't honestly say that I find it obviously beneficial, no.

I am familiar with type theory, but there seems to be a very large terminological gap between us here. What you refer to as "conventional type theory" I view as a relatively new (1980'ies and onwards; specifically, the works of Milner et al) extension to type theory.

I do not believe, however, that the software mentioned was written, compiled, and then "just worked". Rather, these programs were most likely produced in a write-test-rewrite cycle just like any other programs. My point is that this isn't embarrasing or problematic: write-test-rewrite is a good way to produce software. The "once I get it to compile, it just works" mentality is IMHO detrimental.

You're taking that phrase too literally. It's a characterization of an experience, not a law. The point is that working with a statically-checked language, a large number of errors are caught by the compiler before you ever run the program. In addition, these errors are caught more quickly, and with less effort on the part of the programmer. The result is that, compared to writing programs in dynamically-checked languages, it often feels as though programs "just work" the first time you run them, even though that's not literally true in every case.

BTW, write-test-rewrite is a big waste of time, and someone's money, when tests fail with (what would otherwise have been) a type error.

For example, taking a head of nil.

(duck)

What are some papers that are representative of the sort of conventional type theory you're talking about?

Just about anything in the field of type theory that doesn't pretend that static typing (or dynamic typing, for that matter, if such papers exist) is the only kind of typing.

You're taking that phrase too literally. It's a characterization of an experience

It's also a mindset. In the worst case, this mindset inspires inexperienced programmers to first substitute compiler-petting for design and then to skip testing because "if the compiler says it's okay, then it will work".

A clean compile is an indication that none of a limited set of recognized type errors occur in the program, nothing else. There may still be loads of bugs in it.

The result is that, compared to writing programs in dynamically-checked languages, it often feels as though programs "just work" the first time you run them, even though that's not literally true in every case.

I'd say that's a property of writing trivial programs, not of whether one is using a dynamically-checked or a statically-checked language. One does not get that feeling when writing non-trivial programs, again regardless of type checking style.

The problem, as I see it, is that the programmer using modern statically typed languages is encouraged to believe that the program will work once you get a successful compile.

BTW, write-test-rewrite is a big waste of time, and someone's money, when tests fail with (what would otherwise have been) a type error.

I'm not saying that static type checking is useless, in fact it's a great complement to external test cases. In languages like Common Lisp, you can have the best of both worlds: dynamic typing augmented by strategically placed static checks.

How do you feel, waste-of-time/money-wise, about failures due to spurious type errors? (I mean "violations" of type rules that don't actually matter, such as multiplying an integer by a "real".)

What are some papers that are representative of the sort of conventional type theory you're talking about?

Just about anything in the field of type theory that doesn't pretend that static typing (or dynamic typing, for that matter, if such papers exist) is the only kind of typing.

Surely you realize this is begging the question. You might as well just say "Just about any papers that are representative of the sort of conventional type theory I'm talking about." (Particularly following on Frank's citation-heavy last post...)

How do you feel, waste-of-time/money-wise, about failures due to spurious type errors? (I mean "violations" of type rules that don't actually matter, such as multiplying an integer by a "real".)

Actually, I just spent time this week tracking down a subtle rounding error that would have easily been caught if Java didn't have implicit rules about promotion/rounding. Does it really make sense to you that "x / 10000" and "x / 10000.0" have different types and different results? Of course I know Java well and knew very well that this was the case, but I still made the mistake...



I also knew very well that I wanted a floating point result, but Java quietly allows "double y = x / 10000;" by implicit promotion, so I had no help there either...

Surely you realize this is begging the question.

No, it's not. Do you expect me to actually cite every paper on type theory written in the last 100 years or so?

Does it really make sense to you that "x / 10000" and "x / 10000.0" have different types and different results?

Certainly not. That's just another example of why it's misguided to expect the program to work properly just because you've run it through a static type checker.

Do you expect me to actually cite every paper on type theory written in the last 100 years or so?

No. Just one or two representative ones would be fine, so we might have some idea of what you're referring to.

How do you feel, waste-of-time/money-wise, about failures due to spurious type errors? (I mean "violations" of type rules that don't actually matter, such as multiplying an integer by a "real".)

There is no such thing as a spurious type error. If an identifier named * is assigned the type Int -> Int -> Int, then it's a function on values of type Int and not on ones of type Double. On what grounds can you say otherwise? (And BTW, on what grounds would you argue that the meaning of * applied to Doubles is real multiplication? It could be any function.) The type system defines not only the meaning of a type but also the meaning of functions.

The type assigned to * says to the compiler and developer, "you are free to implement this function in such a way that it applies only to int; if someone tries to do something else with it, I promise to kick them in the ass."

If you want a function that multiplies both ints and real, then you write a function with a type like Num a => a -> a -> a.

And if you want a function that checks the implementation dynamically, you can write, for example, a value of type Univ.

These are all different functions/values, but you have the option to use the one you want. In a DT language, you have only the last option. How can you complain?

All your arguments sound to me like, "I want to use your language this way, but I can't do it!" when what is actually occurring is that you can do it, but you just have to do it a little differently. And this problem stems precisely from the fact that you can't get over the fact that "your type" and "my type" are not the same thing. If you see that, you will be able to use ST languages more effectively (and also DT ones). If changing your point of view lets you become more effective, how can it be wrong?

he problem, as I see it, is that the programmer using modern statically typed languages is encouraged to believe that the program will work once you get a successful compile.

This is just dogma. Programmers have lots of misconceptions about programming languages and tools, especially sophisticated ones. That's unavoidable, and we try to correct such misconceptions when we can.

P.S.: Strange for a DT advocate to claim something like, "We shouldn't allow X because it might go wrong"! :)

There is no such thing as a spurious type error.

OK, if you say so :-)

On what grounds can you say otherwise?

I'm not saying it's otherwise, in fact I was pointing out that this is the way it is with *ML languages.

These are all different functions/values, but you have the option to use the one you want. In a DT language, you have only the last option. How can you complain?

In Common Lisp, I have the option to statically limit application to (say) integers, or numbers, or some other number type, or to just relax and let the dynamic type checker handle it. I'm not complaining. :-)

All your arguments sound to me like, "I want to use your language this way, but I can't do it!"

No, when I use a language like SML, it's because it want to give modern ST a spin. I have a wonderfully inspirational book called "ML for the working programmer" (Paulson; no link, google if you don't know about it) that at times almost makes me fall in love with static typing.

When I don't want to do ST-style programming, of course I use another language (Lisp, Tcl, Squeak when I program with my kids). I'm not so masochistic that I want to do DT-style programming in SML.

P.S.: Strange for a DT advocate to claim something like, "We shouldn't allow X because it might go wrong"! :)

Assuming I'm the DT advocate, what am I saying we shouldn't allow, and why would it be strange for a DT advocate to want to disallow something that might go wrong?

What are some papers that are representative of the sort of conventional type theory you're talking about?

Just about anything in the field of type theory that doesn't pretend that static typing (or dynamic typing, for that matter, if such papers exist) is the only kind of typing.

I'd say that's a property of writing trivial programs, not of whether one is using a dynamically-checked or a statically-checked language. One does not get that feeling when writing non-trivial programs, again regardless of type checking style.

I disagree. The advantages of early catching of errors doesn't go away - if anything, the advantages are magnified in non-trivial systems. Once again, you're focusing too much on a literal reading of the phrase in question, rather than the characterization it's intended to convey.

Also, your objections about what programmers are encouraged to believe are not realistic, in my experience. I've never come across or heard of anyone being surprised when a program that passes the typechecker still has bugs.

In languages like Common Lisp, you can have the best of both worlds: dynamic typing augmented by strategically placed static checks.

That helps, but it still misses the point I made in the top-level post of this thread: type information and types do exist statically, even in dynamically-typed languages, whether or not terms or names are explicitly annotated with types. Arguments of the sort you're making against what can be called syntactic type theory are in fact arguments against particular type systems.

One of the most important reasons to learn about (modern) type theory is that it allows you to deal with and talk about types independently of the quirks of particular programming languages. Otherwise, you're stuck in Sapir-Whorf land, unable to discuss the things you don't have language for.

How do you feel, waste-of-time/money-wise, about failures due to spurious type errors? (I mean "violations" of type rules that don't actually matter, such as multiplying an integer by a "real".)

I've never come across or heard of anyone being surprised when a program that passes the typechecker still has bugs.

It happened all the time during my teaching years. Sometimes it seemed to me that I spent more time convincing the student that there actually could still be bugs in a compiled program than finding and squashing it.

That was of course quite a long time ago; maybe students are brighter now. Or maybe other teachers are better at explaining these things.

Arguments of the sort you're making against what can be called syntactic type theory are in fact arguments against particular type systems.

Um, I don't really feel that I'm arguing against "syntactic type theory" at all, but rather against the notion that STT is the be-all and end-all of type theory.

One of the most important reasons to learn about (modern) type theory is that it allows you to deal with and talk about types independently of the quirks of particular programming languages.

Exactly, at least if the parentheses means "modern or non-modern" instead of "modern but not non-modern".

Again, this is an objection to a particular type system.

Certainly. I don't see this specific example as symptomatic of a generic limitation of STT. I was just curious about to which extent mr Snively was concerned about "false positives" during type checking, if at all. I see now that it has the look of an attempted strike-back, which was not what I consciously intended.

At least static checks allow such things to be caught early, which keeps their cost low.

You are possibly not getting my meaning here. I was referring to cases where the type checking system reports errors that aren't actually errors in the sense that they corrupt the intended computation. (I realize that in the type theory sense, they are still errors and should be reported, but in practice you might not want it to be reported.)

I cite Russell's "Mathematical logic as based on the theory of types" as an example of an important work in type theory that does not limit type to a compile-time property.

But, insofar as the terminology can be mapped across disciplines, Russell's work does "limit type to a compile-time property"! The whole point of Russell's work was to be able to reject formulae which were considered meaningless, based on the types of their terms. This is exactly analogous to rejecting erroneous programs based on the types of their terms, which is what syntactic type theory does.

On the more mathematical side, "simple type theory" is also known as "higher order logic". It's exactly what Russell was trying to achieve! And on the computing side, modern type theory and type systems are the direct results of this kind of work, applied to programming languages, as Paul Snively pointed out earlier. Are there any necessary or important pieces missing from modern type theory, that was dealt with by Russell et al (excluding the bits that were shown to be unnecessary, such as orders of propositions)? I'd be rather surprised if there were.

From Russell's work, follows the reason modern type theorists have to reject the word "type" when it comes to runtime values. For them, programs are formulae consisting of terms which have types, and the very definition of "type" has to do with its use as a way to classify terms, and reject meaningless ones. Same as Russell. As Frank put it, in such a system, "there is really no such thing as 'static' or 'dynamic'. You have terms and types, and every term is assigned a type." Tagged values that come into play at "runtime" are outside of this system - only the syntactic type they belong to is relevant to the type system, and in the case of untyped languages, that's a single type like Univ.

Now, you might say that this is all very well, but there still should be some way to apply Russell-like type analysis to runtime values. But that's why I was asking for references - who has done this for programming languages, and ended up in a significantly different place from modern type theory?

Even if Russell's work didn't inherently fail to support your case, it would still fail on the basis that it doesn't deal with programming languages, which after all are somewhat different from the sort of logic that Russell worked with. In fact, if anything, your argument is really that modern type theorists are taking Russell too literally! They restrict themselves mainly to "programs as proofs" in the Curry-Howard sense.

However, afaict, what you're going to end up with when you do apply Russell-like types to programming languages, is something very like a variety of modern type theory. The reason is simple, and it goes back yet again to what I wrote in the top post: even in purely dynamically-typed languages, terms have types! You can't reasonably avoid this. Programmers in dynamically-typed languages simply do type inference in their heads, all the time (and then they confuse the types in their heads with the sets of tagged values in their program ;o)

I doubt you can create a useful type theory for programming languages that doesn't take this into account. You can ignore the fact that you do type inference implicitly when writing code, but you can't ignore it when you're developing a theory of types. And if your theory of types involves the typing of terms, you're back to a version of modern, syntactic type theory.

I'm of the opinion that current type theory could provide a better formal accounting of the relationship between syntactic types and their runtime correlates. Terminology-wise, at the very least, the current situation is unsatisfactory. However, it seems to me that any meaningful theory of types is going to have to account first for the syntactic aspect, because that aspect is logically unavoidable, and is a very basic, inherent property of all useful programs.

You are possibly not getting my meaning here. I was referring to cases where the type checking system reports errors that aren't actually errors in the sense that they corrupt the intended computation.

Well, that certainly seems like a reasonable cutting off date for talking about when type inferencing was introduced, but saying that that's when "type theory" arose is simply not true, by which I mean that there are published uses of the term dating at least to the 1930s, and they refer to the discipline that Milner works within. You might be able to make an argument that "type theory" began in the 1980s had Milner's work overturned the old theory, but of course it did no such thing. So as Frank pointed out in his own reply, it's perfectly all right for you to use the terminology you like. When it happens to overlap terminology that's in use by another, established community, though, be prepared to explain how it's consistent.

Peter: I am not all that familiar with this branch of type theory because I find it of limited utility and increasingly convoluted and esoteric as paper gets stacked on paper (e.g. I recently saw a paper by Benjamin Pierce that had me laughing out loud -- but possibly it was supposed to be a joke, and I just didn't get it).

First, may I ask which paper?

I have to confess that I find this vexing; it isn't a "branch" of type theory; it's type theory. And we continue to see real results from it: even the simply-typed languages that are popular are based on it, and of course it's the bread and butter of the more expressive languages such as SML, O'Caml, Haskell, Cayenne, Epigram... now we see results like TyPiCal: compile-time proof of lack of deadlock and race conditions and information flow. Information flow is also treated well by Flow Caml's type system.

Perhaps sticking closer to the "real world," phantom types are often used in functional languages with C FFIs to provide type-safe wrappers around type-unsafe C APIs. I'm thinking of lablgtk and lablgl as good examples here.

Types are all about knowing at compile time that certain classes of things are not possible at runtime. The assertion that you've been making without any support is that this is of "limited value." "Limited relative to what?" is the question that I should have asked from the outset, because I can keep enumerating values until the cows come home.

Peter: It is my sense too that mr Atanassow gets very frustrated, but he could refrain from being rude and condescending.

Oh, nice Dowdism, Peter. You neglected to quote the part where I suggest exactly what it is that Frank becomes frustrated with, and now I admit to sharing his perceived frustration: you claim that type theory is of limited value when even C is an existence proof (however poor an example it might be) of its value; you insist on conflating the two meanings of the term "type" without offering anything comparable to the body of work that exists in type theory or the pragmatic results of that work (offering up latently-typed languages as pragmatic results won't work because, as Frank has demonstrated one more time, they are subsumed by typed languages), and you ignore repeated demonstrations of the principles that govern the domain under discussion while insisting that somehow you are engaged with the domain. At some point, all one can say is "OK, if you say so."

Me: But of course Knuth was programming in Pascal at the time, so that was a reasonable disclaimer. ;-)

Peter: It's just as applicable today, even with ML-style languages.

No, it isn't, and I think this particular assertion really does show the nature of the difficulty. If we take "just as applicable" literally—and please feel free to let me know if you were merely engaging in a bit of hyperbole—your assertion is isomorphic to claiming at least one of the following:

1. Standard ML, Haskell, or O'Caml's type systems make no more guarantees than Pascal's.
2. The guarantees that SML, Haskell, or O'Caml's type systems make are unenforceable.

If you say what I honestly expect you to say, which is "neither," then we will have arrived at the conundrum: to say simultaneously that Knuth's quote is "just as applicable to code written in an ML-type language as to code written in Pascal" and "ML-type languages make stronger enforceable type guarantees than Pascal does" is inconsistent. This is why people like Frank and myself tend to look askance at claims of limited utility or expressive equivalence from people who promote latently-typed languages. Again, it's not that I don't care for them; I've been developing in such languages for decades. I had just made my own kind of category error: I used to think that interactive, incremental development was necessarily a feature of latently-typed languages like Lisp and Smalltalk. Type inference and good toploop tools in SML, Haskell, and O'Caml proved me wrong, so now I enjoy the guarantees that static typing and type inferencing in a rich type system provide.

Peter: Regarding the examples you linked to: I certainly didn't mean to question the existence of working and useful O'Caml programs. I do not believe, however, that the software mentioned was written, compiled, and then "just worked". Rather, these programs were most likely produced in a write-test-rewrite cycle just like any other programs. My point is that this isn't embarrasing or problematic: write-test-rewrite is a good way to produce software. The "once I get it to compile, it just works" mentality is IMHO detrimental.

Peter, this is just silly. Making guarantees that classes of bad behavior cannot happen at runtime is what types do. How can it possibly be detrimental to say "I want to prove before runtime that certain bad things can't happen?" Of course there's still a write-test-rewrite cycle; if there weren't it would be because the entirety of the computation could be done at compile time a la those perverse factorial-as-C++-template-metaprogram examples we've all likely gagged over. When I declare something to be "int," for God's good sake, I do indeed expect that code that I write using that type "just works" given the algebraic definition of integers. Of course, many popular languages violate that expectation and impose details of, e.g. machine word size on my code, the bastards. So fine: I learn algebra and some stuff about range and overflow. I'm still working from an assumption-set; I'm still asking the compiler to promise me, pretty please, not to start treating my int as if it behaved the same as a float or a string. If I, in a fit of sleepy late-night coding, myself treat my int as if it were a float or a string without telling the compiler that that's my intention, I want the compiler to call me on it rather than blithely building nonsense into my product, with said nonsense maybe or maybe not being caught by testing, and maybe or maybe not causing my product to crash on my customer's machine, which may or may not cause them to lose data or even all of the unsaved data on the whole machine.

All that modern languages with rich static type systems do is expand the scope of guarantees that they make at compile time. All type inferencing does is recognize that type annotation is a pain in the neck. The result of their use is software about which stronger claims can be made than would otherwise be the case. Does this make the software perfect? Of course not. Does this mean that SML, Haskell, and O'Caml are the final word in typed programming languages and we can stop now? Not at all. Does this mean that latently-typed languages should be abolished and laws passed forbidding their use? Good heavens, no. It just means that the time at which certain properties of a program are checked is different among different languages. There are plenty of application domains in which checking and perhaps failing at runtime is perfectly fine, and some of the recent work on automating testing, particularly automating comprehensive test coverage, is very exciting. Personally, I'd like to see a conjunction: a rich static inferred type system, maybe even as rich as Cayenne's, coupled with an automatic comprehensive-coverage test generator.

Me: has it not been your experience that static typing with a richer type system than, e.g. C++'s or Java's coupled with Hindley-Milner type inferencing is obviously beneficial?

Peter: Ouch, I wish you hadn't used that exact word. I'd say obviously superior in many ways (I still stand by my assessment of SML as being impressive and inspiring). But I can't honestly say that I find it obviously beneficial, no.

OK, that's honest and fair. To get any further with it would, I think, require us to begin splitting hairs over what the distinction between "superior in many ways" and "beneficial" is, and I confess that I can't imagine that being productive.

The funny thing is, I think there's a sense in which we're in vehement agreement. You say there's still a write-test-rewrite cycle; I agree; You say that you still need to test your software; I agree. Here's the kicker: if you do comprehensive-coverage analysis and automated test-case generation on your program, you're doing type inferencing and you're doing it statically. The only thing you're not doing is doing it in the compiler. If you eliminate the comprehensiveness requirement, you're no longer proving anything. Maybe that's OK for you. Heck, it's OK for me some of the time. But in general I want more guarantees from my compiler, not fewer.

Actually, Frank's position is "conventional type theory". For example, the wikipedia page gives Pierce's definition about type systems being "a tractable syntactic method" for classifying program terms. "Syntactic" implies that types are statically knowable & checkable. The page goes on to point out that "type theory, as described herein, refers to static typing disciplines."

Cardelli's survey paper, "Type Systems" gives an overview of this perspective. The paper refers to languages like Lisp as untyped, where "untyped" indicates that terms in the language don't have statically known/knowable types, or, more or less equivalently, they all have the same type. (Although type theorists often seem to confuse lack of static checking with languages that are untyped.)

What it boils down to is that type theorists have found nice formal ways of dealing with types, and within those formal systems, "type" has a very specific, formal meaning that can't be fudged. In that context, what we call "types" in dynamic languages can't really be considered types, so they're called tags instead.

Naturally, all sorts of terminological shenanigans ensue, because of course the things that type theorists don't want to call types are, to a first approximation at least, actually the dynamic equivalent of the static entities they do call types.

Discuss. ;o)

I feel that the assumption that software development activities are all static activities is incorrect. Given sufficiently capable languages, software development is a very dynamic activity, where the type signatures of functions may be changing even as the program is running... or the nature and behavior of the types themselves.

This kind of flexibility to sketch interactively on a running system is something that I always miss when I go back to ML.

It seems to me that it would be nicer if type inference and type consistency checking were optional, programmer-invokable features of an environment.

I feel that the assumption that software development activities are all static activities is incorrect. Given sufficiently capable languages, software development is a very dynamic activity, where the type signatures of functions may be changing even as the program is running... or the nature and behavior of the types themselves.

What I mean by software development being a static activity is not that one does not run programs during development. I mean rather is that one is that it is a meta-calculation, that the programming language is the object language and that the things one is calculating are programs.

In my view, any software development process, no matter how chaotic or informal, amounts to a program derivation, that is, a series of program refinements, with the last refinement producing the release product. Along the way, one also produces some wrong programs (which you can think of as branches). In the intermediate products, and the missteps, you may have a values and functions with types different from those in the final product. But, as I regard the final product as being a different program from the ones preceding it, I do not regard such values and functions as having "dynamically changing types". [1] Indeed, as far as I'm concerned, if two values have different types, they cannot be identical; your notion of "type" may be different.

It seems to me that it would be nicer if type inference and type consistency checking were optional, programmer-invokable features of an environment.

I may have missed the point of your previous postings, though I don't think that my point necessarily affects any of your arguments, merely one of your assumptions. I think you may have missed my point. I am not saying just that one runs a program while developing it, but that one may develop a program while it is running. Also, that those meta-calculations of producing the "product" may be several layers deep, as the programming language, the program, and its data need not be completely distinct entities.

Not every piece of software has the same idea of concrete releases -- in some cases, the "releases" are constant, incremental changes to the running program. I suppose that, at a fine-grained level, this is still static, as functions are replaced atomically.

Consider the case where a system is running where function F returns values of type FOO. A new function G is written that uses F, and so G is typechecked to ensure that it works with values of type FOO. After all this (and while, say, G is serving requests asynchronously), we adjust function F such that it can also return values of type BAR, knowing (to the best of our imperfect human estimates) that G won't call F such that it returns a value of type BAR. So, we no longer have a type-consistent program, but for its convenience, we're (I'm?) willing to take our chances (good practice in this case would, of course, be to change G to handle BARs before doing the modifications to F). Generally, the worst that could happen is that G receives a BAR and causes a run-time error, so we patch G from the debugger and send it off running again.

That seems to make sense to me, but I apologize in advance if I'm getting this all wrong, or if my example isn't sufficiently illustrative.

If there were an instance that I wanted to change something in the way you're suggesting, then I'd have to change all calls to it anyway or I am really doing something different and should just make a new function.

I hate how it's so damn hard to encode information that I'm using into the program text and actually start using that information in the system.

I think you may have missed my point. I am not saying just that one runs a program while developing it, but that one may develop a program while it is running. Also, that those meta-calculations of producing the "product" may be several layers deep, as the programming language, the program, and its data need not be completely distinct entities.

How you develop your program is your business. What I am concerned with is that your development process actually terminates.

In other words, you produce a product, and that product gets delivered to end-users who treat it as a black box and it will never again be altered by you from that point on. No maintenance, or bug patches, or new versions or whatever. If you alter the program so it behaves differently, I consider it a different program.

That is the sense in which development is a static activity, while deployment is a dynamic activity. Unless you are actually trying to produce buggy software or induce your users to upgrade regularly, the ideal a programmer strives to achieve is that there is a complete separation between the development and deployment phases (or "use phase"—I guess "deployment" is not quite right).

(Did I mention maintenance as a development activity? If so, I was mistaken.)

Now, let me predict: someone is going to jump in red-faced and pronounce, "But maintenance-free software is impossible to write!" Whether or not that is true, it doesn't change the fact that maintenance-free software is the goal of software development. At least, it is my goal. And if it isn't yours, that's fine; just be up front about it and warn all your potential users that correctness is not a priority for you.

At Q42 we have built several web applications for customers who regularly send e-mails with new feature requests.

These features are developed on a test server and then remotely installed on the live web server, while it keeps serving requests.

It has nothing to do with maintenance. It's just gradually adding or changing functionality. And as long as there is no end to the need (or immagination) for new features, there is no "termination" of the development process.

[Message deleted. This clearly was interpreted as an attack; since I did not intend it that way, I'm simply removing this message. Something wrong must've been in it to spill over into a promising new thread. Here endeth the bullshit, whether or not I caused it.]

This is like rejecting valid forms of creativity, such as brainstorming, because they do not purport to have a sound logical result at each step or even at the end. Even if each step does culminate in a product of some sort.

Brainstorming always have a sound logical result at each step, you just have to look at the right level. For example I usually use Haskell to do quick simulations and when my program type-checks it means that my current model is consistent. As I'm just hacking the results may be different from what I expect but they're sound with the model (i.e. the model is incorrect according to my expectations).

If a given creative process isn't logically sound how can we assess it? I'm not saying that every one should be rational but we should have some way to verify if it is complete or not (even if this way is emotional, e.g. "when I'm satisfied").

This is very interesting, because while I think my prejudices lie over in the camp of Frank's (Make your program as correct as possible before letting users use it), I'm interested in this model that you seem to be working with, Julian, where your program runs for a long time and pieces get inserted and removed while it's running. I know there's some work on hot-patching running systems, which seems intuitively crazy to me but maybe is not so crazy when I think about it.

I can see the value, in the case of systems where one second of downtime (while stopping and starting for a new version) can be very expensive--for example, a web service or some kind of real-time embedded system (in a spaceship, say).

In this case there would seem to be some value in having the freedom to change the precise contract of a given library function, while somehow honoring the spirit of it, so that its (still-running) client continues working.

But Julian, you said you'd ensure to the best of your human fallibility that G wouldn't call F in such a way as to produce a BAR result. If you're willing to count on your human resources, then it sounds like you just don't need type checking in this case.

On the other hand, wouldn't it be nice if you could ascertain that G really does never call F in such a way as to produce a BAR? And wouldn't it be nice if you could determine that by statically checking the F-G ensemble as a whole? Just because you don't want to stop, upgrade, and restart G, doesn't mean you can't statically check it (unless you've lost the source code, in which case, I don't know what to do).

When you say, "I don't need to check my code statically," a corollary of that (I think) is, "I prefer to check it dynamically," that is, at run-time, and through particular test-cases, rather than by "proofs" over the code. But if particular test-cases and human fallibility are acceptable to you, then I'm suprised that your service is so critical that you're unwilling to stop and restart it!

Then again, I wonder what are the limits of static checking, in the face of software evolution. If G was designed without the notion that F might return a BAR, then will it be possible to construct a checker that will determine that F-G is safe?

I know there's some work on hot-patching running systems, which seems intuitively crazy to me but maybe is not so crazy when I think about it.

But if particular test-cases and human fallibility are acceptable to you, then I'm suprised that your service is so critical that you're unwilling to stop and restart it!

Stopping and restarting interrupts all your users, and can require a great deal of coordination and scheduling. But any given patch typically only affects a small part of the system. Even if a change breaks the system in a particular area, you can always revert to the previous version, and only a small subset of your users is likely to have been affected.

As much as anything else, hot-patching can be a convenience feature. Paul Graham wrote about how, with their ViaWeb/Yahoo store application in Lisp, they would patch the system to fix a bug or change a feature while a customer was on the phone. Imagine the alternative: shut down the entire application so that all customer's stores go offline. Hot-patching provides flexibility, and removes what can otherwise be quite a serious barrier to deploying changes.

BTW, this applies to dynamic and statically-typed systems equally - hot patching is routine in Java applications, too, and Java application servers provide built-in support for it.

AFAIK there's limited support in Java app servers (I'm happy to be wrong about this):
- can we add/remove fields?
- can we change inheritance relationships?
- can we ...

You're right, I shouldn't have said "equally". However, you can work around some of the issues with class loaders. For example, you could change an inheritance relationship between classes which are loaded by the same class loader, by dropping that class loader and reloading it. Class loaders can be used to partition a system into pieces that can be independently loaded.

But you're right, it is more limited than a dynamic system. Still, for many sorts of changes, it works fine. It works particularly well for something like JSP pages, where the framework is architected to support dynamic changes.

The basic thesis of interactive programming is that it's not so crazy when you try it, it's actually very good. You get to know the dynamic side of your program by interacting with it and shaping it while it runs, continuously for days, weeks, or years. This is a beautiful thing that you have to experience to appreciate.

I don't think it's very exotic either. Emacs is a one-million-line program written in exactly this way. It works extremely well despite having no static checks, no test suites, dynamic scope, no module system, etc. One million lines of Emacs Lisp. How can this be?

In the last year I worked with a team who maintained a couple of millions lines of COBOL. That was my exact thought: "Millions of lines of COBOL. How can this be?"

;-)

1. Designed and implemented by a small group of deep wizards.
2. Leveraged extreme OS, language, and domain insight (that is, its designers weren't "text-editing specialists," but rather had written text editors, programming languages, and OS subsystems before).
3. 2nd-system effect: EMACS was originally a collection of TECO macros.
4. About 35 years of evolution.
5. It/some of its packages are nevertheless buggy.

EMACS is a great system, but let's be fair; as an example, it's pretty unique. It certainly seems hard for me to argue that its success tells us anything about elisp or latently-typed languages in general!

If we really wanted to attempt an apples-to-apples comparison, I'd have to suggest that we compare and contrast <http://www.mozart-oz.org and <http://www.ps.uni-sb.de/alice since they at least stem from the same foundations, but Oz is latently-typed while Alice is statically typed.

There's no conflict between being statically typed and interactive development. One of the things that I appreciate most about O'Caml is that I have it all: an interactive toploop, a bytecode compiler with a very nice time-travel debugger, and a native-code compiler with a profiler. All development stages, from the most free-wheeling seat-of-my-pants type-and-go exploration to the crystalization of architectural choices with a debugger to help me out when I get it wrong to building what I expect to ship and profiling it to get it as fast as it can be are accomodated very, very nicely.

Oh, and the toploop/compiler will helpfully tell me when I'm not even making sufficient sense at code-entry/compile stage, leaving me with vastly fewer worries at runtime. And I still only have to mention types in my code once every blue moon. Win-win, I say.

Interestingly enough, there's an extensible editor written in O'Caml; you can find it at <http://pauillac.inria.fr/cdrom/prog/unix/efuns/eng.htm.

The Yi text editor is written in statically typed Haskell, yet can have most (maybe all?) of its functionality changed while it's running, by dynamically loading and reloading code. Thus, you don't need a dynamically typed language to do this kind of thing.

I think rather than saying static is superior to runtime it is better to say they compliment each other. How do you for example guarantee the correctness of a distributed service based systems where programs invoke third-party services that may be located on the other side of the globe. While static type checking can be used to confirm the type-correctness of a program, the third-party services may change their behavior unpredictably at runtime due to Byzantine faults/attacks/compromise. So a statically type check program may behave unpredictably at runtime.

msupratik: I think rather than saying static is superior to runtime it is better to say they compliment each other... While static type checking can be used to confirm the type-correctness of a program, the third-party services may change their behavior unpredictably at runtime due to Byzantine faults/attacks/compromise.

These two statements are certainly true. However...

msupratik: So a statically type check program may behave unpredictably at runtime.

is not necessarily. It certainly is true for popular statically-typed languages such as C, C++, and Java. However, most of the statically-typed languages that tend to be popular here (Standard ML, O'Caml, Haskell...) don't suffer this deficiency: they don't "go wrong" (see this Wikipedia entry for a good overview of what that means).

Having said that, type-safe distribution, specifically, remains an open area of research. Let me trot out my favorite examples of encouraging work in the domain: Peter Sewell and colleagues' Acute and HashCaml efforts.

I agree with your statement about C/C++, but I don't quite understand, how Java can go wrong? Did you mean NullPointerException? Or ClassNotFoundException? Or InvocationTargetException? Or IncompatibleClassChangeError?

I agree, some of them are far from intuitive, but they are defined in the spec, and so certainly do not mean "going wrong".

On the other hand, one can see these kind of exceptions as manifestation of the dynamic side of Java type system.

On the completely orthogonal hand, where does Haskell go when it takes a head of an empty list?

Andris Birkmanis: I agree with your statement about C/C++, but I don't quite understand, how Java can go wrong? Did you mean NullPointerException? Or ClassNotFoundException? Or InvocationTargetException? Or IncompatibleClassChangeError?

I agree, some of them are far from intuitive, but they are defined in the spec, and so certainly do not mean "going wrong".

Right on all counts. I was referring to a combination of Java Is Not Type-Safe and the fact that Java doesn't even have a formal semantics, so how can you prove that it won't "go wrong," even though it's intended to be type-safe? I have actually had Java VMs core dump on me, something that I've never seen with O'Caml or Haskell.

Andris Birkmanis: On the completely orthogonal hand, where does Haskell go when it takes a head of an empty list?

It throws an exception, of course. Throwing an exception isn't "going wrong," and certainly isn't "unpredictable." Although, of course, it might still be unpredicted by the programmer. :-)

I suspect that most of statements from "Java Is Not Type-Safe" are about ancient Java specs. It's much harder to talk modern Java into "going wrong", though I agree with Vijay Saraswat that classloaders are one of the murkiest parts of the language.

Yes, I've got core dumps from JVMs (dozens of them), but that's primarily the fault of implementations, not the spec. OTOH, having informal spec does help to create unstable implementations, I agree with that (and I already ranted about this problem on LtU).

But returning to my pattern of defense, is Haskell indeed defined in a formal way? Is Haskell 98 Language and Libraries, The Revised Report the ideal way to specify a PL? Where is the formal definition of semantics?

A quote from introduction:

This report defines the syntax for Haskell programs and an informal abstract semantics for the meaning of such programs.

I agree that modern Java is better than when Saraswat documented his results (thank God).

It's also true that not all of even languages such as O'Caml and Haskell have fully formally-defined semantics. What they do tend to have, or at least are relatively easily amenable to, are proofs of preservation and progress for their evaluators. So maybe it's more a matter of not having parts of the spec say "undefined behavior" than anything else.

So there do seem to be some shades of gray, with C/C++ at a very unsafe end of the spectrum, Java at a pretty-good midpoint, and Standard ML/Haskell/O'Caml at the very safe end. And, um, Acute and HashCaml in the infrared spectrum. :-)

AFAIK, the only practical language with a complete formal definition so far still is Standard ML. But IIRC even for that no complete soundness proof has been done (though significant parts). Harper's group is currently working on a machine-checkable proof in Twelf based on their alternative type-theoretic formalisation.

Haskell and OCaml are only informally defined. The Haskell Report at least contains a semi-formal spec of significant parts of the operational semantics, by means of transformation rules into a relatively simple lambda calculus. A full formal definition along the lines of Standard ML was started by Wadler & Peyton Jones long ago but never finished. OCaml probably is too complex to ever receive a formal definition.

Java also is informally defined, but modest subsets of the language have been formalised and even proved safe by others.

Acute has a relatively complete definition but is in fact unsafe as of yet, because its unmarshalling mechanism is not supposed to verify type/data consistency. Likewise HashCaml, AFAIK.

It throws an exception, of course. Throwing an exception isn't "going wrong," and certainly isn't "unpredictable." Although, of course, it might still be unpredicted by the programmer. :-)

I think one of the reasons for these endless debates about static typing is that normal programmers don't appreciate this distinction :-)

(and rightly so)

...is that the metatheory doesn't appreciate this distinction, either.

That is, if you start adding features like dependent types to a language, where the evaluation of terms can affect the type level, you quickly learn that anything that can "go wrong" in an informal sense (like throwing an exception) makes your soundness proofs sadistically harder. (And that's only if they are even still true!)

I figure any 'catchable' variant of bottom is fair game as typecheck failure? The sort that might not halt is another matter.

edit: Just remembered that not everybody does their exceptions via a monad, which does rather make it harder as hypothetically a larger term incorporating the one with an exceptional type might do something at type-level to catch the exception...

You're right, though as a practical engineering matter people who do dependent types work really hard to stay in languages without any "bottoms" at all, simply to stay sane.

The full explanation goes like this....

With dependent types, you have terms showing up in types. So if you have a Sequence type that's indexed with an integer noting its length, it will be a type constructor with a kind like Sequence : Nat -> type, and you will have types like Sequence(15) and Sequence(9).

Now, for this facility to be useful, we want two type expressions like Sequence(5) and Sequence(2 + 3) to represent the same type. So the typechecker needs to know how to show that 5 and 2 + 3 are the same, in order to know whether two types are equal or not.

This is such a basic point that you may have to think quite hard to realize that we need to do it at all!

So to typecheck a dependently-typed program, we need to know whether two program expressions are equal or not. And all the difficulties that human programmers have reasoning about things like exceptions, state, nontermination, and so on will show up in the code you write to check whether two terms are equal.

State does strike me as a potentially much scarier thing to add without control. It seems to me that the problem with non-termination is more that non-terminating typechecking isn't overly desirable in practice.

Of course, I guess I'm assuming the existance of normal forms for terms. Non-termination is not your friend there, by comparison exceptions seem pretty benign.

I've been doing a fair amount of background reading, though I've not got round to implementing anything myself - amongst other things I've an interest in starting to use Pure Type Systems or a variant thereof to structure descriptions of lambda calculi more than is commonly seen in the literature, so that eg more proofs can be reused, intuitions about what changes or combinations of features will or won't break properties, things like that. I'm trying very hard to ignore the whole issue in some of my personal projects though!

Personally, I find the Pure Type System stuff to be elegant but somewhat obscure. I like keeping type constructors and terms syntactically distinct -- it's easier to understand what's going on, even though you end up doing a bit more work (because you have to prove things like substitution properties twice, for both type constructors and terms).

When I started learning about dependent types, it was really helpful for me to first study F-omega (it's in Pierce, chapters 29 and 30), because it has a nontrivial type equality, but doesn't have dependencies in it. That made the number of new things I had to learn to understand dependent types smaller.

I should have been clearer: my only real point is the distinction between "unpredictable" and "unpredicted" and between "crashing my runtime" and "signaling a problem that I can handle within the context of the language/OS." I find these distinctions absolutely critical, and to call throwing an exception "unpredictable" relative to crashing the runtime, or throwing an exception "going wrong" relative to crashing the runtime, seems like unbelievably sloppy thinking/terminology to me.

Are you [Ehud] saying "normal" programmers don't understand the distinction between, say, undefined behavior that may silently corrupt your program vs a guaranteed exception? And that they shouldn't understand this?

No, no. I knew I wasn't being too clear, but I was going for funny...

My point is that when we are "selling" type soundness we say "typed programs don't go wrong", but this claim is true only for a strict and narrow meaning of "wrong" while programmers are interested in more. Many debates are of the sort "but even in [insert your favorite tryped language here] you can do [insert something that causes a runtime exception]".

I am not the first to claim that the "don't go wrong" slogan can do more harm than good. It is better to explain what is really meant by type safety & soundness. That's all I am saying.

Ok, I see what you're saying. The "don't go wrong" slogan is too simplistic, and promises too much when taken at face value. I agree, I found statements like this confusing when I first encountered them. They do have a sort of marketing/spin feel to them, which I don't like.

Let me say that I totally agree.

The problem with "Well-typed programs don't 'go wrong'" is that it's a written pun rather than a verbal one: the punctuation is significant. The scare quotes around "go wrong" tip you off that the phrase isn't to be taken in the usual sense. It's hard to inject those scare quotes when you just toss off the line in conversation, however.

I stop short of saying that it's "just spin," however, because some folks really don't make the distinction between "throwing an exception" and "crashing the runtime." One is utterly predictable and entirely within the evaluation regime of the program; the other is not. That's the difference between "not going wrong" and "going wrong," and if we need to come up with a better way to educate people about that distinction, by all means, let's do it.

I agree with both of you guys. But...

if we need to come up with a better way to educate people about that distinction, by all means, let's do it.

Are we trying to educate them about this or about the benefits of static typing, I forget :-)

For the industry, crashing the runtime and throwing an exception is exactly the same: the flow of work stops, the client can not work, engineers need to be employed so as that the program is tested, the problem is analysed and solved etc.

A program that has stopped working has 'gone wrong'!

I think the real step forward would be to eliminate even the throwing exception errors, so as that the promise 'once the program is written, it is correct' is fulfilled (I will not say 100%, because that's physically impossible) to a much greater level.

An abnormal program termination which is caused by an assertion failure or raised and unhandled exception is way easier to debug than one caused by a synchronous crash; and both are way, way, way easier to debug than data corruption bugs that manifest themselves at a great semantic distance from the cause of the failure.

For programs which have been deployed in the field; those that crash and are able to email bug reports and provide the user with diagnostics that say "we suck, but we know we suck" are more reassuring that programs which silently stop working with no explanation as to why; and both of which are infinitely preferable to buggy programs that trash the user's valuable data.

Progress is needed on all fronts: permitting the programer to specify more and more requirements in a (semi-)formal manner such that they can be verified in advance of deployment; and/or allowing the tools to infer such requirements and ensure consistency; and ensuring that programs which do go wrong fail in a well-defined way. Neither should be considered an exclusive replacement for the other; no more than the presence of breakage alarms on the perimiter windows of a building obviate the need for motion sensors in the interior.

Defense in depth. Single points of failure are bad. Proofs of correctness generated by compilers are greatly helpful; but even they are insufficient, as they only approximate proof of that holy grail we call "correctness".

Of course it's easier to debug an application when the error is known, but my point is that what the industry would like is for those exceptions not to exist in the first place.

"More reassuring" is meaningless in the face of deadlines and contractual penalties.

It's very important to distinguish between what a programmer expects about 'right' and 'wrong' and what the compiler writer (which is also a programmer, although usually more formally educated) means on these terms.

For me, purely functional programs can go easily go wrong, because the algorithm I typed is wrong. But they are not 'wrong' programs, from the perspective of the compiler: they do exactly as I specified.

Is it possible to go one step beyond what purely functional programming offers and help the programmer even more? there is still knowledge that can not be encoded in the best type systems.

Here are some important questions (for me, because for other members of LtU they might be answered):

Why, I, as a human, can tell more about the properties of my program, than the compiler?

What is it that the compiler misses so as that it can not reach the same level of conclusions as me?

I think that the answers to these questions will offer valuable insight into how to make better programming languages.

My insight (from experience) is I, as a programmer, make more and better abstractions in my mind than the compiler allows me to express, and thus working on this higher level it's easier to reach conclusions.

there is still knowledge that can not be encoded in the best type systems.

Actually, it's an extremely tricky philosophical question as to whether that's true if "best type systems" = "most expressive". The reason being that we already have turing complete ones, and if it can't be expressed in those then it's difficult to see how you can actually know as opposed to believe.

What can be easily and readily encoded is another matter, of course. You may well have to embed a more appropriate logic/language.

Why, I, as a human, can tell more about the properties of my program, than the compiler?

What is it that the compiler misses so as that it can not reach the same level of conclusions as me?

We don't do most of our reasoning consciously. In fact, I'm pretty sure I mostly use conscious thought to reflect on my reasoning - I don't even consciously think about how to 'prettyprint' it half the time when I'm doing stuff on paper! The compiler doesn't have a handy subconscious though, it needs everything in front of it (I was going to write "explicitly", and it certainly all needs to be represented in some manner). This means that unless you've done a fair amount of work, you know (and especially suspect) a lot more than you've told the compiler enough to figure out.

If you haven't already, you might get something out of learning to use a theorem prover - it'll teach you more about how to embed things you do know.

The outstanding problems are in how to reduce the workload - both figuring out how to fill in the gaps and in building the kinds of libraries and frameworks that an approach like this calls for. Because we're talking about modelling formally things you may be playing fast and loose with (potentially without realising!), there will also be new concepts to learn along the way.

One final gotcha: sometimes we're interested in properties we weren't already keeping track of in advance, and this can really challenge the flexibility of our code when we then attempt to show that they hold for code we wrote without looking to make that property visible.

Why, I, as a human, can tell more about the properties of my program, than the compiler? What is it that the compiler misses so as that it can not reach the same level of conclusions as me?

Actually we (humans) can't tell more than the compiler or vice-versa. Currently we have three sets of properties: (a) the entire set, (b) what humans can know, (c) what compilers know. We know that a ⊇ (b ∪ c). The problem is ensuring that the type system can express everything a human can (i.e. c ⊇ b) in an easy way (as Philippa pointed out we can with some type systems today if we accept the encoding complexity). Also we know that bugs catchable by expressive type systems occur in other languages (e.g. adding meters to feet, some kinds of infinite loops) so these are cases when the compiler know properties that the (human) programmers didn't know. Also I doubt the abilities of humans to be as comprehensive as compilers when assessing program's properties: I can be certain that the Haskell compiler catches all the cases of incorrect usage of Maybe (i.e. using something of type Maybe a as something of type a) but I'm never sure in Java that I tested against all possible unintended occurrences of NullPointerException.

I think the main issue here is how can we define a language that can ensure the properties the programmer want, when we don't know before defining the language what kinds of programs people will write: Do we need to express time and space properties (if so how precise it needs to be?)? What about the resulting precision of floating point operations, is necessary to encode this in the language too? An interesting problem with the type systems available today is that we need to predict which properties will be interesting to the future programmers: If I write a list module I must predict that some of it's users need to assert properties about its length (encoding the length in the type), but if they also need some other property they can't just reuse all the code available in the list module because they're going to use their own data type. Actually with something like type classes we can have generic operations (e.g. imagine in Haskell some class that has a class containing this method map :: Proof p q => (a -> b) -> C p a -> C q b where Proof p q is a witness that for that particular transformation we can change the proof in some way) and we just need to instantiate the particular implementation for our datatype (and provide the methods without default implementations) or we could just ignore type classes and yet another phantom type to the data type (e.g. the list would go from List Size Element to List Property Size Element) and some operators to compose properties. Both implementations may be too cumbersome but would be interesting to see if it worked well in practice (we could do both in either Haskell or Epigram now, AFAICS), also I believe we would lose true implementation hiding (i.e. the extended proof needs to know the structure of the implementation to be able to be properly validated).

Ok, I agree that humans can't tell more things than the compiler. What I meant to say is that humans know more of the interesting (to the humans) properties of a program than the compiler.

For example, I may know that a list never contains more than N objects, because the insertion has been encapsulated in a module which checks the number of objects of the list prior to the insertion. But the compiler does not know that, and so when I want to store all the elements of the list into an array (for example, if I want to quickly process all the elements of the list by keeping them close), the compiler can not infer that that the array can never contain more than N items, and therefore it can not optimize out the code as I would.

Another example is the order of operations: I know that a certain object is not required after operations X and Y, and therefore I can delete it after X and Y are executed; the compiler can infer that and automate the deletion.

Compilers are actually pretty good at catching the operation order case, it's a well-studied problem (though I've a suspicion it's one of the ones we can only take a good approximation for if we want good performance for the optimiser in the general case).

The combination of proofs and hints needed when you know the maximum size is trickier though. First of all, you shouldn't ask the compiler to infer it from the encapsulation - really you're looking at a new list type that comes with a proof of size (and allows an implementation change without affecting everything else). From there, it's possible to envisage a language that allows placing the list interface/view on top of an array of known size - indeed, this sounds a lot like the kind of thing that the FP group at Nottingham have been working on lately. Doing it manually is something we already know how to do today - you just reimplement the list interface and change the representation type.

In general we can't ask the compiler to do everything we would've done in the way of optimisation - DWIM commands are only intermittently successful. On the other hand, it should be possible to give it a few hints ("use a fixed-size array", say) and let it fill in a lot of the obvious stuff (OTOH, it might well not know without being told that all the indices are in bound too the way you do!).

It's worth bearing in mind that a lot of the idioms and conventions we use to communicate to other programmers reading our code aren't entirely foolproof - this really isn't a property we can afford in our compilers.

Again, it'd probably do you some good to play with a theorem prover sometime - building an array-of-known-size type and the appropriate means to avoid bounds checks would be a good beginner's exercise (in fact, the interface is a common example - it can be described as an improvement on a typical list type).

If I know that a list will never have more than N elements, and I want to encode that knowledge in a program so that the optimizer can use it, I write an assertion.

The compiler knows that code downstream from the assertion can only be executed if the assertion was true -- and therefore that the number of datums we are looking at is less than N. So it knows it can allocate an array of N elements and will never need to spill.

Assertions are how we tell the optimizer things that it cannot prove for itself. It gives us a runtime check while debugging, plus static optimization of the downstream code.

I'm an advocate of heavy type inference, plus type declarations as assertions. If we assert something that the system can prove wrong, we should get an error. If we assert something that the system cannot prove right, we should get a warning about possible runtime exceptions, and dynamic checks of our assertions performed at runtime. If we declare something correct that the optimizer could tell anyway, we should get code no different than we'd have got by skipping the declaration (ie, no actual runtime checks should be performed).

Speaking of exceptions thrown when taking the head of an empty list, Oleg Kiselyov has a nice little write-up about Exceptions in types and exception-free programming.

First - thanks for the reply. I was aware of type inferencing, but hadn't looked into it very much (I had a brief play with OCaml a while ago). Soft typing sounds interesting, I'll have to look into it.

The question doesn't really arise, in that no-one can call your code unless they provide values of the proper types, which is mostly determined and enforced statically.

The problem is not with people calling my code, it's with me calling other people's code and getting back some value encapsulated in an inappropriate type. As I don't have a real world example to hand, I'll invent a highly-contrived example:

Suppose some library function returns a stack value of some sort. Now, let's say this stack defines just two operations: push and pop. But what if I want an equivalent of a peek operation? I have to code it up as a pop followed by a push, which is inefficient. To go further, perhaps I want to be able to display the entire contents of the stack (in some GUI window perhaps). I have no way to do this without popping every single element and then pushing them all back onto the stack. I can't even find out the number of items in the stack without doing this. This gets even worse in situations where the defined operations for a type do not allow you to accomplish everything you want: imagine there was no push operation.

Now, if I happen to know that the stack is implemented as a list, I should be able to override the type system, break encapsulation, and treat the thing as a list. It may not be a great thing to do, but it is often preferable to rewriting an entire library.

I think in a case like that, I'd probably do something like:

copyOfStack = []
while stack.size > 0:
   copyOfStack.append(stack.pop())

- export the contents of the stack to something that does what I want, then work with that.

That's not really a solution. Firstly, you've added a size property to the stack! But that's not a real problem (if there wasn't a size property, then presumably pop would have some way of signalling end-of-stack). What is more of a problem is that sometimes this isn't possible - the defined interface doesn't provide enough operations to be able to recreate it in some other form. Second to that, is also the problem of efficiency: if that stack contained a million elements (or a billion...), you wouldn't really want to copy it.

then I guess I wouln't be wanting to display the entirety of its contents in a GUI, either.

In a way this is besides the point - I understand that you're talking about what happens when you need to circumvent the public interface of some external component in order to do things that interface doesn't support. You basically want a fall-back so that when it looks like you're totally fscked, you're actually one step away from totally fscked. All this does is buy you time, though: if you then find you want something that the list-based implementation doesn't support (like for it to have been b-tree indexed all along), and that you can't just emulate with a wrapper in the way I was describing, then I guess you're totally fscked after all.

Yes, you are right that there is still a possibility of not being able to do what you want at the list level. The key difference is really not about static typing, but about enforcing information hiding. It seems subtyping involves adding more interfaces to a type (thus making it more powerful/flexible), whereas information/implementation hiding involves removing the interfaces of the underlying data structures, and providing a new interface (thus making it less powerful/flexible, but easier to control). I think I'm advocating that implementing a stack should be done by creating a list (or whatever your concrete implementation is) and adding a stack interface to it, rather than creating a new abstract type and hiding its implementation. Sounds a bit like Self.

To bring this back to static type checking, I think what I want is a system which will check whether the assumptions I have made are valid for the code as it is now (is this what type inferencing does?), and not whether they will remain valid in the future (which is what implementation hiding/ADTs seem to be about). Of course, being able to do both would be useful (errors for the former, warnings about the latter).

But what if I want an equivalent of a peek operation? I have to code it up as a pop followed by a push, which is inefficient... Now, if I happen to know that the stack is implemented as a list, I should be able to override the type system, break encapsulation, and treat the thing as a list. It may not be a great thing to do, but it is often preferable to rewriting an entire library.

You complain about the minor inefficiency of coding peek via pop and push and propose to solve the problem by eliminating abstract types in every program everywhere? Please be serious.

How about the major inefficiency associated with the fact that you cannot now ever reimplement the ADT without breaking client programs? And if you are willing to break clients, why do you brook at rewriting the ADT? And if the ADT designer knows he will never reimplement the ADT, why would he make it abstract?

Anyway, this has nothing to do with static typing. You can write unencapsulated data structures in any language; it's a non-feature.

You can easily reimplement the ADT. You only break those programs which choose to ignore your public interface and peek around in the guts. I don't propose to eliminate ADTs. I propose that an ADT (as an interface) should be something you add to a concrete implementation, rather than use to hide the concrete implementation. Which interfaces are supported is a documentation issue.

The problem of writing peek in terms of pop and push is indeed minor. I said it was a contrived example. Often these problems crop up in areas which are not minor, and in which a reasonable person may make an informed decision that breaking encapsulation (bypassing supported interfaces) is a cheaper alternative than rewriting from scratch. In much the same way that opening up some piece of electrical equipment and soldering on some extra features may not be a good idea and will invalidate your warranty, but you can still do it, if you really really want to.

[EDIT: You are right, though, that this isn't a static typing issue. I apologise for confusing the issue.]

You can easily reimplement the ADT. You only break those programs which choose to ignore your public interface and peek around in the guts.

If you reimplement it, then the new implementation has to support the private interface you exposed, or raise an error when it is used.

And if you are willing to raise an error then, then you are only using a convention to distinguish publics and privates.

And if the only thing guaranteeing the well-being of your clients is a convention "don't touch my privates, unless `you really really want to'", then you might as well make them explicit in the interface and add a note, "please don't touch my privates while I expose myself, unless you `really really want to.'" Conventions require no language support.

A better, simpler solution is simply to expose your implementation separately along with your ADT, or, if you have subtyping, to ensure the former is a subtype of the latter.

data Stack a = Stack (StackImpl a)
...

class Stack { ... }
class StackAsList extends Stack { ... }

interface Stack { ... }
class List implements Stack { ... }

I propose that an ADT (as an interface) should be something you add to a concrete implementation, rather than use to hide the concrete implementation.

This is already possible, as I just explained. (You use the words "bypassing supported interfaces", so I assume you don't mean this as a methodological proposal but rather as a language feature proposal. Otherwise, I would agree that it is good practice to expose an implementation along with an encapsulated version.)

Exposing representations is a non-problem; hiding them is where the difficulties lie.

And if you are willing to raise an error then, then you are only using a convention to distinguish publics and privates.

Exactly. And this is what I advocate - only using convention to distinguish publics and privates. You could formalize that convention by allowing keywords "public" and "private" if you wish, but they do nothing except indicate intent to the programmer (and documentation generator!).

Exposing representations is a non-problem; hiding them is where the difficulties lie.

Yes, so why allow people to hide them at all? ;)

A question: does type inferencing automate the process of separating out interface from implementation ("if it looks like an X, and acts like an X...")? If so, I should really have another look at Ocaml (unless someone has a better suggestion).

this is what I advocate - only using convention to distinguish publics and privates.

Hmm.

A question: does type inferencing automate the process of separating out interface from implementation ("if it looks like an X, and acts like an X...")?

No, this is impossible. I can use lists to implement, for example, sets, bags, catenable sequences, stacks, even integers and real numbers. There is obviously no way for the compiler to determine which one is desired. That choice is, in part, determined by which operations are exposed and which are hidden.

If so, I should really have another look at Ocaml (unless someone has a better suggestion).

I suggest you look at 80386 assembler.

80386 is one of the world's most efficient dynamically typed programming languages, and will never get in your way when you want to break abstraction—which is expressed entirely by convention. You can apply any operation to any piece of data, and there is no such thing as a type error. After all, it always makes sense to add, multiply or divide two words, whether they represent integers, floats, addresses, strings, window handles, grocery lists or JPEG images. No bondage and discipline here!

Another virtue of the 80386 language is that libraries written in it are extremely portable: only client programs which use 80386 architecture-specific features will break if you decide to reimplement your library in, say, 68K. 80386 assemblers usually support a valuable feature called "comments", which you can use to advise clients about architectural dependencies without forcing them to do things they might feel uncomfortable with, or which might violate their religion.

80386 is flexible. One can code up any conceivable language feature in 80386: tuples, higher-order, continuations, hash tables, and so on. The proof of this is that every major compiler for programming languages supporting such features can produce 80386 code.

80386's major weakness is its syntax, which some people find too minimalistic. However, regarded as a concatenative language, 80386's "less" is "more", and you should rather regard it as an intellectual game you can play while writing code. Or you could code up your own syntax in m4, maybe something cute with lots of parentheses?

My motivation for persisting with this thread is that I have run into problems of inflexibility with C++ and Java in the past. I've played with Haskell and Ocaml a few years ago, and while I appreciated their elegance, I had technical difficulties with the compilers I had (I needed to build shared libraries, and couldn't figure out how), so I had to abandon both before I'd got a real feel for the languages. Now that I have a bit more time, I can go back and learn one of them properly, or I can pick up a different language. But before I invest effort in learning the languages, I was trying to see what practical advantages they would offer me over C++[*]. To this end, I outlined a typical problem I have had, in order to see if someone could expain to me if and how Haskell/Ocaml/some other language would help me solve that situation.

[*] Over and above support for functional programming, which I do recognise the value of. Indeed, I realise that this is a good enough reason on it's own to make the switch, but there are unfortunately practical considerations to take into account (shared libraries and integration with existing "legacy" C/C++ code for instance).

I can give you the same problem in any language that supports closures.

Type annotations are essentially proofs of different properties of your program. Even with the current set of commonly-used statically typed languages, you get a lot of value. For example:

int add(int a, int b);

The types prove that the function MUST accept to integer parameters and MUST return a single integer value. Though this probably isn't the most impressive example, I think the problem is that this level of typing is taken for granted.

Another example is the Haskell I/O monad, which is designed to statically ensure that you cannot perform state-modifying computations in a function that is delcared to be pure.

That said, I've read a little about dependent types. This is a more complex form of typing that lets you prove more complex properties of a program. For example, if you wanted to define the boolean OR function, you could write:

bool OR(bool a, bool b);

However, you could also treat 'true' and 'false' themselves as subtypes of 'bool' and write:

true  OR(true  a, true  b);
true  OR(true  a, false b);
true  OR(false a, true  b);
false OR(false a, false b);

Note that the above is a *single* type signature.

Then, in your program, when you use the OR function, the type system (not the optimizer's constant propagation system) can statically determine, for some boolean values, whether they are guaranteed to be true or false. If 'NOT' were similarly defined, the type system could prove that "OR(NOT(x),x)" is a tautology.

The OR example is kind of limited, but you can take this kind of extreme typing and apply it to more complicated values. For example, you can define a type that means "sorted list" (though it's pretty complicated) and can write the function signature:

sorted-list mergesort(list l);

When the type system checks the function's types, it will essentially have to prove that the function mergesort returns a correctly sorted list! Awesome, huh? Unfortunately, this kind of typing is not (yet?) practical for most programming tasks because the type annotations become so complex and cumbersome that it's probably not worth the trouble. Another problem is that the typechecking algorithm isn't decidable, so you might have to Ctrl+C your compiler once in a while :)

Awesome, huh?

Of course!

Unfortunately, this kind of typing is not (yet?) practical for most programming tasks because the type annotations become so complex and cumbersome that it's probably not worth the trouble.

Conor McBride elaborates on some ideas how to make advanced typing more user friendly by employing interactive programming.

Another problem is that the typechecking algorithm isn't decidable, so you might have to Ctrl+C your compiler once in a while :)

In some related theories it is decidable. One of the classics is An Extended Calculus of Constructions by Zhaohui Luo. I find it very accessible (I was able to grok it despite having no experience with either type theory or logic). ECC has very nice meta-theoretic properties. In fact, I am even considering to hack something in Eclipse based on this paper and Conor's ideas :)

Inductive types in constructive languages by Peter Johan de Bruin¹

Being amazed at the lack of a general language for the irrefutable expression of mathematical argument, I looked for it in the direction of what is called Type Theory.

This thesis circles around two themes that closely intertwine: formalized mathematical
language, and inductive types.

we start with the traditional description
of inductive sets by means of well-founded relations. Then we move to the categorical
framework, which will be our main tool to bring various induction principles under a
common denominator

The introduction of the thesis gives an overview of related efforts, including Automath, ITT, Nurpl, LCF, ML, CC, Coq, ALF, DEVA.

The thesis maintains a nice balance between enjoyable prose and succinct formulas.

¹Not to be confused with N. G. de Bruijn, known for Automath and de Bruijn indices.

The link in the above comment has move it is now Inductive types in constructive languages. The Groningen pages promise that that link will be more permanent.

I'm not familiar with that puzzle. Would you care to elaborate?

It can also be easy to make practical DSLs for which all programs terminate just by careful choice of control constructs. In general I much prefer to have language constructs that naturally guide me to desirable programs rather than program-checkers that complain to me about undesirable ones. But if the typed languages are a lot more general then it could be worth it.

As an example, I can imagine a type system that detects unsafe sharing of variables in multithreaded programs and can be used to prove the absence of those errors. But I'm much more interested in a language like Erlang that leads naturally to a better programming style, and doesn't even have a way to express the errors that the type system would detect.

I can also vividly imagine the author of such a type system presenting pages of learned theory to establish the soundness of it, and shaking his head in exasperation that I don't appreciate that he's proving things! But my imagination is overly uncharitable. :-)

This old LtU thread discusses this issue in more detail.

You seem to argue that the theory is irrelevant or, at least, unimportant.

Like Haskell's, though it's inconsistent, since every type is inhabited.

I thought about this long and hard, and did some research, but I couldn't understand this.

I could see that the lack of an empty type could make the type system incomplete.

Can you explain how it makes it inconsistent?

Thanks!

(Sorry to add to your already high LtU tutorial load. ;-))

A logic is inconsistent if every proposition is a theorem, so a proof theory is inconsistent if every proposition has a proof, so a type system is inconsistent if every type has an inhabitant.

I could see that the lack of an empty type could make the type system incomplete.

It's the other way 'round; Gödel showed that a logic cannot be both complete (w.r.t. Peano arithmetic), and consistent. A programming language is complete by definition (w.r.t. "Turing semantics") so cannot have a consistent type system.

The inconsistency is usually caused by general recursion. Polymorphic lambda-calculus is incomplete, but consistent; add an unrestricted fixpoint operator to it, like Y, and it becomes complete but inconsistent.

I think I was making a spurious distinction between a system that is "too weak" to express false propositions and one that can express false propositions but has a distinguished proposition (or set of propositions) that can be proved both true and false.

Upon reflection, I realized they are formally the same thing.

Thanks for your help, Frank and Kevin!

I can't even believe you're going to try to turn this argument around.

I was just trying to reply as directly as possible to the question you asked. You asked if it made sense to me that "x / 10000" and "x / 10000.0" have different types and different results?. I answered in the negative, since it doesn't make sense to me, and added that I regarded this as an example of how bugs can remain even if the type checker does not report any type error.

I can't believe anyone is really so obtuse as to be unable to see what my example has to do with your claim that "multiplying an integer by a real" is a type error that doesn't "actually matter." I can assure you, it actually matters to me.

I am obviously so obtuse. I used multiplying an integer by a real as an example of a type error that does not actually distort the computation (barring rounding errors, the computational value of a multiplication expression is the same regardless of term (sub)type, given that the values of the terms are unchanged, e.g. 2 × 2 = 2 × 2.0). I called this a "spurious type error" or "false positive".

You used integer/real division as a counter-example, and specifically mentioned checking this with the Java type-checker. Many languages, including Java, set the value of a division expression differently depending on the types of the terms, possibly distorting the computation. This is what I would call a "false negative": a "type problem" (by definition it isn't a type error in Java, even if it probably should be) that causes a bug, but isn't reported by the type checker.

I'm not trying to be clever or avoid your argument, it's just that I can't see where your counter-example connects to my original statement.

(Even more alarmingly, people in general seem to think that what I'm trying to do in this discussion is to argue that dynamic typing is somehow "better" than static typing. This is totally false, and if anyone has gotten that impression, it only reflects a monumental and embarrassing failure to communicate on my part.)

I may have minor quibbles with some of your statements, but I can't think of how to address them without causing more confusion. For the record, I recognize your reply as a full and valid rebuttal to my previous statement, and hereby retract it.

In honor of the patient and sincere attempts to discussion by you and Anton van Straaten, I will try to produce final answers to some of your earlier postings, and then I will remove myself from this forum to avoid causing further irritation.

I, for one, am not irritated. However, I am saddened that this is the outcome of a (mostly) civilized professional discussion.

(Even more alarmingly, people in general seem to think that what I'm trying to do in this discussion is to argue that dynamic typing is somehow "better" than static typing.

You shouldn't take that personally - that discussion is hard to escape around here (and in programming circles in general). Like many arguments between two camps, e.g. conservatives vs. liberals, it's a largely artificial dichotomy in which many people self-identify themselves into one camp or the other, and then classify other people via litmus tests based on statements they make (type inference! ;)

What we've been discussing is at the heart of that dichotomy, and it's the reason I think it's important to learn about modern type theory: it's not about static vs. dynamic; "syntactic" types are something present in all languages and all programs. The exception at the extreme would be the untyped lambda calculus: but no useful languages are "untyped" in that strong sense.

The static vs. dynamic dichotomy mainly comes into play because the low-hanging fruit for syntactic type systems is on the statically-checked language side, so that's where most of the syntactic type theory action is.

The weaker sense of "untyped" - which I think is an unfortunate overloading of the term that detracts from clarity of discussion - is used to describe languages which don't assign types to their terms by annotation and/or inference. However, in these languages, many terms nevertheless do have types - in the sense that it is possible to insert an assertion on every term about the "rutime" type(s) of value produced at that term, such that the assertion would never fail. It may not be possible to automatically infer such assertions, but it is always possible for a human who understands the program to create them.

Even the terms that don't have identifiable "types" per se (corresponding to a set of runtime type tags) nevertheless must assume some kind of type information, such as "this object accepts the print message". In a more rigourous type system, that information might be represented as a typeclass or an interface.

As I said in the top post, you can't write useful code without such type information present "syntactically" in a program. So modern type theory is applicable to all languages, it's just a lot more difficult to apply it to languages which have ignored it, where the (syntactic) type system being used is entirely ad-hoc, as is the case in most dynamically-checked languages.

It's difficult to escape the fact that the application of type theory to real languages is still, in some senses, in its infancy, or at least in an early generation. In discussions like this, fans of syntactic types are often all too willing to gloss over the weaknesses of the actual existing systems, which turns off the people in the other camp because from their perspective, the claims for existing systems seem exaggerated. From their own perspectives, both sides are right to an extent, but they're both also missing some important points.

One of those points is that type systems can be improved, and will be improved. And that process is, or will be, as relevant to dynamically-checked languages as it is to statically-checked languages. It may not seem so right now, but that's a self-fulfilling conclusion - if, as Frank suggests, syntactic type theorists don't care about the sorts of things done in dynamically-checked languages, and users of the latter languages don't believe syntactic type theory applies to them, the result is the situation we have today.

We may have to wait for languages that convincingly demonstrate the sort of thing I'm talking about, before people will start paying attention to the possibilities. But in the meantime, we could at least raise the level of discussion by, on the dynamic side, learning more about type theory, and on the static side, being more willing to acknowledge the limitations of existing type systems. I liked Conor McBride's ostrich comment, but there are ostriches on both sides.

Today, the choice of one camp or the other is largely based on problem-domain requirements and/or on which tradeoffs a person is most comfortable with (even if the person in question won't admit it ;)    I'm willing to bet that there will be languages in future, which have the characteristics that dynamically-checked language users want, but which also have sophisticated syntactic type systems, that don't require significant tradeoffs. IOW, I'm saying I believe syntactic type systems are the future, for both camps.

Another way to put this, which might seem less controversial, is that the existing latent type systems in dynamically-checked languages will be improved and exploited.

Of course, purely dynamically-checked languages will continue to survive, if only because of the point which Mario B. raised, that "run-time checking of tags is much easier to implement". But they won't be the best of what's available.

All I can can with any certainty is that the early 21st century is an absolutely fascinating time in which to be following programming language design!

Mario: If there was such a thing as an untyped Java, nobody in his right mind would prefer it to the typed Java. Empirical evidence for this is that there is no untyped Java on the market, even though it would have been relatively easy to implement.

Here's an irony: I have to disagree with both your conclusion and your claim of evidence! My counter-evidence is <http://groovy.codehaus.org>. Groovy is a very pleasant dynamic language for the JVM with all sorts of Python/Ruby/Smalltalk-inspired goodness and an impressive collection of libraries. It very definitely passes my "convenience of development" smell test.

It might be interesting to compare-and-contrast Groovy with <http://nice.sourceforge.net>, which might be described as the Haskell of the JVM-language world. I think such a comparison would be valuable for two reasons:

1. There's a strong sense in which the languages are "otherwise the same" modulo their type philosophies: both are implemented in terms of the JVM, and both make a concerted effort to integrate easily with other Java code. This may be as close to a practical apples-to-apples comparison as one could reasonably get.
2. It should be relatively easy to avoid falling into the trap of focusing on sociological issues. For example, both tools have Eclipse plug-ins, so environmental benefits might not be incorrectly ascribed to the presence or lack of a static type system given that both can be situated very similarly, if not identically.

So here we are in the real world, where one can simultaneously value the guarantees made by rich static type systems and the flexibility and convenience of a good latently-typed language. As always, we'd like to have the luxury of using the right tool for the job, whatever that happens to be, but once more, sociological issues count. If I'm working at a Perl shop, extoling the benefits of O'Caml isn't likely to be warmly received. :-) So thanks for the reminder that there are many important issues to consider in language selection beyond the types vs. tags debate.

Thanks for the links. Groovy and Nice indeed make a very good pair for a types vs. tags shootout. From a quick glance at both, my impression is that, safety aside, Groovy has more features than Nice. Both languages have added support for closures to Java. Nice also has multi-methods, tuples, optional parameters and assertions. Notice that none of the added features are hard to type. Groovy, on the other hand, has added markup-language support, path extressions, SQL expressions, and several extensions that seem to build on the markup-language support.

Groovy's extensions are not impossible to type, and for some of them types could even be inferred without type annotations. But there's no doubt in my mind that adding the type inference alone would be much harder, probably involving one or two orders of magnitude more effort, than what's been implemented so far.

So, I'm afraid your example supports what I've said very well. You may have misunderstood my comment: I never mentioned any sociological issues, I tried very hard to stick to the technical issues alone. My central point is that type safety is not the only technical issue we should compare from one language to another. The decision to have static type checking in a language or not to have it has huge effects on the rest of the language. And your two examples support this (rather obvious) fact.

I've taken a look at the features of Groovy, and though I don't mean any criticism of the Groovy language or team, I wasn't impressed by the power of the feaures compared to what's available in Nice. I've started an in-depth rebuttal of the claim that Groovy "has more features than Nice". The first installment is here.

Damn! We should have been using Turbo Prolog after all!8-((

>>> listOfPeople = [ new Customer("James"), new Customer("Bob"), { "name" : "A map" } ];
>>> names = listOfPeople.name;
>>> println(names);
["James", "Bob", "A Map"]

• construct a new type for every markup literal
• infer type for every markup expression
• infer type for every path expression
• check type compatibility for every application of a path expression to a markup expression

Now back to my original point: Given a choice between a language with fully-typed markup and path expressions and a language with the Univ solution, of course the the full typing is better in all respects. But this is not a choice you'll get. The choice you have is between an untyped language with a lot of practical features and a type-sound language whose designers are reluctant to add any feature that doesn't fit in its type system.

Another good example would be meta-programming in Template Haskell vs. MetaML. Haskell designers in this case made an atypically practical choice to use a Univ-type scheme for the terms. I have no doubt everybody would have preferred to have metaprogramming that "can't go wrong", but the choice they had was between the ugly Univ and an elegant nothing.

Your Web page certainly makes Nice looks better than Groovy,

That's not my intention necessarily; I'm trying to point out that Nice also does the things that Groovy does. Groovy advertises these as features, which causes people such as yourself (no disrespect intended, just an example) to conclude that there is some substance to them. There are a zillion little things that Nice does that do not appear in feature listings because they're not really significant.

but I get a feeling that you're avoiding some the complexity issues. What whould you do with this example from Groovy:

> listOfPeople = [ new Customer("James"), new Customer("Bob"), { "name" : "A map" } ];
    >>> names = listOfPeople.name;
    >>> println(names);
    ["James", "Bob", "A Map"] 
]]>

What is the type of listOfPeople? It's not a list of Customers, for sure.

Without any context to justify why Customers and dictionaries should be treated the same way, I'd reject it as an error. If there was some justification, and we absolutely had to make it work, we could stoop to reflection and casting, just like Groovy does. But I think it's a bogus example. Customers are statically guaranteed to have a name field, dictionaries are not guaranteed to have a name key, so your example is positing a List<Univ> and asking how I'd handle it better than a DT language would. I wouldn't, that's what Univ is for.

A full support for markup languages and path expressions with static typing would have to:

• construct a new type for every markup literal
• infer type for every markup expression
• infer type for every path expression
• check type compatibility for every application of a path expression to a markup expression

Mmm. "path expression" is just "expression", so inference is already taken care of. As for the markup stuff, obviously you can't make up a name and call it in a statically typed language. So if you want to be able to do:

XmlBuilder.foo(bar: 1, baz: 2) { quux() };

without predefining foo and quux, you'd better choose Groovy. Personally, I think allowing that syntax lulls you into thinking that this is something other string munging. I think it's better to have show that something is dynamic, rather than pretend that calling make-believe methods on XmlBuilder is the same as calling real methods like System.currentTimeMillis(). So if I wanted to do something like that in Nice, I'd be explicit about the fact I'm building something dynamically and there's no safety net:

XmlBuilder.node("foo", [("bar", "baz")]) { node("quux"); }

Now back to my original point: Given a choice between a language with fully-typed markup and path expressions and a language with the Univ solution, of course the the full typing is better in all respects. But this is not a choice you'll get. The choice you have is between an untyped language with a lot of practical features and a type-sound language whose designers are reluctant to add any feature that doesn't fit in its type system.

But you do get the choice! If you write (or generate from a schema, say) the markup functions for your flavor of usage, then you get static typing. If you don't you can still use the dynamic version. It's just that you can easily tell which one you're getting.

Another example: Nice has typesafe variants of zip which handle 2, 3, or 4 list arguments. Actually I think we may only have them for generators and iterators at the moment, but leave that aside. All of these are written in terms of unsafeZip, a method which takes any old function, and a list of as many lists as you like, and makes a good faith effort to zip them all together. If the number of lists isn't the same as the number of arguments the zipping function takes, you get an error, just like in a DT language. If Groovy had zip(), it would always be unsafeZip, but that doesn't mean that Nice can never use unsafeZip.

Another good example would be meta-programming in Template Haskell vs. MetaML. Haskell designers in this case made an atypically practical choice to use a Univ-type scheme for the terms. I have no doubt everybody would have preferred to have metaprogramming that "can't go wrong", but the choice they had was between the ugly Univ and an elegant nothing.

It's a start. On the other hand there's MetaML... Me, I'm always looking for the extension to Nice's type system that will let me get rid of unsafeZip altogether, because the type checker can check that the number of lists passed and the the arity of the zipping function are the same.

Me, I'm always looking for the extension to Nice's type system that will let me get rid of unsafeZip altogether, because the type checker can check that the number of lists passed and the the arity of the zipping function are the same.

Look no more, HOFs to the rescue.

... and useful, but alas, not quite what I'm looking for. Or so I always thought. Maybe I need to take a look at that one again. this example from Oleg is similarly fun.

I agree with everything you've said, except for the following:

Without any context to justify why Customers and dictionaries should be treated the same way, I'd reject it as an error. If there was some justification, and we absolutely had to make it work, we could stoop to reflection and casting, just like Groovy does. But I think it's a bogus example.

I suppose this is the kind of righteous posture that makes people use untyped languages. You can't ask for a "justification" for everything people want to do with the language. You may be a top PL expert, but that doesn't make you a software engineering expert, if there is such a thing. If the type system doesn't allow something that would otherwise be legal (i.e. no run-time error) and has no easy workaround, it's the type system's fault, pure and simple. The best you can say in that situation is that it's too hard to do properly. Don't claim that anything that doesn't fit in the type system must be somehow wrong.

I suppose this is the kind of righteous posture that makes people use untyped languages. You can't ask for a "justification" for everything people want to do with the language.

Certainly not, only for the things they want help from the compiler for. Dynamic stuff is always an option, in fact it's even easier in Nice than I generally make it look. See here, for example. My point is that throwing a dictionary and a Customer in the same list is not a realistic example for deciding if your static type system is good enough to help you do real work.

You may be a top PL expert, but that doesn't make you a software engineering expert, if there is such a thing.

I'm anything but an expert in the academic sense, I'm 100% self-taught. My first serious language was Java, then I became a raving Pythonista for several years (mostly a reaction to Java), and then realized static typing didn't have to suck, because I saw Vyper, which was written in Ocaml. That led to Haskell, Dylan, and lots of others, including Nice.

With all that, I'm still under a decade of work experience in the field, so I'm not trying to tell anyone how to do his or her job, or how to write software. I'm just saying I've found real, compelling advantages to modern static typing, despite having seen, and loved, the other side.

If the type system doesn't allow something that would otherwise be legal (i.e. no run-time error) and has no easy workaround, it's the type system's fault, pure and simple. The best you can say in that situation is that it's too hard to do properly. Don't claim that anything that doesn't fit in the type system must be somehow wrong.

class Customer {
    String name;
}

String name(Object o) = throw new Exception("Sorry, you knew the rules!");

name(Map m) = cast(m[cast("name")]);
name(Customer c) = c.name;

void main(String[] args) {
  let list = [new Customer(name: "Fred"), [("name", "Barney")].listToMap()];
  for(obj : list)
     println(obj.name);
}

I think this entry helps me understand a lot of the, er, dynamic here lately. Brynn is saying that he's a convert to static typing. I've acknowledged that I also am a convert to static typing. And I wonder whether, just as there's no pain in the neck like an ex-smoker talking to a smoker, a health freak who used to be a 400 lbs. walking heart attack, or (forgive me) a religious convert proselytizing, people like Brynn and myself aren't just passionate converts, having difficulty why what we see isn't obvious to everyone.

I do know that I contribute to the sense of talking at cross-purposes more than I intend to. I realize this when examples like the "list-of-customers-and-dictionaries" not only fail to persuade me, they make me wonder what my interlocutor is thinking. You can say "would otherwise be legal (i.e. no run-time error)" all you like, but you can't prove it, and if you claim that it doesn't matter to you that you can't prove it, all you've done is recapitulated the difference between type theorists and non-type-theorists.

Maybe this is what's happened; we've hit bottom. But at least we haven't "gone wrong." :-)

if you claim that it doesn't matter to you that you can't prove it

Can you explain why it does matter that you can prove it?

I claim the proof itself is almost irrelevant for most systems, with the usual exceptions for truly mission-critical situations (aerospace, self-guided missiles, surgery tools...)

For most systems, the real-world benefits are:

• Convenience - catching errors earlier, saving time. Sure, this is a consequence of the "proof" aspect, but its not the proof that's the point. It's convenience. If that's forgotten - e.g., if you have to trade off convenience for proof - then the benefit is reduced.
• Better, machine-checkable documentation and enforcement for interfaces between modules. Again, there's a connection here to proofs, but again, static proofs are not the point, and any cost for achieving static proofs will not be gladly paid.

The problem with Haskell, ML, OCaml et al is that for them, static proofs are an end goal in themselves; whereas for most real systems, proofs just aren't the point, and never will be.

It's very hard to respond to this in the general case because I admit that I end up appealing to an intuition that doesn't appear to be widely shared: people appear to be quite comfortable even developing man-rated software in languages that have no formal semantics and are not memory-safe (C, C++), so whatever I might say here will, by definition, go against the tide. With that said, perhaps what I should do instead is go farther. If what I have to say is admittedly subjective, why not go so far as to become speculative?

I'm still naïve enough to believe that computing can change the world. I believe that we can have ubiquitous cooperation among mutually distrustful pieces of software without vulnerability, up to and including having digital cash and many other vastly more interesting smart contracts. I believe that it's possible to develop software that can adapt to environmental changes in a robust and human-acceptable way rather than crashiing when the environment changes out from under it. I believe that it should be possible for non-experts to write software using tools that exhibit gentle-slope characteristics: that the dichotomies between "scripting" and "industrial-strength," "interpreted" and "compiled," "local" and "distributed," "Von Neumann" and "concurrent," to say nothing of between "imperative," "object-oriented," "functional," "logic," and "constraint," are all artificial. Heck, for that matter, so is "compile time" and "runtime;" it should be possible to treat the difference there as merely an optimization question.

As of this writing, my speculative thesis is largely a matter of what's referred to as "theoretical computer science," although this being Lambda the Ultimate, there's quite a lot more nibbling around the edges of this stuff here than there is in any other single place that I know of, which is one reason of several that I think the name is so apropos. If you ask me for cites on any of the topics alluded to above, I can and will happily provide them. Or you can just google "site:lambda-the-ultimate.org snively" and start reading. ;-)

What this has to do with proofs is quite simple in a certain narrow sense: I want software to keep doing harder and harder things to get right. Put slightly more concretely, I want software to augment human intelligence, not merely reflect it. Let's take Flow Caml as an example. It allows me to define a security policy as a lattice of principals and actions, annotate only crucial parts of my code with information about the policy, and the compiler will guarantee that the policy is adhered to. In a world in which billions of dollars in ecommerce is conducted annually and in which databases of credit card numbers sit on web servers for the taking, to say nothing of our law enforcement and national security needs, doesn't this seem like a worthwhile thing to have a proof of correctness for? If someone claimed this for a 250,000-line C++ program—that it had a formal security policy and didn't violate it—would you believe it? On what grounds?

OK, so that was a big example. What about the example of selling a modern shrink-wrapped productivity application such as Microsoft Word or Adobe Photoshop? Am I the only person who's bothered by the MTBF on these things? Part of what astonishes and dismays me is that after a mere 30 years of personal computing we've allowed our expectations to be set so low: software fails. When it fails, it often takes down the entire process and sometimes, especially until about 3-5 years ago, could take down the entire machine. When it does that, any data that the user hasn't "saved" is lost.

Why do I need to "save" it? Why isn't it "safe" once I've entered it? Where am I "saving" it to? How come I can only take back my last command or revert to my last "document?" For that matter, why can't I just turn off the machine whenever I want, and when I turn it back on, it's in exactly the same state it was when I turned it off, modulo authentication?

If software development has a problem—and with an 85% project failure rate, it's awfully damned clear that software development doesn't have a problem; it has a full-on crisis—it's that software developers don't take it seriously. As an industry, we honestly believe that whole-processs and even whole-machine crashes are not only inevitable but are de rigeur. We believe it's impossible to eradicate worms, viruses, and spam. We would never trust an economy built on digital cash, and if someone were to develop, e.g. an MMORPG with digital cash and an exchange service for real cash, we'd expect the proprietors to get ripped off blind. We think it's OK that users have to know the difference between RAM and hard disk; we see no need for transactional persistence across the board; we believe it's character-building for them to lose data from time to time. And of course you have to wait for your OS to come back when you reboot, then you have to relaunch your apps, then open your documents again. How else could it be?

What we're left with—and I hate to say this—is mostly trivial software, lost data, frustrated users of trivial software, nervous users of what little non-trivial software exists, and entire application domains that remain unaddressed because no one would dare trust a piece of software that attempted to address them.

These observations are far from original with me; Alan Kay is in a much better position than I am to make them, and did so with his characteristic blend of history, insight, and wit at the O'Reilly Emerging Technology Conference in 2003. Videos of his presentation are available at <http://www.lisarein.com/alankay/tour.html>. These are well worth viewing if only for the presentations of Ivan Sutherland's "Sketchpad" and Doug Englebart's "NLS" systems: it's astonishing to see where the state of the art actually was circa 1968 and, by extension, how fundamentally lousy a job we've done at going beyond since.

Kay takes a hard opposite perspective to mine on the static typing vs. late binding question, saying, in summary (not a direct quote), "What to do until software engineering is invented... do late binding, which means being able to make the changes easily." Actually, perhaps it's not really opposite, since he could be interpreted to mean "either do software engineering if you can or make the cost of changes as low as possible, which is best done at the current state of the art with late binding." That is, get out of these tools that do neither software engineering nor dynamic change well (C, C++, Java...) and either head for software engineering (SML, O'Caml, Haskell, Concurrent Clean, Epigram, Alice...) or head for late binding (Common Lisp, Scheme, Smalltalk, Oz...). Formulated that way, I can't help but agree with him, and merely choose to focus on heading towards software engineering after spending decades in late binding.

Anton: For most systems, the real-world benefits are... The problem with Haskell, ML, OCaml et al is that for them, static proofs are an end goal in themselves; whereas for most real systems, proofs just aren't the point, and never will be.

My argument is that this tends to keep software in the ghetto of the trivial. By way of contrast, consider the rigor inherent in developing <http://manju.cs.berkeley.edu/ccured>, <http://www.lsv.ens-cachan.fr/~cortier/EVA/eva-comp.php>, or <http://sumo-pbil.ibcp.fr>, for example.

So I have to respectfully disagree that for Haskell, O'Caml, et al "static proofs are an end goal in themselves," or at least it's no more true than it is for C or C++, which are also statically typed. On the contrary, the ML family arose precisely out of needing to address a domain—automated theorem proving—that would have been excruciatingly poorly served by the popular mainstream languages. What's been fascinating since then is how far the ML family (including, by wild abuse of analogy, Haskell) has strayed from its theorem-proving roots: it's hard to see a connection between that and <http://www.cs.caltech.edu/~jyh/ejb or <http://cs-people.bu.edu/liulk/slurpcast>, for example, although the latter does lapse into formality by saying:

The main interest of this project is to provide a foundation for typed transport protocol experiments. We hope to promote the use of functional programming language for writing applications because we believe that functional programming enables us to write very scalable programs. This initial effort provided us with insights of inner workings of a streaming server.

• type-safe interaction between programs, with marshal and unmarshal primitives;
• dynamic loading and controlled rebinding to local resources; modules and abstract types with abstraction boundaries that are respected by interaction;
• global names, generated either freshly or based on module hashes: at the type level, as runtime names for abstract types; and at the term level, as channel names and other interaction handles;
• versions and version constraints, integrated with type identity;
• local concurrency and thread thunkification; and
• second-order polymorphism with a namecase construct.

• Know that my code is deadlock-free.
• Know that my code is race-condition free.
• Know that my code doesn't leak authority.
• Know that my code is upgradable without violating encapsulation or leaking authority.
• Will parallelize across multiple processors automagically when possible and serialize when it's not.
• Will not throw an exception that will not be caught and handled.
• Will have inferred all memory allocation and deallocation and do it automagically for me, letting me know if the dynamic characteristics of my code require the linking of a garbage collector.
• Will let me know if I attempt to take the tail of an empty list. :-)

Thanks, that was an enjoyable post. I certainly won't argue with the desire to take giant leaps forward in the state of software technology, and of course, that all has to start with languages.

But there's one crucial connection that I think is missing: any convincing demonstration that the static proof aspect of typesystems in current functional languages will actually help significantly with the things you've mentioned.

Remember, I'm not arguing against better type systems, or better semantics for languages: I'm saying that for most real-life purposes, the "static proof" aspect is seriously overrated as a benefit.

Even for something like the security example you mentioned, there's no particularly strong reason that you need to statically prove that a program doesn't violate security policy, as long as when it actually tries to violate policy, it's prevented from doing so.

I'm not saying there's no benefit to a static proof in this case, but it's nowhere near as strong a benefit as you seem to be implying.

Also, I suspect that the majority of people working in industry who're reading your posts aren't working on the sort of systems you're talking about - so when you write about these advanced needs for static proofs, they'll just say "oh, ok, that doesn't apply to me then". If you really want to encourage the adoption of better tools, techniques and practices, you need arguments that will make sense in more common scenarios. And "static proof" is not such an argument.

Heck, for that matter, so is "compile time" and "runtime;" it should be possible to treat the difference there as merely an optimization question.

Hey, good idea! Except if you move type checking from compile time to runtime, you lose your static proof capability. :)

At the end of the day, I want modern type theoretic ideas in my programming language...

So do I! But it doesn't all necessarily have to be statically checked.

...so that, at compile time, I can: [list snipped]

Alright, let's say I agree with that list, I want to be able to assure all of those things statically. How many of those can I actually do today, for a real system? Cobbling together a bunch of research projects doesn't count. The answer, I think, is not enough to rise to the level of "must have". If you could point to a single language or even a set of languages that would let me do all of these things in a real system today, and some examples of real systems that were doing these things, then I'd probably have to say you're right.

But we're not there today, and you can't point to existing languages and claim that they have all of these real benefits. So you're really arguing that static proof will become more important in future because of the kinds of things you'll be able to do with it. I look forward to that! But that's not much use for someone choosing tools today.

As for whether the static proofs are an end unto themselves for static functional languages, I was trying to characterize a mindset that can be found amongst many proponents of those languages. I'm perfectly happy modifying that claim to say, as I did above, that the benefits of static proofs are overrated in most real-world cases. And, as I said, the reason it's worth caring about that, is that with the state of the art right now, "static proof" is not an argument that's going to convince anyone who isn't already convinced - nor should it.

Not really. By your logic, we don't need any guarantees that programs don't violate security policies, since programs run on operating systems and part of the job of an operating system is to enforce security policies! Of course, the problem with this argument is that operating systems sometimes have flaws that allow programs to violate security policies. There can be no guarantee that programs that try to violate security policies will be prevented from doing so without some sort of guarantee of the correctness of the underlying operating system. So there's still a basic need for some sort of method for proving properties of programs statically, it's just a matter of whether you choose to verify the operating system or individual programs.

You're saying that layered security is good, for redundancy reasons, and that adding a layer at the compiler level would help. The viability of that would depend enormously on the overall environment, though.

For a start, the main scenario in which compile-time checks can add real security is when the source to the untrusted code is available to the system running it. That rules out a huge percentage of commercial scenarios. Even statically checkable bytecode is a problem - companies that want to protect their code know that bytecode can be more easily reverse engineered than native code.

To get around that issue, you'd need something like compilers which cryptographically sign code that they compile. But unless the compilation is done centrally by a trusted compiling service, those compilers would be in the hands of users who could find various ways to compromise them, and get them to sign code that shouldn't be signed.

So, I stand by the claim that verifying security policies via static typechecking, is not "a particularly strong reason" to need static proofs, in the real world, and certainly not today. Even if it has relevance in future, that still isn't much of an argument for static code proofs today.

If you can ensure the system is deadlock-free without running it, you know you can get by with a simpler runtime system, a more simple design (no need to handle most deadlock situations) etc.

It is basically easy to check local properties at run time (e.g., am I trying to apply integer addition to strings), much harder to verify non-local properties.

Type systems help in both cases, so we shouldn't forget about the non-local case, which raises interesting issues.

Proof-carrying code has none of this problems. It's statically checkable, doesn't require a cryptographically signed binaries or trusted compilers, can be used with real machine code and don't need to have the source available. This paper is really enlightening in this issue:
Safe Kernel Extensions Without Run-Time Checking.

Excellent! After the lengthy and now regretably terminated interaction with Peter, I confess to feeling that I'm entirely too strident on these issues vs. merely feeling strongly about them (which I obviously do), but being able to have a reasonable (even enjoyable!) conversation about them.

Anton: I certainly won't argue with the desire to take giant leaps forward in the state of software technology, and of course, that all has to start with languages.

That's a nice crisp articulation of where the static typing and dynamic checking communities find common ground. And of course I'm aware of both your sincerity and genuine interest in the static typing side of the question, since you started the thread.

Anton: But there's one crucial connection that I think is missing: any convincing demonstration that the static proof aspect of typesystems in current functional languages will actually help significantly with the things you've mentioned.

Oh, absolutely right, which is why I was quite cautious to explain that I was going to go into a more speculative mode versus continuing the debate about where we find ourselves with our current languages and their type systems. To a first approximation (insert wild handwaving here), what you get from Hindley-Milner (SML, O'Caml, Haskell—strictly speaking, read "Algorithm W") as implemented in the type systems of the current batch of type-inferred languages is analogous to what you get from type annotation in C/C++/Java, or, from a runtime perspective, from the design of the runtime systems of Common Lisp, Scheme, Python, Perl, Ruby, Groovy... Given this, I think it blurs the issue and leads to debates that really are more about the current languages and type systems than about static-typeness or type theory. So I was making an attempt to move beyond the arguably epsilon-magnitude deltas.

Anton: Remember, I'm not arguing against better type systems, or better semantics for languages: I'm saying that for most real-life purposes, the "static proof" aspect is seriously overrated as a benefit.

Absolutely. And I'm calling that the ghetto of trivial software, by which I mean that what we call "most real-life purposes" are, to some extent, shaped by what we perceive ourselves to be able to do, and to some extent what we perceive ourselves to be able to do is shaped by our tool choices. Read Paul Graham's work if you haven't already for lots of material delivered from this perspective.

Anton: Even for something like the security example you mentioned, there's no particularly strong reason that you need to statically prove that a program doesn't violate security policy, as long as when it actually tries to violate policy, it's prevented from doing so.

I don't know about this. People claim to ship secure software all the time and it still succumbs to attacks. No doubt there's some middle ground between the way security is generally done now (i.e. it isn't in any meaningful way) and making security an aspect of your type system. Just proving critical components/algorithms of your system correct would be a great start. But there's also a nasty pragmatic issue here. Capability security, for example, arose in the operating system community in the 1960s, but was largely abandoned not long thereafter, partially on pragmatic grounds: fine-grained checking of capability invocation, especially where user space/kernel space boundaries are crossed per-check, is extremely expensive. This is definitely an area where the "optimization" of doing as much as possible at compile time can make the difference between having a feasible and an infeasible system. In this case, you essentially get the "proof" for free ("types as proofs"), which is a nice side benefit when you're talking about security.

Anton: I'm not saying there's no benefit to a static proof in this case, but it's nowhere near as strong a benefit as you seem to be implying.

I have to respectfully disagree. Again, the major point behind putting features into type systems is so that users of the type system can develop correct code without necessarily having to understand the theory behind the type system: it's a small, but IMHO crucial, step towards addressing "Formal methods will never have any impact until they can be used by people that don’t understand them," which is attributed to Tom Melham. As Pierce points out in "Types and Programming Languages," type systems are a "lightweight formal method" that lots of people who don't understand them use successfully every day.

Anton: Also, I suspect that the majority of people working in industry who're reading your posts aren't working on the sort of systems you're talking about - so when you write about these advanced needs for static proofs, they'll just say "oh, ok, that doesn't apply to me then".

I don't know how to respond to this any differently than I did before: it seems to me like a chicken and egg problem. Are people not doing these things because they don't want to/there's no point to them, or because at the current state of the art it's too costly to pursue them? My very strong belief is that it's the latter. To keep it perhaps a bit closer to a current contextual frame, you surely can't honestly be suggesting that C++ is an adequate language in which to develop highly-available, scalable, reliable, secure distributed systems, right? Yet that's what I try to do every day at my job, and guess what? We fight deadlock, race conditions, system throughput, object persistence, serialization issues, and security every day. To most of the team, the idea of changing languages would be laughable, but quite honestly I can't tell you how much better off we'd be developing in Erlang or Oz or Alice. And yes, I'm mindful of the fact that Erlang and Oz are dynamically checked. I do know that Oz at least has a formal semantics, which helps me be accepting of it. Heck, it even has an animated virtual machine at <http://www.imit.kth.se/~schulte/misc/vamoz.html>, so if you like the PLT reduction semantics library this might also be worth checking out.

Anton: If you really want to encourage the adoption of better tools, techniques and practices, you need arguments that will make sense in more common scenarios. And "static proof" is not such an argument.

At the moment, the argument remains that inferred static types allow me to write highly-performant correct code more quickly than the alternatives. There's definitely a sense in which the correctness argument is a statement of faith: I trust that the type system is correct and implemented correctly. But IMHO, that's preferable to trusting that the code that I wrote isn't going to fail in some unpredictable way at runtime because I neglected to handle a case that can actually arise in the wild but is only checked dynamically.

The trust argument might be worth making a point about explicitly: I need to be able to trust my compiler, and one of the other things that's essentially taken for granted in my experience of assembly language, Pascal, C, and C++ is that compiler bugs happen. While it's certainly true that compiler bugs happen in Haskell, O'Caml, and SML too, they seem to be both more rare and hanging around rather extreme edge cases that don't affect 99% or more of users. And when they're fixed they tend to stay fixed and not exhibit unpredictable effects on other aspects of the compiler. So it seems to me that the evolution of the tools themselves reflects the benefits of their own architectural choices.

Me: Heck, for that matter, so is "compile time" and "runtime;" it should be possible to treat the difference there as merely an optimization question.

Anton: Hey, good idea! Except if you move type checking from compile time to runtime, you lose your static proof capability. :)

Right, so don't move all of your computation to runtime! :-)

More seriously, though, I'm keenly interested in multi-stage programming a la <http://www.metaocaml.org/tutorial04>, where we find:

MetaOCaml is a programming language that provides special support for MSP by providing:

• Hygienic quasi-quotation notation for distinguishing different computational stages (that is, the generating vs. the generated code) in a program, and
• An evaluation construct that allows generated code to be generated and executed at runtime, and
• A type system that statically ensures that this is done safely.

Me: At the end of the day, I want modern type theoretic ideas in my programming language...

Anton: So do I! But it doesn't all necessarily have to be statically checked.

And now we're back to "if it isn't statically checked, it isn't type-theoretic."

Anton: Alright, let's say I agree with that list, I want to be able to assure all of those things statically. How many of those can I actually do today, for a real system?

N, where N is the length of the list. The problem is that the container isn't a bag; it's a set. Its members are disjoint. :-)

Anton: Cobbling together a bunch of research projects doesn't count.

It does when what you're doing is a proof-by-demonstration that type systems can do all of these things. The next step is to come up with one type system that does all of these things.

Anton: The answer, I think, is not enough to rise to the level of "must have". If you could point to a single language or even a set of languages that would let me do all of these things in a real system today, and some examples of real systems that were doing these things, then I'd probably have to say you're right.

But I or others have already pointed to all of these systems; they do exist. All I've done is made reference to them. And "real systems that were doing these things" at this juncture is irrelevant to me. I'm not talking about industry "best" (read: average, cf. Erann Gat) practices or conventional commercial wisdom here. I'm explicitly talking about what type systems are capable of and why getting software out of the ghetto of the trivial relies upon them. This kind of argumentation is what I mean when I say that I worry about people moving the goalposts. "But the things you're talking about aren't in large-scale production; they aren't popular!" Well, no. If they were, they wouldn't be research; if they weren't research, they wouldn't be advancing the state of the art.

Anton: But we're not there today, and you can't point to existing languages and claim that they have all of these real benefits.

No; I can point to languages and claim that they have all of these real benefits. What I can't do is point to a language and claim that it has all of these real benefits.

Anton: So you're really arguing that static proof will become more important in future because of the kinds of things you'll be able to do with it. I look forward to that! But that's not much use for someone choosing tools today.

I think the premise is fair but the conclusion is flawed. Consider that new technology adoption uptake requires an average of a decade. Consider further that choosing a new language has life-altering consequences in terms of becoming fluent in the language, becoming a member of a different community and largely leaving the old one behind with all that implies, and learning to use available idioms, patterns, and libraries effectively. If this is your profession, it could also mean replacing your client base. It's just an enormous commitment, so if you believe that this is something to look forward to, my assertion would be that there's no time to get ready like the present: learning about module systems, dependent and phantom types, type classes, monads, etc. should keep anyone busy until the unification and mainstreaming comes. :-)

Anton: As for whether the static proofs are an end unto themselves for static functional languages, I was trying to characterize a mindset that can be found amongst many proponents of those languages.

Sure, myself included. I would make the same observation that I made to Peter: even if you use a simply-typed type-annotated language such as C, C++, or Java, you are, in fact, relying on your compiler to perform static proofs of correctness of some aspects of your code. All that statically-typed type-inferred languages do is expand the scope of those proofs, and maybe do so enough that requiring type annotation would be cost-prohibitive, so they strive to make that unnecessary. Why this gets such strong push-back from some quarters baffles me.

Anton: I'm perfectly happy modifying that claim to say, as I did above, that the benefits of static proofs are overrated in most real-world cases.

Right. And I'm saying that the real world reflects expressive limtations of its current tools, by which I obviously don't mean "lack of Turing equivalence," but rather the cost of expressing classes of notions that are difficult to convey using currently-popular languages.

Anton: And, as I said, the reason it's worth caring about that, is that with the state of the art right now, "static proof" is not an argument that's going to convince anyone who isn't already convinced - nor should it.

I still feel this is too strong, but not by much. If it were uniformly the case, you wouldn't have converts like Brynn Keller and myself. So it's worth having the discussion even in the context of the available statically typed, type-inferred languages because some folks aren't using them because they don't know that they exist, or because they have the erroneous impression that they don't perform well, or that they don't interface with C APIs well.

That's bad enough, but that's just ignorance; it's easily corrected. Once in a while, though, I come across someone who actually seems to believe what I attributed to Peter before he left: that he sincerely believed the contradictory propositions that while SML/O'Caml/Haskell do, in fact, make stronger correctness guarantees than, e.g. Pascal/C/C++/Java, it's still "just as necessary" to test whatever those guarantees are as it is in Pascal/C/C++/Java. This kind of arrant nonsense I won't tolerate. I don't see folks writing tests for their C compiler's definition of "int." So people who claim this are either deluding themselves, by which I mean that either they don't believe one of the contradictory propositions that they claim to believe or that their logic is so flawed that they can't see that the propositions are contradictory, or their actual motivation for rejecting statically-typed type-inferred languages lies elsewhere. In my experience, it typically lies along what I've described elsewhere as sociological dimensions. No programmer seems to want to admit this, which to me is ironic; as I've also written elsewhere, sociological issues count, and particularly when the technical differences between one option and another are at epsilon magnitude, the sociological issues are overwhelmingly likely to dominate the decision. That's OK; that's healthy; that's constructive. It'd just be nice if we could be more honest about it, and from this particular dynamic-checking-to-type-theory convert's POV, there isn't generally a lot of honesty in the debate with dynamic checking aficionados regarding what the issues are.

Even for something like the security example you mentioned, there's no particularly strong reason that you need to statically prove that a program doesn't violate security policy, as long as when it actually tries to violate policy, it's prevented from doing so.

There are cases where the effort required to correctly prevent the violation at runtime is much harder than the statically inferred properties. For example assume program_b has a tighter policy than program_a:

program_a param =
    let func x y = ...
    in program_b param func

func should be able to do everything program_a can do even when executed by program_b, which can't do things that func does by himself. This kind of problem can be solved with static analisys but in the runtime we should be able to annotate func with backdoors to program_b's sandbox and in some way verify that program_b's parameters to func don't abuse this backdoor (e.g. if func is a HOF the functions given by program_b should respect its policy unless otherwise stated).

Hey, good idea! Except if you move type checking from compile time to runtime, you lose your static proof capability.

That's not true. If we use a staging system we can ensure that every program constructed in stage N is type-safe before executing it in stage N + K.

Alright, let's say I agree with that list, I want to be able to assure all of those things statically. How many of those can I actually do today, for a real system? Cobbling together a bunch of research projects doesn't count. The answer, I think, is not enough to rise to the level of "must have". If you could point to a single language or even a set of languages that would let me do all of these things in a real system today, and some examples of real systems that were doing these things, then I'd probably have to say you're right.

Well the proposition here is that some kind of statically verifiable behavior is better than none. In DTLs we have X possible classes of errors and in STLs we have Y possible classes of errors where 0 < Y < X. So STLs provide value even if some of the errors in DTLs are still possible.

the benefits of static proofs are overrated in most real-world cases.

IME one of the most important sources of problems in large projects (more than 4 people for more than 3 months) is communicating the contracts of programs. Usually we need some kind of coding standard to decide what are the best practices (e.g. exceptions vs. error values, real nulls vs. null objects, immutable objects, border conditions, when to catch exceptions) and we need to ensure that not only the practices are being followed but when should we break them (e.g. calling third-part libraries). The simplest example that sold me to ST was Maybe (or Option) type. If I'm using Smalltalk I never know if a particular message will return Nil or an empty collection: I always need to check the documentation and trust the programmer to have followed it carefully, correctly verifying all possible error situations. Now with Maybe types the compiler will never allow a Customer -> [Order] function to return Nothing. This kind of proof is, IMO, quite underrated IMO: we usually forget how many hours we spent getting burned by this kind of problem and the effort used to build the discipline necessary to avoid them.

Hey, good idea! Except if you move type checking from compile time to runtime, you lose your static proof capability.

That's not true. If we use a staging system we can ensure that every program constructed in stage N is type-safe before executing it in stage N + K.

Word "stratified" comes to mind, from dramatic times of Russel and Frege.

Modern type systems use stratification in form of various devices.

Mario, I don't understand your Groovy code example. Are you sure it's correct? (I'm looking at the docs, such as they are, right now.)

>>> listOfPeople = [ new Customer("James"), new Customer("Bob"), { "name" : "A map" } ];
>>> names = listOfPeople.name;
>>> println(names);
["James", "Bob", "A Map"]

I assume that Customer is an object that supports the name method. But you apply name to listOfPeople, which is a list. Don't you mean something like listOfPeople.map { it.name }? (There is no map method apparently, but who cares...)

Also, it seems that { "name" : "A map" }.name should raise an error; to get the value associated with key "name" you need to write { "name" : "A map" }.get("name").

If you fix these issues (for example, make Customer a subclass of Map), does your complaint still persist?

It's the fourth example on this page.

I suppose this is the kind of righteous posture that makes people use untyped languages. You can't ask for a "justification" for everything people want to do with the language.

"Ours is not to reason why, ours is but to do or die." On the whole, I agree with this sentiment. But consider this example:

[13, "foo", new Bar(), 9.1]

By the aforementioned principle, it is not my job as PL designer to ask why someone would want to do this. But what can they do with it? Basically, they have to traverse the list and do a typecase on each element. And this is essentially also what you have to do in a typed language, if you represent this using Univ. So I don't see much need to provide a "typed version" of this idiom.

The Groovy example is admittedly a bit different, but look at all the problems with it:

• It breaks lexical scoping, since name is not bound in that scope.
• It breaks encapsulation of lists, since you can (successfully) invoke any method on a list.
• What would happen if the "property" name were actually a list method? (And suppose I subclassed it.)

These are issues which, admittedly, complicate typing, but also are legitimate issues for untyped languages. Rejecting the construction on these grounds is not self-righteous or exclusionary or whatever.

I think it is not the duty of a PL designer to try to figure out a way to type every crazy construction which users (or the W3C) come up with. If you do so, you will eventually break every property of the language and end up with a pile of mud.

The constructions we want to type are the ones which preserve the direction in which the language is heading, and the commitments it has made. If, as a PL designer, I were put in a position where it became important to support such a construction, I would look for a different way to do it which preserves the spirit of the language.

This has nothing to do with typing, really. Just consider Haskell: it's a lazy pure functional language. If some user comes along and says, "Hey wouldn't it be great if you could mutate values? Here is an example in my program where I would find this really useful." Well, I think there is nothing self-righteous in saying to such a person, "Forget it; referential transparency is more important," or "You will have to use monads; you painted yourself into a corner because you didn't know any better."

Now, if this were Typed Perl, where the idea is that "there's more than one way to do it," and elegance is not a priority, and "who cares about referential transparency?!", then it might be in the spirit of the language to search for a way to type your Groovy example. But I think people who believe in expressive typing generally don't agree with those principles.

(And, BTW, even Larry Wall undoubtedly has principles which he is unwilling to bend. I admit I think they're inconsistent, but he believes they are. If you look at the "apocalypses", after all, he rejects or changes the majority of language proposals.)

These are issues which, admittedly, complicate typing, but also are legitimate issues for untyped languages. Rejecting the construction on these grounds is not self-righteous or exclusionary or whatever.

I think the only way out is to admit that there will always be two groups of languages: those optimized for programmers' convenience, and those optimized for sound engineering practices. I'm not saying that the first group should abandon static typing altogether; it should do as much static typing as possible without making it a hassle. The "sound practices" languages, on the other hand, should require explicit type annotations even in places where they could be inferred.

I'm not trying to weasel out. As I said before, I completely agree that having types is always better than not having them, everything else being the same. But everything else is never the same in practice. What we need for dynamic languages are type systems that can work on a subset of the language they can handle and just leave the rest alone. The Template Haskell example is that kind of compromise. I don't believe that even hardcore Perl fans would object to a type-checker that doesn't require any annotations and reports only errors that would occur at run-time anyway.

It would be a shame if "dynamic" people were left with inferior tools just because type theorists are preoccupied with sound engineering practices and all-encompassing type systems. I'm not implying anything or accusing anybody, just pointing out a potential danger. Misunderstandings can cause wars.

Where's that quote coming from?

At one extreme, dynamic-typing crowd would argue that it's never a language designer's job to define what's a sound software engineering practice.

There is a difference between defining "sound engineering practice" and enabling it. We have agreed, finally, that in a typed language it is possible to write untyped programs, so typed languages enable any kind of design pattern that is possible in an untyped language—up to syntax, and even that can be fixed with a quotation mechanism, like, say, in Template Haskell or camlp4.

I think that's enough.

I do think it is the PL designer's job to identify effective programming techniques, and enable them; I don't think it is his/her job to figure out how to express every possible construction using the available features—there just isn't time enough for that. The designer should develop the feature, show some important examples of its use, provide feedback and clarification on major issues, and the rest is up to users.

And, sorry to put it this way but, I don't see that that Groovy example is worth my time to investigate.

What we need for dynamic languages are type systems that can work on a subset of the language they can handle and just leave the rest alone.

What bothers me about this is that, again, typed programs are not annotated untyped programs, and so one does not write a typed program in the same way as its type-erased version. So it is not a question of trying to "lift" every untyped idiom to a typed idiom. For me it is enough that every untyped idiom can be expressed via Univ.

Where's that quote coming from?

Actually, I got it wrong.

Their's not to reason why,
Their's but to do and die:
Into the valley of Death
    Rode the six hundred.
— The Charge of the Light Brigade, Alfred, Lord Tennyson

What we need for dynamic languages are type systems that can work on a subset of the language they can handle and just leave the rest alone.

What bothers me about this is that, again, typed programs are not annotated untyped programs, and so one does not write a typed program in the same way as its type-erased version. So it is not a question of trying to "lift" every untyped idiom to a typed idiom. For me it is enough that every untyped idiom can be expressed via Univ.

Some of this went over my head, I'm afraid. Could you clarify what you mean by "enough"? If you were using Template Haskell, would you be completely satisfied with its Univ-style embedding, or would you desire a finer type system? If former, then why do you consider the same solution so unsatisfactory for the language as the whole? If the latter, then why aren't other un(i)typed languages worthy of a better type system?

Nevermind the parent post—I didn't manage to say what was in my head.

What I wanted to say was, although I think PL designers should be agnostic in a sense, I think agnosticism paradoxically requires bias: choosing some engineering practices over others, and then recovering the road not taken by other means. The reason is that some "best practices" contradict each other, so you cannot simultaneously support all of them "at the same level."

For example, consider mutation. On one hand, mutation is undeniably useful (see, for example, Peter van Roy's "Concepts" book). OTOH, in the FP community many people argue that mutation should be used as little as possible. So by outlawing mutation as in Haskell, you are violating one best practice, while by supporting it as in ML you are violating another. However, you can appease both sides, in a way, by a mechanism like monads: Haskell is pure, but mutation is possible in a monad, so monadic programs are impure. What you have done is made one thing the default, but supported the other by pushing it to another level.

Typing is similar. Strictly speaking, one cannot simultaneously support dynamic typing and static typing. However, by committing to static typing, you can embed every DT program using a type like Univ. Here again, you have supported conflicting features by pushing one to another level.

With mutation, I think you can take the opposite approach as well: support mutation globally, but introduce an effects system so that certain programs are statically known to be pure. I don't think the same is possible with typing.

Algebraically, this reminds me of universal constructions; I would say, "mutation factors through referential transparency + monads" and "dynamic typing factors through static typing + recursion".

And if the language supports macros, then, you can more or less make the language appear unbiased. For example, I showed below how to use a quotation mechanism to relieve the syntactic burden of embedding untyped programs in a typed language. I think a similar thing can be done for mutation and monads.

I think it is not the duty of a PL designer to try to figure out a way to type every crazy construction which users (or the W3C) come up with.

That's true, but "every crazy construction" is at the extremes. There's plenty of scope for providing type systems that are more relaxed than current ones. And there would be demand for them, if they existed and worked well. Actually, demand for them might cut into demand for Haskell/ML-like type systems, so perhaps there's good reason to argue against such systems if you're a fan of fully static systems.

Current type systems are the way they are exactly because of they're driven by philosophies, as you say. But the philosophy that drives current static type systems is "static proofs uber alles". And, as I've just written in a response to Paul Snively, that's not all that relevant to most real systems.

There are some basic truths that won't ever go away, that aren't affected by some people's choice to play by stricter rules: not every program needs to be fully statically typed; and not every language needs to be able to infer the types of all of its terms. Better type systems for languages which recognize these truths will still be useful.

There's plenty of scope for providing type systems that are more relaxed than current ones.

There you go again. I think using the term "relax" to talk about increasing the expressivity of typing is exactly the wrong way to think about it. It's not about relaxing type systems so we can annotate more untyped programs; it's about making type systems more rigorous so we can express more dynamic behaviors.

A ring is more expressive than a monoid, yet set-theoretically the rings are a subset of the monoids.

The more you relax something, the less you can say about it. You can say very little about the set of all people in the world: they have little in common. You can say more about the set of all Americans, or the set of all basketball players, or the set of all programmers. And you can say the most about an individual. Making a set smaller increases its invariants.

But, I don't have the energy any more to get into this. :( This thread has worn me out, and it moves too fast for me now, and I have emails to answer and theses to write. Talk amongst yourselves. :)

There you go again. I think using the term "relax" to talk about increasing the expressivity of typing is exactly the wrong way to think about it. It's not about relaxing type systems so we can annotate more untyped programs; it's about making type systems more rigorous so we can express more dynamic behaviors.

That's precisely one of the points of disagreement. You're taking the above point as an article of faith, since you can't point to a type system that provides all the capabilities of dynamically-checked languages, including e.g. runtime evolvability. I'm not saying you're wrong, necessarily - but how many years will it be before you can demonstrate that you're right, with an actual language?

The more you relax something, the less you can say about it.

Exactly. And that's a feature - when you're prototyping, for example, or when you're developing a system whose specification is evolving as you develop it, and there are many aspects of the system that you can't say much about. You earlier mentioned the idea of types as a skeleton for an application - well, in the real world, having an application's skeleton be very flexible, even weakly defined, can be an enormous asset!

The idea that more rigour is better is simply one of perspective - it doesn't apply in all situations. While you're figuring out how to statically type the universe, people have real projects to get done, and if we want them to take advantage of better type systems, more relaxed type systems are one of the things that are going to be needed.

Take a look at the holes in the Java and C++ type systems - some of them are there for a reason. Upcasting and downcasting etc. are not necessarily things to be eliminated, they're features! However, the rest of those type systems could presumably be done better. And you could probably usefully add more holes into those type systems to produce useful languages.

The problem with what I'm saying is that there are certainly no end of applications for which more rigour is better, and with the predilections of academics such as yourself, that's what's going to get focused on, and you'll be able to point to high-tech applications and say "see?" But then you shouldn't be surprised when this stuff doesn't translate into the mainstream - it's because it's not delivering some of the features that count in those contexts.

Eh? Frank in particular has demonstrated, repeatedly, that in fact all typed languages have strictly greater expressive power than untyped languages. Untyped languages are a proper subset of typed languages. So the issue revolves around convenience and syntax, and Frank has also invested a fair amount of time in demonstrating that hygenic macros might address the syntactic convenience issue in writing Univ-based code in, e.g. Haskell. At this point I have to question what the point is. How much farther do you want to go with this? The fact that untyped languages have a syntactic convenience advantage over SML/O'Caml/Haskell has been stipulated and addressed. What more do you want?

Regarding your specific example, "runtime evolvability," let's just take some information from a single post on this very weblog: Acute: high-level programming language design for distributed computation:

• type-safe interaction between programs, with marshal and unmarshal primitives;
• dynamic loading and controlled rebinding to local resources;
• versions and version constraints, integrated with type identity;

Anton: The problem with what I'm saying is that there are certainly no end of applications for which more rigour is better, and with the predilections of academics such as yourself, that's what's going to get focused on, and you'll be able to point to high-tech applications and say "see?" But then you shouldn't be surprised when this stuff doesn't translate into the mainstream - it's because it's not delivering some of the features that count in those contexts.

I now refer you to http://www.cl.cam.ac.uk/users/pes20/Netsem, in particular "Rigour is good for you and feasible: reflections on formal treatments of C and UDP sockets." It would be difficult indeed to get more hard-nosedly pragmatic than C and sockets.

I'm afraid that my conclusion remains what it has been for the past 3-5 years: the real problem is that once those committed to rigor deliver results, they discover that industry still can't be bothered to be rigorous.

Frank in particular has demonstrated, repeatedly, that in fact all typed languages have strictly greater expressive power than untyped languages. Untyped languages are a proper subset of typed languages.

I disputed this point, and Frank agreed with me: "It's true that Scheme, Perl, Python, etc. have a more concise syntax for untyped programs". That translates to their being more expressive for those programs. That's the state of the art right now.

How much farther do you want to go with this? The fact that untyped languages have a syntactic convenience advantage over SML/O'Caml/Haskell has been stipulated and addressed. What more do you want?

I'm saying that until these languages have been demonstrated being used successfully in the scenarios where untyped languages excel (e.g. here), whether untyped languages are a proper subset of typed languages is not very relevant to actual practice.

You quoted someone at Cambridge (maybe Peter Sewell, but the link was messed up):

I'm afraid that my conclusion remains what it has been for the past 3-5 years: the real problem is that once those committed to rigor deliver results, they discover that industry still can't be bothered to be rigorous.

This is more of the attitude that I'm arguing against: because they don't get the answer that makes them happy, some of these proponents of rigor assume the "other side" must be at fault. It never seems to occur to wonder whether there's something that's been overlooked in terms of real-world requirements. It's easy from the academic side to get infatuated with the beauty of a narrowly-focused theoretical system, forget about the hairy issues of integration with the rest of the world, and then blame everyone else when the results aren't universally acclaimed as being useful. Muttering about "industry still can't be bothered to be rigorous" is just the easy way out.

In this case, I absolutely see this happening with statically- vs. dynamically-checked languages. Frank's point about not relaxing typesystems is a case in point. Saying that the answer to the need for dynamic behaviors today is to press on with the development of more rigorous typesystems may be a theoretically valid answer - time will tell how complete an answer can be reached this way - but it's of no use to someone evaluating languages today.

Something similar goes for systems like Acute, as well as many of the other references you've given. Acute is described as an "experimental" language. So great, in future all these hard problems are going to be solved by advanced type systems. But that doesn't make, say, OCaml any more attractive, today. I can't count on Acute's functionality being integrated into OCaml, ever. Plus there are a dozen other capabilities that have been raised - which language is going to be the winner that ends up having the most useful combination of features? One of the most rational things a business can do in this scenario is wait, and to some extent, the same applies to the developers they employ. Unfortunately, that's going to be one helluva long wait, as long as there's so little focus on bridging the gap between beautiful formal systems that solve tough theoretical problems, and making them do something useful as part of other real systems.

But I'm saying there are lots of good uses for type systems, and there are lots of benefits from checking of types, and it is important to educate oneself about type theory. But you have to distinguish between the benefits that can be obtained now, and the benefits we expect these systems to provide at some indeterminate point in the future. Confusing those two is only going to lead to disillusionment - I don't think we want to be tricking people into using languages with advanced typesystems. You earlier said something about honesty in the debate with DT folk - but be careful that in your enthusiasm, they don't end up feeling the same way about you.

Also, there had better be better reasons to use those languages than that in future, they might become more useful.

That's where I was coming from regarding the benefits of static proof. "Static proof" is not a benefit in itself, for the most part, in industry. You can talk about it until you're blue in the face, and it won't get you anywhere. You have to be able to explicate the useful consequences of static proofs, in languages that are available today. Also, I think it's important to keep in mind that not all that is useful about type systems has to do with static proofs.

Ironically, talking about static proofs is a little similar to talking about "dynamic behaviors" as being important. To someone who hasn't actually experienced the underlying issues, this is meaningless. DT advocates aren't often very effective explicating these things, either. In the Udell story Ehud just posted, the linked article quotes Sean McGrath's remark, "anyone coding middleware in a statically compiled language, working in a commercial environment where time is money, has rocks in their head." Talk about an argument that's in the weeds! But are you entirely sure that there's absolutely no basis for these sorts of opinions? I'm pretty certain they do have a basis. Perhaps not as strong as its proponents think, but then something similar is true for "static proof". (Perhaps "static proof is dual to dynamic behavior", with apologies to Wadler.)

Eh? Frank in particular has demonstrated, repeatedly, that in fact all typed languages have strictly greater expressive power than untyped languages. Untyped languages are a proper subset of typed languages.

Geez, I really hate to wade in here. I have to say, though, that Frank didn't actually demonstrate that. He seems to believe it, and offers a lot of rhetoric :). He demonstrated one inclusion, and claimed of the other that he strongly suspected it was impossible.

But it's not. All of the latently typed (or whatever PC term you want to use) languages we're talking about are able to suspend evaluation (lambda anyone?) and most of them can even cons up code to evaluate at runtime.

The "dual" of the Univ construction is to represent staticly typed values by a pair of a type and the code for the value. In Scheme we can compile to closures, and we can use some special syntax for checking literals (just like Frank has to manually tag literals):

(define-syntax return
  (syntax-rules (int string)
    ((_ int lit)
     (if (integer? 'lit)
         (cons 'int (lambda () lit))
         (error 'return "type error")))
    ((_ string lit)
     (if (string? 'lit)
         (cons 'string (lambda () lit))
         (error 'return "type error")))))

We have to reimplement all the primitives (just like Frank does), providing checking versions of them:

(define plus
  (lambda (v0 v1)
    (if (and (eq? (car v0) 'int) (eq? (car v1) 'int))
        (cons 'int (lambda () (+ ((cdr v0)) ((cdr v1)))))
        (error 'plus "type error"))))

And of course, we have to use our own special application combinator---just like Frank does:

(define t-app
  (lambda (v0 v1)
    (if (and (function-type? (car v0))
             (eq? (argument-type (car v0)) (car v1)))
        (cons (return-type (car v0))
              (lambda () (((cdr v0)) ((cdr v1)))))
        (error 't-app "type error"))))

(which uses some helpers, below for the sake of completeness):

(define function-type?
  (lambda (obj)
    (and (vector obj)
         (= (vector-length obj) 3)
         (eq? (vector-ref obj 0) 'fun))))
(define argument-type (lambda (t) (vector-ref t 1)))
(define return-type (lambda (t) (vector-ref t 2)))

Lambda is a special form for convenience (but need not be, it could be a function that takes a thunk):

(define-syntax t-lambda
  (syntax-rules (:)
    ((_ (formal : type) body)
     (let ((p ((lambda (formal) body) (cons 'type (lambda () (void))))))
       (cons (vector 'fun 'type (car p))
             (lambda ()
               (lambda (v)
                 ((cdr ((lambda (formal) body)
                        (cons 'type (lambda () v))))))))))))

Now, a typed computation is the computation of a pair of a type and "code" (a thunk), or else an error. If we get a type (i.e., the code is well-typed), then we know staticly that our code cannot go wrong at "run-time". What's run-time? That's when we safely force that thunk:

(define-syntax run
  (syntax-rules ()
    ((_ exp) ((cdr exp)))))

You might object to this global last projection and application (to obtain a Scheme value), but it's the equivalent of the case dispatch required by Frank to extract an ML or Haskell value from his universal type.

For example:

Welcome to MzScheme version 208, Copyright (c) 2004 PLT Scheme, Inc.

> (t-app (t-lambda (x : int) (plus x x)) (return int 42))
(int . #<procedure:STDIN::6706>)

> (run (t-app (t-lambda (x : int) (plus x x)) (return int 42)))
84

> (t-lambda (x : string) (plus x x))
plus: type error

> (t-app (t-lambda (x : string) x) (return int 42))
t-app: type error

See? Staticly typed code in Scheme is no more inconvenient than untyped code in ML. So obviously (with tongue firmly in cheek), staticly typed languages offer no benefits except a convenient syntax for restricted code generation and some builtin checking algorithms.

Paul wrote:

Untyped languages are a proper subset of typed languages.

I probably said this to simplify the argument, but I knew it wasn't strictly true; I thought the distinction was academic, but it's not.

The unityped (note the "i") languages are a proper subset of the typed languages, but making an untyped language into a unityped language involves several global choices: a choice for the type which plays the role of Univ, and a choice for how to translate values into type Univ; modulo those choices, an untyped language is unityped. (I started writing a long post about this, but decided not to finish it and post it because I spend too much time on here anyway.)

Kevin wrote:

The "dual" of the Univ construction is to represent staticly typed values by a pair of a type and the code for the value.

Yes, you have divined a fault in my argument. I have, in fact, written code similar to yours, Kevin, but it depends on a global choice (see below), and that's why I thought it wasn't comparable to the Univ embedding. However, as I explained above, I realized recently that the Univ embedding also depends on a choice.

This method depends on a mechanism for doing static computations (here, the macro system); without that, you would have to stage your program into static and dynamic stages, and that involves a global transformation, which is a global choice. (You are making the choice here by opting to use the macro system to indicate what is static and what is dynamic.) This corresponds to the global choice you make when you pick the target type Univ.

The other thing is, to get the performance of a typed language, the compiler needs to be aware of this choice, to know where it can generate unsafe code (no unnecessary tags); this is about the same as saying that the compiler is a compiler for a typed language.

So, to summarize, I have to retract my claim. I don't see that a typed language is comparable to an untyped language without making some global choices, and if you allow a global choice to embed untyped in typed, then you can make a global choice to embed in the other direction. The unityped languages are inferior to many-typed languages in every way; however, an untyped language is not unityped.

Update: "The unityped languages are inferior to many-typed languages in every way". Well, actually not. Nat is all you need. But I don't want to get into that.

OK, this clarifies things dramatically, as did Kevin's post, and now I'm embarrassed not to have seen the flaw myself. Knowing of the Futamura projections alone should have suggested that the distinctions were not as strong as I had been making them out to be, by which I mean that the Futamura projections don't result in unityping! How embarrassing.

It's quite common for "path" languages to support implicit map (function). For example, OCL of UML (un)fame does this as well.


By the same token these languages sugar access to maps (data structures).

The reason is that you'd also need to change the type system to support using the Univ type conveniently, without having to explicitly annotate terms that use Univ. Otherwise, you'd end up with the worst of both worlds.

What Frank's claim really says is that any DT program can be trivially translated into a (longer) ST program. That's true, but no-one wants to write programs in that ST language.

I think all you need to support untyped programs comfortably in a typed language is an extension to the syntax along the lines of a quotation mechanism. For example:

typed_plus (Int x) (Int y) = Int (x + y)
typed_plus (Dbl x) (Dbl y) = Dbl (x + y)
typed_plus (Dbl x) (Int y) = Dbl (x + fromInteger y)
typed_plus (Int x) (Dbl y) = Dbl (fromInteger x + y)

untyped_plus = `(\x y -> ,(typed_plus `x `y))
example = `(,untyped_plus 3.1 ,(4 + 5))

Or something like that. (I may have the quotations slightly wrong.) The last two lines would expand to:

untyped_plus = Fun (\x -> Fun (\y -> typed_plus x y))
example = untyped_plus $ Dbl 3.1 $ Int (4 + 5)

Note how you can infer the required Int constructor from the type of the body of the antiquotation ,(4 + 5).

VB and VBA have a "variant" data type, which appears close to Univ: any data type, object or collection of objects can be stored as a variant.

But for a slightly expanded definition of "security," the claim for static typing is somewhat stronger. A sufficiently rich type system—even something as relatively simple as Standard ML's—prevents a larger number of potential security holes by eliminating what we might call "wild casting," the insistence on the part of the programmer that it's OK to treat a value of type A as if it were type B in whatever context. That's a real benefit over both the popular statically-typed languages and the dynamically-typed languages. Consider, e.g. JavaScript, in which "3" + 3 = "33."

But moving on to a rather dramatically expanded definition of "security," in which there's an explicit goal to support "patterns of cooperation without vulnerability," and to support the safe interaction of fine-grained components that have no reason to trust each other or their sources, you do definitely arrive at E, and I hasten to point out that I'm a huge fan of E, have posted about it before, and have even posted about E's auditors before. Since then, I've been interested to learn more about how such fine-grained security can be expressed via type systems, paying particular attention to Flow Caml as described in this interesting thread, and to "An extension of HM(X) with bounded existential and universal data-types" at <http://cristal.inria.fr/~simonet/publis/index.en.html>. From the latter:

""Our main direction for future work is to study the possibility to make security levels also values of the Flow Caml language. This would permit some dynamic tests—whose correctness must be verified statically—on existentially quantified variables when opening data structures. Continuing with our example, this would allow—for instance— computing the total balance of a subset of clients."

This would seem to come close to providing the features of auditors in a statically-typed setting, but I haven't done nearly enough research to actually make that claim. Suffice it to say that it's more than enough to warrant such an investigation, in my opinion.

I would also add that the wide-spread confusion of terms (strongly typed, safe, statically typed) does not help to clarify the meaning of security. Also, while static typing is indeed not necessary for security (for an informal definition I have in my mind), it is much harder to achieve security without safety. The less safe is the language, the less abstractions are guaranteed to be protected by it, the less possibilities are left for building secure programs.

one of the most useful motives for improving programs with type annotations seems to me to be their use in compilation to efficient machine code.

A statically typed program need not have any type annotations at all. See for instance Haskell and SML. It's important to keep in mind that type annotations and static typing are two different things.

Type annotations don't automatically give speed even in dynamically typed languages. The Groovy implementation has been blasted because if you use type annotations it get slower. That may have changed recently, but it was true the last time I checked.

Finally, the performance difference of static type systems is frequently overplayed, IMHO. There have been some amazingly fast dynamically typed language implementations and some stupendously slow statically typed implementations. While dynamic and static typing may have some influence on the upper bound of performance for a given static/dynamic pair of somewhat related languages, there is no hard and fast rule that says "static types = fast, dynamic types = slow."

On the other hand, specialising a program leads to much repetitive implmementation.

Unless of course, your language implementation creates specializations for you. See JHC and MLton.