Lambda the Ultimate

All type systems are ALWAYS a compromise with the Halting problem.

A type system is a way of proving that programs have certain properties, and proving properties about arbitrary programs is just what the Halting problem is. So we try to come up with systems that type most of the programs people naturally write, and don't take too long to run, and don't fail to terminate.

This is always a tradeoff, and sometimes it's a good idea to give up on termination for all programs in order to get success on the programs people do write.

sometimes it's a good idea to give up on termination for all programs in order to get success on the programs people do write

Sadly, sometimes language designers go the other way and say "it's a good idea to give up on all of the programs people might write in order to get decidable type checking for all of the programs we will let them write."

;-)

In fact, I am one of the people who say "it's a good idea to give up on all of the programs people might write in order to get decidable type checking for all of the programs we will let them write."

That's because a restriction cuts two ways. First, it sets limits on the data you can construct as output. This is obvious.

Second, and less obviously, a restriction strengthens the invariants on the data you receive as input. This means that you can make stronger assumptions about your input, and this means you can do more things with your input data!

For example, in a language like Scheme or ML, there's no way to ensure that repeated calls to a function will return the same results, since the function might rely on a piece of imperative state.

So a pair expression like (f(x), f(x)) can't be safely refactored into let v = f(x) in (v,v). In Haskell, by contrast, this IS a correct transformation. And it's only correct because the language is restricted so that all functions are pure, which gives you stronger invariants to work with.

So there isn't any simple tradeoff between restrictions and expressiveness. Adding a restriction can increase the strength of your invariants, which can increase expressiveness more than it costs. That's why language design can get tricky....

Just a nitpick, since I agree with your comment in general: in the example you chose, if the compiler has access to enough of the source code and is sufficiently smart(tm), e.g. a whole-program compiler, then it can make that transformation.

That's why language design can get tricky....

Right - rather than the "sadly" of the OP, I'd say "happily, language designers are exploring all parts of the PL type system universe."

If you're receiving f as an argument to a function, then you can't always make that transformation, because you don't know what you're going to get as an argument. A whole program optimizer can find that out some of the time, but not all of the time.

D'oh!

Well, one can express pure constructions in ML using abstract types. Here is the basic idea expressed in Standard ML:

infix 9 $

structure SKI :>
   sig
      type 'a t
      val prj : 'a t -> 'a
      val $ : ('a -> 'b) t * 'a t -> 'b t
      val S : (('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c) t
      val K : ('a -> 'b -> 'a) t
      val I : ('a -> 'a) t
   end = struct
      type 'a t = 'a
      fun prj x = x
      fun f $ x = f x
      fun S x y z = x z (y z)
      fun K x _ = x
      fun I x = S K K x
   end

There is no way in SML to construct impure values of type t, because there is no function for injecting arbitrary values to the type and the only values of that type are pure.