Lambda the Ultimate

When you pursue the kind of system described here, you have to use functions to do all your member access ("foo(x)" instead of "x.foo") as in CLOS/Dylan (Dylan actually interprets "x.foo" as "foo(x)"). That allows you to deal with name conflicts on slots/fields using your module system (so two different modules that define a "foo" slot would introduce two different slots and two different accessor functions -- CLOS's handling of slots gets this wrong). Then you can introduce new slots in future versions of a module without changing program behavior.

Of course, once you have to call explicitly imported member-access functions fully qualified by their modules you are doing the equivalent of specifying static types (albeit with a less convenient, more verbose syntax).

...same as in Dylan.

From the CLOS hyperspec: "In general, more than one class among C and its superclasses can define a slot with a given name. In such cases, only one slot with the given name is accessible in an instance of C...". Adding a slot "x" to a class C breaks any application where a subclass of C had already inherited (or declared) a slot "x" (since storage for the two will alias). This rule means that you cannot maintain modularity and extensibility unless your slot "names" are all module-private unique symbols/values, which is not what I see in most sample CLOS code. Even if "real" CLOS apps only use module-private unique names for all slots, this still leads to the verbose member-access dilema I described. Dylan (at least by my reading of the DRM) doesn't have the concept of slot "names" as distinct from their getter/setter multimethods, so it doesn't suffer from the aliasing problem (although it still has the verbosity problem when slot-access multimethods names collide).

This all becomes much easier when you resign yourself to the fact that in an extensible system, a given object could have many "x" members, and static typing is the only sane way to know which of these is meant in any given context.

If you go this route, one day you'll realize you evolved the ultimate hacker language, and it became a godawful mess for writing real programs.

This has been one of the upsides of using even C++ versus Scheme for me: the type system encourages organizing things in a particular way, so that a large codebase is more likely to be coherent (**).
The Bracha slides portray the advantages of type systems as "Performance" and "Safety", but there are other aspects.

(** not that I think C++ is the best way to do this -- just better than nothing. The downside to this is that it is less natural to alter the organizing principle.. no cake & eating it too.)

And having them mandatory is cool to if you work in a team. Also terms like brittle or flexible seem pretty useless to me. A program is correct or it is not. I am getting sick of of those dynamic language designers they avoid designing a good type system because it is to difficult for them and than they try to tell users that it is for there own good.

the paper understates the number of important properties that break in an untyped language. If the developer of a popular library adds a new field (function or variable) named "x" to one of his classes, then he breaks all previously-released applications (both source and binary) that have inherit from it and added their own member named "x".

In a Python example:


class Foo( object ): pass
class Bar( Foo ):
   def x( self ):
     return "x"

b.x() # -> "x"


I don't know which "untyped" language you're talking about, but at least the most popular modern dynamically typed scripting languages -- Perl, Python, Ruby and others -- are mostly properly lexically scoped, so i guess the kind of problem you describe isn't "bound" to happen...

The problematic case (to extend you Python example) is:

1 - programmer A creates an application that uses a useful base class Foo

2 - programmer B extends Foo to create Bar and adds a helper method "x" on Bar that returns a number

3 - programmer A (who doesn't know about Bar) updates class Foo to have a new method "x" that returns a list, provides a default implementation, and then changes his application code to use the new method.

4 - The application breaks the instant an instance of Bar is used in the application code that expects someFoo.x() to return a list, since Bar::x is now a method override rather than a new method.

Programmer A, when he wrote "someFoo.x()", knew that he meant the x method define in Foo (or an *intentional* override). Programmer B, when he writes "someBar.x()", knows he means the x method defined in Bar (and knows that this method isn't supposed to override any superclass method). If we use static types to resolve the member lookup, this program does the right thing. If instead we expect the semantics of member lookup to be indepdendent of static context we make collisions between independent extensions almost inevitable.

Parent and child in an inheritance hierarchy are closely coupled, so why shouldn't changing the parent without updating the child break things down?

If we use static types to resolve the member lookup, this program does the right thing.

How does this work?

But A is generous and permits future generations to override x declaring it as virtual. Now we are in the same situation as before unless a more extensive inheritance semantics like that of C# is introduced that forces B to modify the declaration of x in Bar using the override keyword ( intentional inheritance ) or preserve the status quo using the new keyword. In either case nothing works as usual but a compile time error is thrown unless x in Bar is not declared as new initially.

There is no standardized protocol in Python to deal with unintended inheritance. You can prevent unintended inheritance quite well but than you loose the possiility of Bar to lock x into Foo. To achieve this you have to write:

class Foo(object):
    def x(self):
        print "I'm Foo.x"
        
    def f(self):
        Foo.x(self)  # always bind x to Foo

instead of

class Foo(object):
    def x(self):
        print "I'm Foo.x"
        
    def f(self):
        self.x()  # always bind x to the class of particular instance

This has nothing to do with static typing but everything with Pythons object model.

Kay

An object model like C#'s would allow you to get the right behavior without recompiling Bar (and C# will give you a warning or error about your possibly unitended override when you next compile Bar). C++ will give you a compile error when you next compile Bar, if the function return type isn't covariant with the virtual function it now overrides (it would, though, allow unintended inheritance otherwise).

Your supposed "fix" for function Foo::f in the first case above doesn't have the right semantics (if I understand Python right). It will *always* call the x method declared in Foo and not an override (even if that override is intentional). The problem is that without static typing you can't resolve what was meant.

A less ambiguous case to consider is a class (C) that has two base classes/interfaces (A,B) that each define a member "x" (function/slot/property doesn't really matter). When the expressions "foo.x" is encountered for an instance of this class, a dynamically-typed language can only assign one meaning to this (and so either has to disallow such inheritance or let the slots/functions alias in some way - so your string slot "x" and my integer slot "x" use the same storage and neither of us gets the behavior we want). If we look, instead, at the static type of "foo" we can resolve this; if foo is a C the code is a compile-time error since it is ambiguous, if it is an A then we know that "foo.(A::x)" was meant (and similarly for B).

Basically, if you realize that guaranteeing extensibility in a dynamic OO language requires extensive decoration of member names (to avoid conflicts), then you will see that declared static types can be used as a compact notation for automatically generating the decorated names ("foo.x" -> "foo.(staticTypeOfFoo::x)").

C++'s static typing can't really be considered a "solution" to the problem. First of all, it breaks your code. Your program source code was once legal but is now illegal because of a logically non-conflicting change in a library.

Secondly, it only catches the error when the return types conflict. Though I've heard some structural typing proponents claim that a singature is roughly equivalent to the logical behavior of a type, I don't buy it (no type system I've seen is capable enough).

A real solution is C#'s "new" and "override" declaration specifiers. This is one of my favorite things in Diff(Java,C#). If Python required "new" and "override" annotations, the problems would go away, right? Such declarations don't constitute static typing.

Adding C#'s "new" and "override" keywords to something like Python wouldn't help things at all. The fundamental problem is that the semantics of "foo.x" in Python can only depend on the dynamic type/value of the expression "foo". So how can you specify whether you want the inherited "x" member, or the "x" member added with the "new" keyword?

To specify which you mean you either have to rely on the static type of "foo", or require every member-access expression to be more verbose (by specifying the fully qualified name of the member they mean). If your static type system is absent or optional, the first option isn't possible.

[I feel like we've driven this issue into the ground...]

Adding C#'s "new" and "override" keywords to something like Python wouldn't help things at all. The fundamental problem is that the semantics of "foo.x" in Python can only depend on the dynamic type/value of the expression "foo". So how can you specify whether you want the inherited "x" member, or the "x" member added with the "new" keyword?

Depending on an instance bar is usually not that bad because you can access the class hierarchy from bar. But you still have to locate the "right" x. If you call bar.x and x is defined in bar.__class__ you are done. But what happens if you call bar.f instead, where f is defined in Foo and f calls self.x() in its body? That's actually the tricky part because you have to access the definitional context of f when x is accessed within the body of f by an instance of Bar. This can nevertheless be done with all kinds of metaclass trickery, overriding __getattribute__ and call stack inspection. But I don't believe it's worth the effort and I don't know anyone who has ever tried to build a contract system in Python on such a weird introspective machinery not even as a proof-of-the-concept.

[I feel like we've driven this issue into the ground...]

I concur.

Kay

Whoops, forgot about that part. But isn't this technically a nominal vs. structural issue and not a static vs. dynamic one? It's the structural typing part that causes ambiguity. Of course, structural typing seems like the only viable option for a dynamic OO language...

It may be "logically non-conflicting", but if the language calls your attention to the fact that you have two unrelated methods in your class tree with the same name, I call that a feature.

Let's also observe that in a statically typed language, you can add a method "x" to the base class and as long as it has a different signature, you really didn't cause any trouble at all. You'd have to add the same method with the same signature.

Untyped languages are far more vulnerable to namespace collisions. Different structures (fields vs. methods) are often in different namespaces.

But the main reason that strongly typed languages are the future is that a dynamic language will never be able to reason about the code, and exhibit do what I mean -- the path towards declarative programming.

The drawback of static type systems is that they force you to write programs in the way that they can reason about, instead of being able to reason about how you actually want to program.

Is that a generalized claim that there can be no programmer that reasons about his programs like his typechecker does? Does everybody actually want to program sans static types?

I think the point is that diffrent people wants to program in diffent ways, and having a single monolithic mandatory static typesystem in some sense, forces all those people to program in the same way, even thougth it can't possibly fit everyone. And that it would be better to have an optional modular typesystem, that you could form after your own needs. If you personally wanted a typesystem that was as static as possible for example, or added runtype checks that can't be implented staticlly you could have that, and not have to compromise with those that coudln't stand that kind of confinment, or insisted that all types must be inferrable. or vice versa. A bit like how a multiparadigmatic language allows you to chose how to implement a algorithm, recursive, categorics, gotos or what you want; but applied to safety instead.

This isn't all good though. For your self you might want perfect freedom, but you probably wouldn't trust your coworkers (or fellow humans, in general) with it. So you could reason that you actually want a system that binds you to a particullar programing style, that removes as much of your free will as possible, so that you just becomes a replacable cog in a machine that produces code. Or well at least your employer might want that.

...is not a type system at all. A good optional type system, just like a good static type system, will influence the way one constructs code. If plugin type system is ignored, then you mind as well not use it at all, since it's probably not going to tell you anything meaningful. The case for the optional type system is not that types don't effect the construction of the code. Rather that there are certain extenuating circumstances where a mandatory type system can prevent you from writing concise valid code.

Designing a pluggable type system that can give meaningful results to dynamic code is a very hard chore - one that I would think near impossible. The only way for a type system to work (optional or static) is to have code that resembles statically typed code - i.e. code that was influenced by a type checker. The advantage of optional types is that you have the option to ignore or suppress the statically reported type errors.

Optional typing sounds more appealing to dynamic language advocates only because it borrows some of their arguments about the corner cases where a type system fetters expressiveness. However, the optional type system will actually require a more radical change from the dynamic PL programmer than it will the static PL programmer.

I think that a language must be designed to have an optional type system. For example it should probably suport algebraic datatypes, and simillar features.

If you have a polite system that only reports errors that are sure to show up anyway, and you ignore that, then your just stupid. (Unless the error message is realy unclear.)

I also think that our type systems is developing the sort of organic complexity, there you just have to let go and not try to understand exactly how it works. Sort of how most programers don't know exactly how the compiler optimizes the code, but just trusts that it does a good jobb. Thats sort of the point of automation/abstraction. That you delegate some of the thinking to an automated system. If you have to understand that system in detail, and think about it all the time, its not much of delegation, is it?

What I meant is this...

Any type system disallows some correct programs that cannot be proven correct by the type system.

Current type systems (even very sophisticated ones) bend the language to fit the kind of proofs that can be performed by the type system. Haskell doesn't allow inclusion polymorphism. O'Caml doesn't allow adhoc polymorphism. And don't get me started on Java!

The problem with type theory is that they force the programmer to jump through hoops to meet the needs of the type theorist, rather than the type theorist jumping through hoops to meet the needs of the programmer.

nat: The problem with type theory is that they force the programmer to jump through hoops to meet the needs of the type theorist, rather than the type theorist jumping through hoops to meet the needs of the programmer.

"The fundamental problem addressed by a type theory is to insure [sic] that programs have meaning. The fundamental problem caused by a type theory is that meaningful programs may not have meanings ascribed to them. The quest for richer type systems results from this tension." — Mark Manasse

http://www.cs.indiana.edu/metastuff/looking/ch6.html.gz

The only way a computer program acquires meaning is by running on a computer.

So, until you run it, there are no bugs, right? Pseudocode examples (as in algorithms textbooks) are totally meaningless. So are comments. Unreachable code has no meaning: it's possible for the "if/then" branch to have meaning while the "else" branch has none...

Piffle.

...and of course, there can never be bugs in implementations, because implementations provide the only definition of meaning, and hence are vacuously correct. Cool!

Type systems let us reason about the meaning of the program by representing it symbolically, but they aren't the meaning itself.

If the system has undesired behaviour that is not detected by the type system, then the type system is obviously not the meaning of the program. The program text has a meaning that is not represented by the types and can only be observed by running the program.

The problem with type theory is that they force the programmer to jump through hoops to meet the needs of the type theorist, rather than the type theorist jumping through hoops to meet the needs of the programmer.

Type theorists jump through hoops to meet the needs of programmers quite often - ad-hoc overloading is the perfect example: in principle, it's totally useless, but it's just so damned convenient.

Unfortunately, the number of hoops a type system has digested does not monotonically increase the joy of working with it - see C++ for example.

An 'untyped' language is more vulnerable to namespace collisions because a type and a namespace are really the same thing, it's just a matter of degree. Languages that lack types have no way of resolving the ambiguity of symbols shared between objects.

I dont think anyone is arguing that types shouldn't be checked at all. And with that in mind, a dynamic type system could just do any checks runtime that a static system would do at compile time. The only diffrence is when you do the checking. I cant see how that would lead to ambiguity.

Or how does your "dynamic type system" check that some arbitrary function has type int->int?

By checking that its input is int every time its applied, and that its output is int every time it returns.

It means that the type-error is raised not at the moment a wrongly-typed function is passed as a parameter, but when it is used?
I cannot put my finger on it, but I feel uneasy about that fact...

I cannot put my finger on it, but I feel uneasy about that fact...

Don't worry, those are just the standard withdrawal symptoms of the typoholic. Deductive proofs can be dangerously addicting! While you're in rehab, you can use methodone, I mean contracts, to take the edge off.

That was one of the funniest things I've read all day! Thanks Anton!

That is not the same thing. You cannot check the type of a functional value, itself, dynamically. Nor can you check the type of a lazy value, or a future, or even a mutable reference.

Nor can you check the type of a lazy value, or a future, or even a mutable reference.

Or a continuation, for that matter.

Sure you can. you can give the function a contract that asserts that the function has type "int->int", and then you can just check the contract. And the contract then throws an exception if the function would take or return a int.

But no, its not the same thing. The dynamic system discovers the error later, then more information is known, so there is less risk that it frows an exception, and even if it does, it might be cathed or handled, so you have a chans of recovery.

The dynamic system discovers the error later, then more information is known, so there is less risk that it frows an exception, and even if it does, it might be cathed or handled, so you have a chans of recovery.

But those are the exceptions I want to have! Because then there is less risk that I blindly execute parts of the code (and possible side effects!) of some function under the false assumption (or hope) that it has the type I expected. I don't see at all how taking this risk could possibly simplify error recovery.

Also, why do you assume that the late runtime check has "more information"? More information than what? It surely does not have the contextual information a static type system can derive.

Just as it isn't an advantage that a car is expensive.

Generally a static type system doesn't throw exceptions on type errors at all, but just refuse to compile at all. So you wouldn't get any exceptions anyway, so there is no way to recover, as well, you don't even get a chance. You could view it as a question of trust vs assurance, you eighter trust your static system to guarantee that your program doesn't have any errors, or you make assurances so that even if you get a error it doesn't stop your program from running.

But no, I didn't actually think it is an advantage to discover errors late. (It could be argued though that it lets you do better debugging by allowing you to do a trace of the program up to the error point.)

But I think that losening the constraint on then to do checks, allows you to do things that isn't reasonable to do earlier. Static type systems isn't realy exact. If you apply them to a dynamic language, you will get situations there it can't be sure if an error will occor or not, there the type system is undecidable. Like hetrogenous lists for example. The method of static languages here is to not allow any such code. And this limmits not only how you can write your program (you lose the expressitivity of hetrogenous lists), but also what safety checks you can make. Checks that have a large portion of undecidable cases would be realy demanding as it would severly restrict your language. Perhaps even below turing completness. You need a dynamic or polite system to allow this, without completly crippling yourself.

'Also, why do you assume that the late runtime check has "more information"?'

I assume that there is some kind of computation going on at runtime, and that this produces some new information. As that is the purpose of runnig a program isn't it? I every computation was done at compile time there wouldn't be so much a program as just some kind of data. And also you can assume that you have more information about the inputs, after some user actually have enterd them.

Generally a static type system doesn't throw exceptions on type errors at all, but just refuse to compile at all. So you wouldn't get any exceptions anyway, so there is no way to recover, as well, you don't even get a chance.

Whaaaaat? By this reasoning, no compiler should ever refuse to compile code. All errors should be left until runtime.

Look--in static-typed languages, the compiler obviously should make the user fix type errors. Programs written in static-typed languages are written in a static-typed mindset; any type errors are programmer mistakes. It's quick, and a good use of time, to fix them.

The sort of argument you ought to make is that the static-typed mindset is not powerful enough, or that static-typed code is hard to read or extremely time-consuming to write. Because once you're in the static-typed mindset, the extra type-checking is in fact extremely useful. I don't see how anyone who has done static-typed programming could think otherwise.

Generally, detecting errors early is a highly valuable feature for any tool. This should be self-evident. Fixing errors later is orders of magnitude more expensive. For non-toy PLs, early error detection is one of the most important problems, period.

I assume that there is some kind of computation going on at runtime, and that this produces some new information. As that is the purpose of runnig a program isn't it?

Information != relevant information.

Type-checking mostly catches simple, stupid programmer mistakes. There is no extra information available at runtime that could possibly be useful for debugging.

Because once you're in the static-typed mindset, the extra type-checking is in fact extremely useful. I don't see how anyone who has done static-typed programming could think otherwise.

Once you're in the static-typed mindset, you think that the extra type-checking is in fact extremely useful. However, if you've done static-typed programming and actually thought about which parts of that apparent extreme usefulness are important, and which parts aren't, then it's quite possible to "think otherwise".

Here are couple of things that I came up within a couple of minutes and have found to be valuable (roughly) in the below order:

• Availability of formal, automatically verified, documentation in the form of types. (Which greatly improves the ability to understand code written by others.)
• Immediate catching of most silly mistakes. (Even silly mistakes can be costly and careful use of a type system can help to catch many. many kinds of silly mistakes.)
• Ability to enforce abstraction and greatly enhanced ability to reason about programs. (Often this boils down to being able to prove that something is impossible. Proving negatives is hard!)
• Compiler optimizations. (Like it or not, performance does matter in some cases, and implementations of typed languages tend to be faster.)

In an ideal world you wouldn't probably need (m)any of the above, but the world is rerely ideal. Documentation (comments) either doesn't get written at all or isn't up-to-date. Testing is done interactively or hardly at all. Hardware spec may be fixed or the language implementation may be just slow.

My original response was primarily to the absolutism of "I don't see how anyone could think otherwise". That's very much a question of mindset, which essentially comes from first accepting the presence of static type-checking as a requirement, an axiom. That acceptance forces one to think from "within" the statically-checked system, but two different systems can't validly be compared from within one of them.

To respond to your specific points, do you consider "sound" and "statically checked" to be equivalent, w.r.t. type systems, as your bullets mostly imply? That seems questionable to me.

Ritualistically, I'll give typical latently-typed responses to your first three bullets, in order: (1) latent types & contracts; (2) assertions/contracts & test suites; (3) same as #1 & 2, with less emphasis on deductive proof.

The "requirement" for deductive proof is often not, in fact, a requirement, except if your mindset imposes it as such. The inductive "proofs" given by testing and successful operation of systems are, in practice, usually good enough.

You suggest that testing is lacking in practice, but that seems to ignore a major industry shift towards automated testing in the past 5-10 years or so. Latently-typed programs are perhaps more likely to have good test suites, to be able to catch errors early (addressing jorend's point). This may work to their benefit, as opposed to relying on an essentially trivial static type check (trivial by comparison to the program's entire meaning) as an incomplete proof of program correctness.

Static checking of ordinary types deductively proves the things that are easiest to deductively prove, and ignores everything else. (I say "ordinary types" because static checks of other kinds of properties, e.g. related to concurrency and security, are potentially more interesting.)

The response to the bullet about performance is more complex, but just practically speaking, I'll offer Erlang as an existence proof that performance-sensitive systems don't necessarily require static type checking, not to mention all the server systems implemented in languages like Python, PHP, and Perl. My experience with such systems is that their performance bottlenecks are not usually language-related.

To respond to your specific points, do you consider "sound" and "statically checked" to be equivalent, w.r.t. type systems, as your bullets mostly imply? That seems questionable to me.

No. I consider "type system" (as a set of rules for assigning types to all valid expressions) and "statically typed" to be equivalent, but this isn't a point I want to make here.

There are two reasons why I said "sound". First, if a type system isn't sound (meaning: it doesn't actually guarantee anything), then the other points are mostly meaningless (e.g. abstraction boundaries can be broken using reflection in Java). Second, this conveniently rules out the mainstream languages, whose type systems I would rather not spend time with.

The inductive "proofs" given by testing and successful operation of systems are, in practice, usually good enough.

The coverage that (ad hoc / "a little here and a little there") testing and succesful operation yield is not enough. I've fixed many bugs, in code written (by me or someone else) in both languages with an unsound type system and in languages with dynamic checking, that would have been caught by sound type systems. But, this should be old news.

You suggest that testing is lacking in practice, but that seems to ignore a major industry shift towards automated testing in the past 5-10 years or so.

I would bet that the ratio of code covered by unit tests to code not covered by any form of automated tests is rather depressing. I'm definitely not against testing. One should have both automated testing and a sound type system.

Latently-typed programs are perhaps more likely to have good test suites [...]

I wouldn't make that bet.

This may work to their benefit, as opposed to relying on an essentially trivial static type check

I wouldn't say that guarantees provided by a sound type system are necessarily trivial. However, it seems to me that I don't share your implied premise; I do not expect that a type system magically proves properties that it does not prove.

(trivial by comparison to the program's entire meaning)

What is the meaning of a program that has unspecified behavior? Call me a heretic, but I consider unspecified return values and unspecified evaluation order (for a strict language - particularly one with first-class continuations) to be totally unnecessary complications (for the language user) at best and fundamental design failures at worst.

as an incomplete proof of program correctness.

Essentially, a sound type system guarantees that a program has a well defined meaning. Nothing more and nothing less.

I'll offer Erlang as an existence proof that performance-sensitive systems don't necessarily require static type checking, not to mention all the server systems implemented in languages like Python, PHP, and Perl. My experience with such systems is that their performance bottlenecks are not usually language-related.

Not all applications are servers where OS level IO (usually implemented in C or some other low level language) is the bottleneck. Imagine, for a moment, that the OS would have been implemented in pure Python, PHP, Perl, or any other "dynamic" language. What kind of performance would you expect from such a system?

No. I consider "type system" (as a set of rules for assigning types to all valid expressions) and "statically typed" to be equivalent, but this isn't a point I want to make here.

I accept that equivalence, with the caveat that the rules can usefully be applied selectively, e.g. to functions but not to all their terms. You could take such a skeleton from a dynamically-checked program, with appropriate stubbing, and compile it in a statically-checked language, and prove the validity of that program's (partial) type scheme. Typically, of course, such proofs aren't performed, since a reasonable assurance of correctness is obtained in other ways.

There are two reasons why I said "sound". First, if a type system isn't sound (meaning: it doesn't actually guarantee anything), then the other points are mostly meaningless (e.g. abstraction boundaries can be broken using reflection in Java). Second, this conveniently rules out the mainstream languages, whose type systems I would rather not spend time with.

That's fine with me, possibly depending on what you mean by "guarantee". If you don't statically check types, and/or if a program includes code that hasn't been statically typed, you lose the proof of type scheme correctness, even though you may have strong evidence of its correctness. A certain kind of guarantee is lost, but that doesn't make the other points meaningless.

I would bet that the ratio of code covered by unit tests to code not covered by any form of automated tests is rather depressing.

I'm talking about comparing statically-checked programs to dynamically-checked programs that follow good testing and other practices. In a professional context, where the quality of the development process is considered, the need for testing and the positive effect it has on the development process is understood, and normal procedures suffice to help catch errors early, even in dynamically-checked programs. It's not important to me how many people aren't operating in that kind of context.

What is the meaning of a program that has unspecified behavior? Call me a heretic, but I consider unspecified return values and unspecified evaluation order (for a strict language - particularly one with first-class continuations) to be totally unnecessary complications (for the language user) at best and fundamental design failures at worst.

This seems tangential, but in any case, you seem to be referring to Scheme and the fact that RnRS does not constrain implementations in certain ways. However, all the implementations I use have a specified evaluation order and specified return values. So your objection seems to be mainly about portability, or perhaps about the merits of different kinds of language specifications, neither of which is relevant here.

As for the meaning of a program that has unspecified behavior:

Essentially, a sound type system guarantees that a program has a well defined meaning. Nothing more and nothing less.

And well-typed programs don't go "wrong". But what is the overall meaning (in a less formal sense) of a program that has a well-defined meaning in a formal semantic sense, but is full of bugs relative to its specification? Type systems deal with a particular subset of program semantics, and whether that subset is proved correct formally, or whether correctness is determined in other ways, doesn't always matter all that much.

Not all applications are servers where OS level IO (usually implemented in C or some other low level language) is the bottleneck. Imagine, for a moment, that the OS would have been implemented in pure Python, PHP, Perl, or any other "dynamic" language. What kind of performance would you expect from such a system?

The Lisp Machine OS seemed to perform pretty well for the time. (Perhaps it had partial static checking, but that's fine with me.) I wouldn't write an OS in any of the "P" languages, but that has more to do with their choice of semantics in general, rather than their type systems specifically. But I agree, this is all about "not all applications". Not all applications need a deductive proof of the correctness of their type schemes.

This seems tangential, but in any case, you seem to be referring to Scheme and the fact that RnRS does not constrain implementations in certain ways. However, all the implementations I use have a specified evaluation order and specified return values.

I'm partly referring to Scheme, but not exclusively. There are many languages out there that share a tradition of leaving many things unspecified or undefined (including C and, to some degree, even OCaml). This tends to make the type system less useful. In C, for instance, one really can't assume much anything about a program that type checks.

So your objection seems to be mainly about portability, or perhaps about the merits of different kinds of language specifications, neither of which is relevant here.

Why do you think that these aspects are irrelevant? I thought that LtU, and this topic (type systems), was all about various aspects of programming languages including their design and specification. The way in which a language is designed and consequently specified can have a tremendous effect on how easy or difficult it is, among other relevant things, to port programs from one compiler to another. I find that an important aspect to consider when analyzing a language specification.

Sorry, I don't have the time right now to reply to other points. I may do so later. However, it seems that this discussion is steering towards issues that I consider less relevant (I'm not blaming you for that). Consider my list of useful consequences of a sound type system and that they are written rougly in an order of importance. The point I'd like to discuss is whether a sound type system makes programs easier to understand and modify. Together, the first three bullets are at least an order of magnitude more important than the fourth bullet. The nice thing is that in a (statically) typed language one can not avoid having the benefits. In "latently typed" languages the programmer can easily skip writing the assertions and test suites or may skip running the test suite. In either kind of language, comments in code can (and quite often do) lie. In contrast, in a language with a sound type system, the types do never lie and will always be there. (And again, I still want the assertions (contracts) and unit tests when the properties aren't guaranteed by the types.)

On the question of relevance, I mean that things like portability and whether a language specification defines e.g. a single, fully specified language or (potentially) a family of languages isn't very relevant to the question of static type checking vs. other ways of validating a program's type scheme, which (to me) is what we're really discussing in this thread. Of course, those things are relevant on LtU in general, though.

I agree that "types make a program easier to understand and modify", but you can achieve that using latently typed languages.

Saying "The nice thing is that in a (statically) typed language one can not avoid having the benefits" is certainly subjective, and seems to imply that you're trying to impose something on someone else - after all, if you want the benefits, don't skip the assertions and tests. If you want that as a process in a company, make it the process.

(And again, I still want the assertions (contracts) and unit tests when the properties aren't guaranteed by the types.)

But "the programmer could easily skip writing" those, so you're not really in that much better a position with a statically checked language (which still seems to be a synonym for a language with a sound type system, in your view). If you don't skip writing those things, then you don't need the static type checking nearly as much. The better your development process, the less important static typechecking is. :)

I agree that "types make a program easier to understand and modify", but you can achieve that using latently typed languages.

By "achieve", do you mean that you can emulate type systems in a "latently typed" language. It is certainly possible, but, again, you assume an ideal world. My real world experience suggests that it just doesn't happen in practice at a large scale. (Indeed, I've experimented with such techniques, but my real world experience suggests that you just can't expect to see it at every programming shop.)

Look, I'm not talking about the latest, state-of-the-art, buzzword compliant, all theoretical possibilities exhausted, software engineering practice in a "latently typed" language vs in a (statically typed) language with a sound type system. I'm talking about everyday programming practice that you can expect to see at any programming shop using either a "latently typed" language or a (statically typed) language that has a sound type system.

Saying "The nice thing is that in a (statically) typed language one can not avoid having the benefits" is certainly subjective, and seems to imply that you're trying to impose something on someone else - after all, if you want the benefits, don't skip the assertions and tests. If you want that as a process in a company, make it the process.

It is more about people agreeing to use a type system to communicate important information than forcing others to use a type system. In other words, when you use a language with a sound type system, you are effectively making an investment in the form of writing a little bit of extra specifications, so that everyone, including you, will be able to understand and modify the code more easily. It is possible to do the same in a "latently typed" language, but it requires a degree or knowledge, maturity and discipline that unfortunately doesn't exist at a large scale and can easily be (and often is) forgotten.

A good type system with abstract types can be used to verify non-trivial properties (e.g. that, say, HTML output is well formed), but that is already beyond of what I think can be expected or what happens by default, and, is, IMO, less relevant.

I do not believe in the idealistic view that processes guarantee quality. Such a belief relies on an ideal world where, among other things, the process, when followed, guarantees quality and that people actually follow the process.

Also, while processes may be considered relevant topics at some places, my impression has been that processes are somewhat of a non-relevant topic at LtU. Let me put it this way, you shouldn't rely on a process to fix a broken language.

If you're talking about "everyday programming practice that you can expect to see at any programming shop", then we're also talking about some variation of Java etc. vs. Python etc. which you earlier indicated that you weren't interested in. What's more interesting is how the languages, processes, and the tools that support processes, wlll change in future.

It is more about people agreeing to use a type system to communicate important information than forcing others to use a type system. In other words, when you use a language with a sound type system, you are effectively making an investment in the form of writing a little bit of extra specifications, so that everyone, including you, will be able to understand and modify the code more easily.

I agree with this. However, you (and many others) are making a questionable leap from this, with the assumption that having written such specifications, that they should be checked statically, and that in order to do so, every other term in the program should also be typed and checked statically, and that if the static checks fail anywhere, the program shouldn't be allowed to run at all. In many respects, that's a very strange leap to make! It's the type theory tail wagging the program semantics dog.

Since the question in the top message in this thread is Optional Type systems, I'm still left wondering if it's a compromise that will be accepted by either side. The latent type proponents seem to be saying that adding a meta type layer above the code just fetters the process and doesn't buy you much. The static typing proponents seem to be saying that any introduction of unsoundness in this meta type layer opens up a hole too large to hold back the deluge.

Disregarding the question of which is better: Do optional typing systems represent a viable compromise to get the advantages of both static and latent typing? Looking at the Smalltalk community, I'd say that Strongtalk never really gained widespread adoption. At least from that experience, it doesn't seem that the dynamic language crowd is particularly enticed by introducing optional type systems.

For me, the compromise is easy to specify: systems that allow types to be declared and used, and to whatever extent possible, checked, without requiring every term in a program to have either a declared or inferred type.

What I am arguing against is the notion that because types are useful (which I don't dispute), it is therefore necessary or important to require a successful static check of the type of every term in a program, before it is possible to run that program.

I would argue that in a substantial majority of cases that do use statically-checked languages, such checks are neither necessary nor important, except in the sense of being a necessary evil in order to get the type scheme mechanically checked by the rather simple-minded checking tools we have today.

[Edit: added the below to (slightly) better address Chris's points.]

The optional type systems I've seen don't really come close to doing what I'm thinking of. (Using contracts/assertions does a much better job.) I don't think that has much to do with technical possibilities, but much more to do with the unwillingness to "open up a hole too large to hold back the deluge", i.e. the tendency in optional systems is still to try to type everything. It's a sort of disease, as Erik suggests, typoholism.

Users of dynamically-checked languages already know what post-deluge life is like. Types are useful for communication and other reasons, though, and some of us put them in comments for those reasons. Just about anything would improve on that, but going from types in comments to full every-term-must-be-typed is like closing the borders of a country that's afraid of terrorism. It just makes life difficult without solving the real problem.

For me, the compromise is easy to specify: systems that allow types to be declared and used, and to whatever extent possible, checked, without requiring every term in a program to have either a declared or inferred type.

Main problem is that this simply won't work out in practice. Every small "hole" somewhere in the type checker's local knowledge quickly cascades to gigantic abysses downstream. In the end, it typically can detect almost nothing. For example, the Oz compiler has a relatively involved static analysis phase, but in practice it rarely finds interesting errors (besides trivial arity mismatches in direct procedure calls).

Useful type checking relies on strong invariants, and arbitrarily leaving holes is in severe conflict with that.

As long as dynamoholics only long for such weak systems, the preconception that type systems only detect trivial errors will be sort of a self-fulfilling prophecy... ;-)

You're assuming that the goal is to statically check things. I'm saying that's the wrong goal, in many cases. The goals were quite well laid out in Vesa's bullet points, if you remove the bias towards static checks. I'm saying you don't need static checking to achieve those goals. Dynamic checks can be quite sufficient. Anything you can do statically is a bonus, as long as it doesn't require restructuring the program to support it.

BTW, my claim about detection of trivial errors applies to fully statically-checked systems. They're trivial relative to the overall semantics of the program.

Anything you can do statically is a bonus, as long as it doesn't require restructuring the program to support it.

They're trivial relative to the overall semantics of the program.

From a theoretical perspective, I'm not sure that you can statically prove much from code that has not been somehow written with static type checking in mind (be it mandatory or optional).

I agree, useful optional typing is highly likely to involve (optional) annotations related to types.

Since Scheme already has a compromise, I was wondering how the Scheme community feels about Soft Typing? (Whether it's in widespread use or just a curiosity piece to prove that Scheme is the ultimate swiss-army knife PL?)

Soft typing is more of a research topic, and it doesn't really prove anything about Scheme (except perhaps how difficult it is to statically check). There are soft typecheckers for Erlang, too, for example. However, soft typechecking appears to be tackling a different problem than the one I'm most interested in — it usually attempts to infer a static type scheme for the entire program, i.e. all terms. This results in the type checker worrying about, and trying to propagate, the types of expressions like (if (test) 42 #f), which leads to incredibly complex inferred types for expressions which the programmer "knows" have quite simple types. Automatic static typecheckers aren't all that smart, whether they're soft or hard. One way to get some of the more important benefit of types without the baggage is to not worry so much about static checking.

Beyond the question of what constitutes trivial vs. non-trivial, I should point out that trivial errors that are not detected can be just as costly.

Agreed. That's why I'm emphasizing assertions, contracts, and tests, all of which are pretty good at catching trivial errors, and helping to validate a program's type scheme, if the program is written in a type-aware way. That's where optional annotations would come in, too.

To my knowledge all optional typesystems so far have been designed as an add on to a language thats already designed to have static typing. I think thats bad. There should be synergies between the language and the type system, at least on some level. I think an optional typesystem would only really work in a language designed to have just an optional typesystem, and not dynamic nor static as default.

To my knowledge all optional typesystems so far have been designed as an add on to a language thats already designed to have static typing.

Just one example of a more or less "optional" type system for a "latently typed" language: A Practical Soft Type System for Scheme.

Maybe a more basic question which I still don't understand, say a language has mandatory static types which is sound wrt to some dynamic semantics which doesn't depend upon it, and an additional optional type system.

If I write a program which is statically well typed, but optionally illtyped, is it a meaningful program? Is the intension that a) optional typing prevents execution, or b) program halts when the optional type system witnesses a violation?

The paper says: [an optional type system] "is one that has no effect on the run-time semantics of the programming language", so isn't Gilad talking exclusively about static type systems? E.g. if a dynamic checks inserted by an optional type system fails, then the dynamic execution is changed.

If I write a statically illtyped program which passes the addition optional type system can this be considered a meaningful program?

Yes, the paper talks about an optional static type system added to a dynamic system in a way so that the static system only reports an error if there is 100% chance that that error would occure if the program was run. But it's not that kind of optional typing that neither me nor Anton van Straaten (I think) are talking about.

But "the programmer could easily skip writing" those, so you're not really in that much better a position with a statically checked language

The type checking would still be there to provide up-to-date and automatically verified information (types).

a statically checked language (which still seems to be a synonym for a language with a sound type system, in your view)

A sound type system implies static checking, but static checking does not imply soundness.

If you don't skip writing those things, then you don't need the static type checking nearly as much. The better your development process, the less important static typechecking is. :)

Actually, I would expect the converse (converse in some sense) to be true. I think that this isn't a question of need, but rather a question of being able to take advantage of a type system. Frankly, arguments based on need are seriously lame. You don't need "latent typing" or a type system to create software. Heck, you don't even need a high-level language to create software.

I would expect that a typical programming shop using a language with a sound type system would take advantage of only a rather small subset (but still an important subset) of the potential of the type system. I would expect that better programming shops would routinely use type systems (and possibly other techniques) to automatically verify many non-trivial properties of the systems they are building.

This is in response to the "ritualistic" responses.

One important difference between (static) typing and "latent typing" is that a type safe interface is a solution once and for all.

Consider the previously mentioned example of providing a module for creating HTML output in a type safe manner. The types of the HTML generating combinators are expressed just once in the signature of the module. The type checker then takes automatically care of enforcing the correctness of clients. Clients of such a type safe interface need not worry about testing the aspects that the type safe interface already guarantees. (Clients may concentrate on testing other aspects.) A type safe interface is essentially a O(1) complexity solution.

Run-time checked contracts can not provide similar benefits. Even though the contracts may be checked in only one place, you will need tests to explicitly exercise every code path to evaluate the contracts with particular arguments (which still doesn't guarantee the absense of type errors). Unless every client comes with a thorough test suite, it may, and does, happen that some specific code paths aren't exercised until much later. A dynamically checked interface is essentially a O(n) complexity solution where n is the number of clients of the interface.

Sometimes bugs in relatively rarely executed code paths are found years after their introduction. I just fixed such a bug (dating back back at least 2 years and 10 months according CVS logs) a couple of days ago.

Once you're in the static-typed mindset, you think that the extra type-checking is in fact extremely useful. However, if you've done static-typed programming and actually thought about which parts of that apparent extreme usefulness are important, and which parts aren't, then it's quite possible to "think otherwise".

I've stated which part I think is extremely useful. Catching errors early.

I should think this is useful regardless of your mindset.

You assume that you only want to make checks on trivial properties. I don't.

Fixing errors later is orders of magnitude more expensive.

Exactly. The cost of having a maintenance programmer fix a bug is often a minor part of the equation. Before a bug is assigned to be fixed by a maintenance programmer, it has often gone through various "layers" of a organization such as technical support (contacted by the customer in the first place), testing (to verify the bug and file the actual bug report), and product management (to decide whether to fix or not). After the bug has been fixed, it needs to go back through most of the layers.

Note: I'm merely pointing out how things work in many organizations.

"Later" doesn't necessarily mean "after deployment". In this context, it could, and ideally should, merely mean during routine test suite runs.

There's no way to be 100% sure your code is free of type errors by testing. That's a silly notion.

You would have to make sure every code path executes with every combination of (significantly different) types that can reach it. Writing a test suite like that would require... well, static type information. Hmm.

Let's aim a little lower--just coverage of every code path. Is that common? I'm far from sure such a test suite exists for any project in a runtime-typed language. How mature are Python's code coverage tools? How about Scheme? What does this say about how often they're used?

Even if you did have 100% test coverage, it's possible with runtime typing for one stupid mistake to mask another, which makes finding and fixing all the bugs time-consuming. This happens to me in practice, even without test coverage.

Whenever I write a Python program that takes more than 30 seconds to run, I start to notice how often I mistype identifiers, or fail to change a call site when I change the signature of a function. (I notice because then I have to wait another 30 seconds to see my next stupid mistake.) It is extremely common, no matter how careful I am.

Now--I think I'm making up the time somewhere else. After all, I did choose Python, not C#. But for you to say that static typing isn't useful contradicts every shred of experience I've gathered.

There's no way to be 100% sure your code is free of type errors by testing. That's a silly notion.

And where does the requirement that you be 100% sure come from? Aside from e.g. life-endangering applications in e.g. aerospace and medicine, the business case for being 100% sure that your code is free of type errors is unclear. Does that mean it has fewer bugs? Can you prove that, i.e. what's the correlation between static typechecking and bugs in a delivered program? Or are you just taking it on faith that static checks are a benefit here, because they give you 100% certainty about something, regardless of its relevance?

But for you to say that static typing isn't useful contradicts every shred of experience I've gathered.

I didn't say it isn't useful. You claimed that "the extra type-checking [required by statically-checked languages] is in fact extremely useful", and said that you didn't "see how anyone who has done static-typed programming could think otherwise." I'm pointing out that this is a subjective call (drop "extremely" and we'll talk), and that it is possible — in fact, quite reasonable — to have done statically-typed programming and think otherwise.

Regarding your other arguments, you're talking about some issues that go beyond typechecking. For example, in Scheme and other dynamically checked languages (even Visual BASIC!), it's common for mistyped and undefined identifiers to be flagged at compile time. In Scheme in particular, a lot of checking happens statically, partly because of macros, and particularly if you're using a good module system. So in part, we have a situation here which is analogous to the one in which people use Java, dislike its type system, and blame static type systems in general, as opposed to the one in Java. Don't extrapolate from Python to all dynamically-checked languages.

When you're focusing on typechecking in particular, the testing situation is not as bad as you make out, in practice. The same properties that allow automated systems to statically infer and check types ensure that type errors in dynamically-checked systems aren't likely to remain hidden for long, except on entirely unused code paths. This explains the effect that's been observed for Erlang, that running typecheckers on working programs doesn't turn up many type errors.

.. and since type systems have reached 100% coverage of type errors there is surely no need for further work on them. :-)

One advantage of discovering errors later is that you can often run a program successfully before a roughly equivalent typed program would even be compilable by a static-checking compiler.

This can be quite useful when developing in an interactive code & test style: you may want to test some working code paths, while the program still has other code paths which are incomplete. Those incomplete paths are likely to generate type errors and other errors, but you may not be interested in testing them yet.

From reading the book and watching the videos, it's rather obvious that their style of programming is to give names to functions as they are going along... and then to later on worry about implementation details.

Of course, a static programmer can do the same sort of design - either by just waiting to run it once everything is written - or to create function stubs on the way. Still, I'd think the tendency is that dynamic programmers start running early and often, and static programmers tend to get more written before the first trial runs. But that's just a tendency, one which really requires discipline either way.

Of all the discussions on static vs. dynamic typing, your and Anton's exchange comes closest to where I find myself, which is to have decided, as I've written before, that the real question is how interactively one can program. Personally, I sit in an interactive environment, trying out snippets of code on the fly, and it matters not in the slightest whether that interactive environment is a Scheme one, a Common Lisp one, an O'Caml one, a Java one^*... and I don't find myself having to struggle to get any of them to do what I mean.

^* Yes, you can do Java interactively, too, with some effort. Here, I'm referring to the "Scrapbook" in the Eclipse IDE.

...was programming 6809ASM for embedded instrumentation systems. In that environment, it took a full four hours between every compile and test cycle. Gave one an appreciation for getting as much out of the way in the coding and compile cycle prior to attempting a run.

My personal take is that these things have to be balanced. Sometimes the churn of an interactive environment can boost productivity off the charts. At other times, it just gets in the way of a more methodical reasoning process - getting hooked into instant gratification. This balance is not a function of the language type, but rather certain PL practitioners have a proclivity one way or the other.

In ML (both SML and OCaml) one can use signatures and functors to compile (and consequently type check) code without having to fill in the implementation details. All you need to do is to invent names and types (you can even use value specifications such as val foo: 'a to avoid having to invent the actual type) for the operations that you would like to have.

Alternatively, and in conjunction with functors, one can use functions that raise exceptions (either always or just in the unimplemented cases). Such functions can be given arbitrary types (either explicitly using type constraints or automatically through type inference). You can then compile your program as well as run parts of it (the parts that don't raise exceptions).

The point is that the effort required to get useful feedback from the type checker (or even to run parts of the program) is probably much less than one might believe.

Sometimes I just use undefined or error "NIY" to stub expressions and functions in Haskell. Doesn't it provide the same flexibility?

Sure, you can stub stuff out. IME, stubbing things out requires more work in a statically typed language, particularly in early exploratory programming. This is partly because type errors tend to propagate, so you have to make sure you put the right stubs in the right place, which is unnecessary work for a code path that you don't yet care about. I think of this as being like burnt offerings — otherwise unnecessary things which you have to do just to appease the compiler.

I think the earlier comment about "mindset" really captures a big part of the issue. When I'm starting a program in say, OCaml, I often find myself concentrating quite a bit on getting the types I want, before I get to the real functionality, along the kind of lines Vesa described. This seems natural in that context. When I program in Scheme, I'm hardly ever focusing on the types so much at first. In fact it can be almost the opposite - functionality first, type discipline later. And as Chris points out elsewhere, there are times when one approach seems more appropriate than the other.

That is not the same thing. You cannot check the type of a functional value, itself, dynamically. Nor can you check the type of a lazy value, or a future, or even a mutable reference.

Sure you can.

You can give a nonstandard semantics to a subset of Scheme (i.e., typable ML terms) that allows you to reify an expression as its type, even functions, promises, futures, and mutable cells. Even continuations (call/cc is just a primitive, and can be given a nonstandard interpretation as well, witness the implementation of dynamic-wind in Scheme).

But you weren't talking about implementing your own interpreter, I guess.

Maybe surprisingly, you can perform a source-to-source translation (and provide nonstandard definitions of the primitives) that allows you to reify your subset of Scheme expressions as their types.

And if you think a source-to-source transformation and nonstandard implementations of the primitives you need is too high a price to pay, consider that it's the same thing you would do in ML or Haskell to implement a dynamic or universal type.

Do you have a reference? I find it hard to believe that it should be possible to derive complete type information in a sort of bottom-up manner at runtime, when this is not possible statically. For example, how do you get the type of, say, the equivalent of ref(nil)? This seems to require (arbitrarily remote) contextual information.

I can see that a source-to-source transformation might work, but that does not really refute what I said, because the transformation is basically an extension of a static type checking/inference algorithm (unless I misunderstand your idea).

I find it hard to believe that it should be possible to derive complete type information in a sort of bottom-up manner at runtime, when this is not possible statically. For example, how do you get the type of, say, the equivalent of ref(nil)? This seems to require (arbitrarily remote) contextual information.

Who said anything about sort of bottom-up (:? A value in the store (for instance) is computed using arbitrarily remote contextual information, isn't it?

Well, when you derive types from computed values only, then it will basically be bottom-up, or how could it not be? A value in the store is computed bottom-up (ignoring futures for now) before being stored. And when the value is just nil (the empty list), then you'll at best have partial type information.

AFAICS, dynamically you can only infer information from results that you have already computed, i.e. past computations. A type system OTOH can sort of "look into the future", and infer the type of some expression from the way it is used "later" (the contextual information I was referring to). As soon as you no longer have least or principal types for everything (like with mutability) this becomes essential.

So unless you can point me to some paper that debunks my ignorance, I'm afraid I won't buy it. ;-)

[Oh dear, wasn't my intention to ignite yet another flamewar about this issue. Excuses to all.]

AFAICS, dynamically you can only infer information from results that you have already computed, i.e. past computations.

Results that you have already computed includes thunks you have constructed but not yet forced, yes?

I don't know of any paper that says what you want it to say (I'll consider writing it if you think anybody would be interested (:). There's nothing deep, it's just a hack (well, normalization by evaluation is kind of deep). The code is too long and uninteresting to post here (I've posted something similar in the past), but this is a real honest-to-god scheme interaction:

> (run (let ((x (literal '())))
       (begin+ (begin+ (display-type (type-of x))
                       (newline+))
               (cons+ (literal 7) x))))
#&(list . #&#&number)
(7)
> (run (cons+ (literal #t) (cons+ (literal 7) (literal '()))))

Error in type-checking: failed to unify #&#&number and #&boolean.
Type (debug) to enter the debugger.

The first expression prints a value and returns another. Notice how the type of '() is known to be list of numbers even "before" it has had a number consed onto it.

The nonstandard interpretation of values is as a pair of a (representation of a) type and a thunk, if the expression is welltyped, and an error otherwise. All that one needs to program at the source level with this nonstandard interpretation is lambda, pairing, and enough structure to represent the types.

And that includes inference as well as checking, as long as you care to code it up (see above). So you lose (: (don't feel bad, you were going up against lambda). Of course, your larger point that it is just a reimplementation of static inference is true. But so is the claim that a sum type in ML is just a "reimplementation" of runtime tagging.

Where does that leave us? With some doubt on the usefulness of claims of "you can't do X with language Y". On the one hand, as long as you give me some latitude, I can reify Scheme values, even functions, as their type at runtime (and catch type errors before "runtime"). On the other hand, if you don't, I will insist that a Haskell function that takes Either Int Bool doesn't *really* take either an int or a bool.

What you really do is splitting program execution into two separate phases: first you do static(!) type checking (which also performs a program transformation), and only when that is successful you execute the (transformed) program. Mind you, the static checking is performed at runtime, but that is not the same as checking dynamically - which I interpret as checking during computation, without relying on information from a separate analysis phase [*]. I would call your approach "late static checking" or something like that. It is an interesting idea on its own, of course, but I'm afraid it does not convince me wrt the point of discussion.

Regarding Either: I fully agree with you ;-). Taking a sum is isomorphic to that, but it's not the same. You'd need intersection types or other forms of polymorphism to express the very thing.

Likewise, I wouldn't disagree that defining a universal sum type, plus appropriate wrappers for primitives, qualifies as reimplementing dynamic tagging - it sure does.

So yes, I tend to agree with most of your conclusion. But I still consider claims like "dynamic checking can check everything static checking can" mistaken, or at least severely misleading.

[*] Without this interpretation, even the implementation of a REPL would suddenly turn a statically typed language into a dynamic one, because it's all "runtime"!

And partial evaluation should probably turn a dynamically typed language in to a statically typed one. (and actually any language with a macro system must be considerd to have static typing.)

But this would also lead to classifing among other thing CMU Common Lisp and Oz as statically typed language, as they do some analyizis even at compile time. And I think at this point that exact distinction starts to become meaningless. Especially as nobody realy seems to want a purly dynamic system.

Dynamic typing does not preclude static analysis. But its crux is that the operational semantics does not assume or rely on any prior typing analysis.

In any case, I'm confused by your argument. Not all static processing is static type checking. What has macro expansion to do with type checking?

I was reasoning that "static" means fixed or known at compile time, and "dynamic" means not static, and by that static type checking is checking done at compile time, and a macro is executed at compile time, and to do that you have to do som type checking, ergo your doing type checking at compile time.

But in hindsight I realize that you don't even make that interpretation of that static and dynamic typing is. But i have to wonder, what is it that is "static" about what you call "static typing"?

To me, "static" simply means before, and independent of, actual execution. I find terms like "compile-time" and "run-time" much too fixated on specific tool scenarios, and not making much sense in contexts where these do not apply. An interactive system is one obvious example, where both overlap. There are also cases where there isn't a single compilation step, but static analyses are performed at several points in time prior to execution (consider a type-safe linker).

Of course I'm aware that even with that interpretation there is no clear-cut distinction between static and dynamic. There are enough imaginable scenarios that blur the distinction further, or render it meaningless. Staged computation actually is doing that intentionally, for example.

Yes, I agree. Actually I think the terms dynamic, static and even type, are becoming more and more irrelevant.

Then I think we agree completely.

But the goal posts have moved pretty far from your original challenge (paraphrasing): how can you tell at runtime that a function has type int -> int before applying it? I answered the question, and I'm not sure why that answer should be rejected on the grounds that it relies on computing that the function has type int -> int before applying it!

You're focusing on a separation of phases that the programmer doesn't necessarily see. Here's the simpler answer I should have given without delving into implementation: you define a suitable set of combinators for constructing functions from int to int, and limit yourself to values constructed by those combinators. (Notice, no talk of staging. How do you guarantee that a value was produced by your combinators? That's a question of data hiding and encapsulation, which is orthogonal to static typing (though not everyone agrees).)

But the goal posts have moved pretty far from your original challenge (paraphrasing): how can you tell at runtime that a function has type int -> int before applying it?

Of course, that "challenge" was in reply to the claim I paraphrased above, so you have to take that context into account. And it established, at least from my reading, the implicit qualification "solely by means of dynamic typing (in the conventional sense)", which I assumed all the way ;-).

With that clarified, yes, it seems we agree. Which is satisfying :-).

You're thinking of contracts, a la Robby Findler and scheme.

One possible reason why types may be more useful with FP is that those languages eliminate most other sources of bugs.

With OOP, I find that static type systems very rarely catch anything that wouldn't be caught by unit tests. And you need the unit tests: there are too many places where you might have hidden state - wrong values - that the typechecker won't catch. If you're testing the actual values, then you get dynamic typechecks "for free", because you run the code every test cycle.

With FP, all state is explicit, and mistakes usually jump out at you through inspection of the code. Pattern-matching captures all possible values that the type can hold, and you know that if a function depends on state, you passed it in. So the primary remaining source of bugs is type errors, and a good static typechecker can make testing basically unnecessary. My (fairly limited) Haskell experience is that programs generally "just work" once they compile, even if I've been doing invasive modifications throughout the code.

I haven't done any large Haskell/Ocaml dynamic systems though, so I can't speak for how well this works with complex, dynamic, distributed systems. Certainly, complex modifications involve changes to more places - but there's more compiler checking, so you don't have to worry as much about breaking things. Also, type inference, structural typing, and a concise syntax help minimize the pain of such changes.

My experience in the Java world is that most large projects are moving to the Jini-model of lookups full of interfaces, dynamically retrieved by class - which supports your point. Granted, that could be because my employer has invested heavily in Jini technology (and was co-founded by one of the Jini architects), so naturally our software follows the same architectural patterns. I'm curious whether Haskell could scale to similar problems: the Acute people have done a lot on type-safe distributed programming, but to my knowledge no real project has used their system.

The Acute link is to a New Yorker article!

Oops, must not've picked it up with the copy/paste. Fixed now.

Saying that those with different opinions on dynamic typing think the world can be "characterized statically and immutably" is I think just a way of discounting the other side. There are meaningful ways of discussing the tradeoffs between dynamic and static type systems, but that's not one of them. And claiming that a dynamic world demands dynamic types seems to me little more than a pun.

I've been developing production software in ML for a decade, and my experience is that static type systems make it easier to deal with a dynamic and changing world, because it helps you change your software with confidence that your changes had the intended effect.

And ML certainly allows you to write dynamic systems in the sense of dynamic loading of code. There's nothing about the type system that prevents that, except that you have to agree on an interface for how your old code and new code will interact.

For me, the most compelling case for gradually typed languages is legacy code --- that's certainly what motivated the racket guys, and it's the same for Hack. If you ask Julien Verlauguet, I think you'll find that he sees no barrier to all of Facebook's code being strictly annotated, except for the complexity of making the change to a large existing codebase.

This is what I got from it: Visual Basic usually uses the dynamic type of an object to determine semantics. The XML syntactic sugar relied on the static type. This inconsistency screws things up. Therefore, static typing must suck.

"The problem is that they were trying to shoehorn two namespaces into a single member selection syntax"

Just for comparison, the Javascript DOM solves the same kind of problem without syntax additions, and allows any number of additional namespace 'axis':

Element.prototype.symbol -> Element.symbol
Element.attributes.symbol -> Element.@symbol
Element.childNodes.symbol -> Element.<symbol>
Element.style.symbol -> "no equivalent"

Or did I miss something?

It's almost as if they are trying to use syntax to give individual types (such as Element), namespaces (such as Attribute, Descendant), which hurts my head.

As Ethan says, there is lots of room for misunderstanding when reading a presentation as opposed to hearing/seeing it live. Many of the earlier responses reflect that. I'll respond to some of Ethan's points right now. A full response is likely to be far too long.

The security guarantees I'm referring to are the language level guarantees that have been popularized by the Java platform, and are largely similar in .Net. These are chiefly pointer/memory safety (e.g., you cannot corrupt arbitrary memory by forging pointers, private data is really private etc.) and type safety. The basic thesis is that because, as a practical matter, systems with mandatory typing rely on them heavily, failure of the type system is catastrophic. One can certainly imagine a system with mandatory typing that carefully avoided any critical dependency on the type system. As Ethan suggests, types would be checked dynamically as well as statically. This doesn't happen in reality - the temptation to bank on the type rules is simply too strong. This is a cultural issue - but cultural issues are very important in programming languages, and cannot be discounted.

Optional type systems could be as complex as mandatory ones - but the difference is that their complexity is self contained. The run time doesn't get more complex every time you add a type system feature. Reification of generics is a good example. Failure of an optional type system does not lead to overall system failure.

The central point of optional types is that it decouples elements of the language design and implementation. This means that the inevitable mistakes that happen are better contained and less harmful. So, if your optional type system is badly designed, or simply has a complex and buggy implementation, it doesn't have a systemic effect.

Language design is notoriously non-modular. Every little change tends to interact with many other seemingly unrelated features. In particular, there is usually a two way dependency between executable semantics and the type system. Optional types simplify matters by making the dependency one-way: types depend on the executable semantics, but not the other way around.

A similar situation holds with respect to type inference. In many cases (e.g., ML) the design of the type system was constrained by the need to support inference - so again, there is a bidirectional dependency, this time between type checking and type inference/reconsruction. I argue it is more robust to make the typechecker independent of type reconstruction. Leave reconstruction to tools, that are free to use any heuristics they want.

I agree (and noted in an earlier post) that the evidence is anecdotal. There is much more of it that I can add, but it is still anecdotal. So are all the arguments for mandatory typing. Language design is much more an art than a science.

Ethan is absolutely right that more such systems have do be built and experiented with. This is starting to happen, and we should see confernece papers on pluggable types in not too long, describing actual implementations. I hope to write something along these lines in the foreseeable future, and I know others are too.

Finally, I will insist that in most statically typed languages, runtime semantics do depend on the type system. This applies to Fortran or ML as much as it does to Java, C#, Modula-1/2/3, Beta.

I followed the same reasoning as you. I have been using OCaml for years and while it's a very good programming language, I got bored with the static runtime that comes with it. IMHO, it's not because everything is typed at compile time that you don't need types at runtime.

More exactly, you would like to be able to define which amount of type informations gathered at compile time you want to be able to use at runtime. That's the reason why I wrote Neko which is a dynamicly typed intermediate language which is targeted by NekoML and other languages such as haXe. A static compiler plus a dynamic runtime proves to play quite good together since you get both safety and flexibility.

I'm not sure I understand your point about the 'type inference': in Scala when the type inferencer fails to analyse the type of an expression, well you just get a compile-time error and you have to declare yourself the type of the expression.

The type inferencer is deliberatedly simple so that the programmer is not surprised in a situation where there could be an ambiguous choice.

That's the best choice in my opinion.

Erlang people take pride in the fact that when people have write type systems for Erlang and typed the standard libraries and demo applications they have actually found few or no bugs. For example, I quote from the Soft Type System for Erlang paper:

We have presented a soft-typing system for Erlang. The system is based
on two ideas -- use a specification language to give the interface of
each module, and use a data flow analysis to verify that the
implementation of the module matches the specication.

As we saw in the experimental section, the system can reason about
substantial programs and produce useful results. It is worth noting
that even though the programs were debugged and tested, the type
system still produced warnings. The warnings typically concerned
programming constructs that the data flow analysis could not analyze
precisely (and where one would not expect any other static typing
system to give better results).

One disappointing result is that the experiments did not
uncover a single bug in programs that had already been tested and
debugged. Perhaps this is an indication that careful testing tends to
reveal most type errors.

We can't be too smug though because the programs are in fact rife with bugs.

I would certainly hope there were few bugs in the standard libraries that would be discoverable by static analysis. :-) In fact, I would tend to agree that careful testing reveals most type errors. One of the advantages of a good static type system is that you don't have to spend as much time on fuzz-testing.

But, how about general, run-of-the-mill code?

Also, it could be argued that Erlang programmers are self-selected not to write those kinds of bugs in the first place, given that they're macho, careful, telecom types. I could suppose that the popularity of a language is inversely related to the median skill of the language's users.

And I would like to point out that "warnings [that] typically concerned programming constructs that the data flow analysis could not analyze precisely" would be precisely the thing that would prevent the use of the checeker on an existing codebase.

[Eh, median, not mean. -TM]

It is really a surprising result, especially given that there is really no lack of evidence that static analysis finds bugs, and it makes me wonder if the type systems in question are somehow not very good at catching errors. Many times when new static analysis tools have landed in OCaml, we've found bugs because of them. Indeed, I've often found bugs by taking an existing tricky piece of code and restructuring it to get more oomph out of the type system.

I think people who use static analysis tools on C and C++ code have similar experience --- and if you don't believe in the real-worldness of those results, listen to what Carmack has said on the subject.