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 

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]

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.

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 th