What is Expressiveness in a Computer Language

[Chris Smith]

We're talking at cross purposes. I'm questioning whether a strong
type system can be completely static as some people here seem to
think. I maintain that it is simply not possible to make compile time
guarantees about *all* runtime behavior and that, in particular,
narrowing conversions will _always_ require runtime checking.

Nah, we're not at cross-purposes. I'm discussing the same thing you
are. My answer is that while narrowing conversion are not (by
definition) type-safe, a sufficiently strong type system can remove
these type-unsafe narrowing conversions from a program.

Again, the discussion is about narrowing the result. It doesn't
matter how much the compiler knows about the ranges. When the
computation mixes types, the range of the result can only widen as the
compiler determines the types involved.

Well, there are certain operations that can reduce the range. For
example, dividing a number that's known to be in the range 6-10 by the
exact constant 2 yields a result that's guaranteed to be in the range 3-
5. That's a smaller range.

That said, though, there is a more fundamental point here. When you
perform a a narrowing type conversion, one of two things must be true:
(a) you know more about the types than the compiler, and thus know that
the conversion is safe, or (b) your code is broken. Exluding the
possibility that you've written buggy code, you must possess some
knowledge that convinces you the conversion is safe. In that case, we
need only allow the type system to have that same knowledge, and the
problem is solved.

(One thing worth pointing out here is that it's quite possible that you
want to do something different depending on the kind of data. In that
case, the sufficiently powerful type system would need to have rules so
that an if statemement creates a modified type environment to take that
into account. This is different from a runtime type check, in that you
are writing explicit code that provides correct program behavior in
either case.)

 

[Chris Smith]

I think that is a misconception. Even at the idealest point it will be
possible (and easy) to write buggy programs. Gödel!

I agree. I never said that the ideal point is achievable... only that
there is a convergence toward it. (In some cases, that convergence may
have stalled at some equilibrium point because of the costs of being
near that point.)

 

[Marshall]

So, how does this "dynamic" type work?

It can't simply be the "any" type, because that type has no/few
functions defined on it.

It isn't. From the abstract of the above paper:

[...] even in statically typed languages, there is often the need to
deal with data whose type cannot be determined at compile time. To handle
such situations safely, we propose to add a type Dynamic whose values are
pairs of a value v and a type tag T where v has the type denoted by T.
Instances of Dynamic are built with an explicit tagging construct and
inspected with a type safe typecase construct.

Well, all this says is that the type "dynamic" is a way to explicitly
indicate the inclusion of rtti. But that doesn't address my objection;
if a typesafe typecase construct is required, it's not like using
a dynamic language. They don't require typecase to inspect values
before one can, say, invoke a function.

"Gradual typing" as described in
<http://www.cs.rice.edu/~jgs3847/pubs/pubs/2006/siek06:_gradual.pdf> is
another alternative. The difference between gradual typing and a
"dynamic" type is one of convenience rather than expressiveness --
gradual typing does not require explicit tagging and typecase constructs.

Perhaps this is the one I should read; it sounds closer to what I'm
talking about.


Marshall

 

[Marshall]

It would depend on the type system, naturally.
Naturally!


It isn't clear to me which programs we would have to give up, either.
I don't have much experience in sophisticated typed languages. It is
rather easy to find programs that baffle an unsophisticated typed
language (C, C++, Java, etc.).

C and Java, certainly, but I'm wary these days about making
any statement about limitations on C++'s type system, for it is
subtle and quick to anger.

Looking back in comp.lang.lisp, I see these examples:

(defun noisy-apply (f arglist)
(format t "I am now about to apply ~s to ~s" f arglist)
(apply f arglist))

(defun blackhole (argument)
(declare (ignore argument))
#'blackhole)

But wait a sec. It seems that these were examples I invented in
response to the same question from you!

Ah, how well I remember that thread, and how little I got from it.

My memories of that thread are
1) the troll who claimed that Java was unable to read two numbers from
standard input and add them together.
2) The fact that all the smart people agreed the blackhole
function indicated something profound.
3) The fact that I didn't understand the black hole function.

The noisy-apply function I think I understand; it's generic on the
entire arglist. In fact, if I read it correctly, it's even generic
on the *arity* of the function, which is actually pretty impressive.
True? This is an issue I've been wrestling with in my own type
system investigations: how to address genericity across arity.

Does noisy-apply get invoked the same way as other functions?
That would be cool.

As to the black hole function, could you explain it a bit? I apologize
for my lisp-ignorance. I am sure there is a world of significance
in the # ' on the third line, but I have no idea what it is.

I agree. The point of static checking is to *not* run the program. If
the type system gets too complicated, it may be a de-facto interpreter.

Aha! A lightbulb just want off.

Consider that a program is a function parameterized on its input.
Static
analysis is exactly the field of what we can say about a program
without
know the values of its parameters.


Marshall

 

[David Hopwood]

David Hopwood wrote:
Marshall wrote:

The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?

In a statically typed language that has a "dynamic" type, all
dynamically typed programs are straightforwardly expressible.

So, how does this "dynamic" type work?

It can't simply be the "any" type, because that type has no/few
functions defined on it.

It isn't. From the abstract of the above paper:

[...] even in statically typed languages, there is often the need to
deal with data whose type cannot be determined at compile time. To handle
such situations safely, we propose to add a type Dynamic whose values are
pairs of a value v and a type tag T where v has the type denoted by T.
Instances of Dynamic are built with an explicit tagging construct and
inspected with a type safe typecase construct.

Well, all this says is that the type "dynamic" is a way to explicitly
indicate the inclusion of rtti. But that doesn't address my objection;
if a typesafe typecase construct is required, it's not like using
a dynamic language. They don't require typecase to inspect values
before one can, say, invoke a function.

I was answering the question posed above: "are there some programs that
we can't write *at all* in a statically typed language...?"

Perhaps this is the one I should read; it sounds closer to what I'm
talking about.

Right; convenience is obviously important, as well as expressiveness.

 

[David Hopwood]

Correction: as the paper on gradual typing referenced below points
out in section 5, something like the "typerec" construct of
<http://citeseer.ist.psu.edu/harper95compiling.html> would be
needed, in order for a system with a "dynamic" type to be equivalent
in expressiveness to dynamic typing or gradual typing.

("typerec" can be used to implement "dynamic"; it is more general.)

So, how does this "dynamic" type work?

It can't simply be the "any" type, because that type has no/few
functions defined on it.

It isn't. From the abstract of the above paper:

[...] even in statically typed languages, there is often the need to
deal with data whose type cannot be determined at compile time. To handle
such situations safely, we propose to add a type Dynamic whose values are
pairs of a value v and a type tag T where v has the type denoted by T.
Instances of Dynamic are built with an explicit tagging construct and
inspected with a type safe typecase construct.

"Gradual typing" as described in
<http://www.cs.rice.edu/~jgs3847/pubs/pubs/2006/siek06:_gradual.pdf> is
another alternative. The difference between gradual typing and a
"dynamic" type

This should be: the difference between gradual typing and a system with
"typerec"...

 

[Pascal Costanza]

No, I'm not. Were we to follow this path of definition, it would not
require that dynamic type systems catch ALL type errors; only that they
catch some. Not that it matters, though. I am analyzing the logical
consequences of your own definition. If those logical consequences were
impossible to fulfill, that would be an even more convincing reason to
find a new definition. Concepts of fairness don't enter into the
equation.

Yes it does. All static type systems define only a strict subset of all
possible errors to be covered, and leave others as runtime errors. The
same holds for dynamic type systems.

You've got to define something... or, I suppose, just go on using words
without definitions. You claimed to give a definition, though.

I have been led by others to believe that the right way to go in the
dynamic type sense is to first define type errors, and then just call
anything that finds type errors a type system. That would work, but it
would require a type error. You seem to want to push that work off of
the word "type error" and back onto "type system", but that requires
that you define what a type system is.

I didn't know I was supposed to give a definition.

Incidentally, in the case of static type systems, we define the system
(for example, using the definition given from Pierce many times this
thread), and then infer the definition of types and type errors from
there. Because a solid definition has been given first for a type
system without invoking the concepts of types or type errors, this
avoids being circular.

Do you mean this one? "A type system is a tractable syntactic method for
proving the absence of certain program behaviors by classifying phrases
according to the kinds of values they compute." This isn't really such a
strong definition because it shifts the problem of what exactly a type
system is to finding a definition for the word "kind".

But if this makes you happy, here is an attempt:

"A dynamic type system is a tractable syntactic method for proving the
absence of certain program behaviors by classifying values according to
their kinds."

Basically, this correlates with the typical approach of using tags to
indicate the type/kind/class of values. And indeed, this is what dynamic
type systems typically do: they check tags associated with values. Other
kinds of runtime errors are not raised because of such checks, but
because of other reasons. Therefore, there is naturally a distinction
between runtime errors that are type errors and those that are not.

I am not convinced that this definition of mine is a lot clearer than
what I have said before, but I am also not convinced that Pierce's
definition is any clearer either. It is merely a characterization of
what static type systems do.

The preciseness comes into play when actually defining a type system:
then you have to give definitions what the errors at runtime are that
you want to prove absent by way of the static type system, give the
typing rules for the type system, and then prove soundness by showing
that the typing rules correlate precisely to the runtime errors in the
first stage. Since you have to map two different views of the same thing
to each other you have to be precise in giving definitions that you can
then successfully use in your proofs.

In dynamic type system, this level of precision is not necessary because
proving that dynamic type errors is what the dynamic type system catches
is trivially true, and most programmers don't care that there is a
distinction between runtime type errors and runtime "other" errors. But
this doesn't mean that this distinction doesn't exist.


Pascal

 

[Pascal Costanza]

A bold assertion!

The general question is, what do we do about partial functions?



This is an implementation artifact, and hence not relevant to our
understanding of the issue.

No, it's not. I am pretty sure that you can model this formally.


Pascal

 

[Ole Nielsby]

A good debugger is invaluable regardless of your attitude
to type systems.

I found that certain language features help greatly in pinning
the errors, when programming in my own impure fp language
(PILS).

Originally, I implemented a single-stepping debugger for the
language, but I trashed it for three reasons, of which two are
rather uninteresting here: it messed up the GUI system, and the
evaluation order of PILS made single-stepping a confusing
experience.

The interesting reason is: I didn't need single-stepping, partly
because the programming system is unit-test friendly, partly
because of language features that seem to mimick the concept
of taking responsibility.

Basically, the PILS execution mechanism is pessimistic. When
a function is called, the assumption is it won't work, and the
only way the function can return a result is by throwing an
exception. So, if a function call doesn't throw an exception,
it has failed and execution will stop unless the function call
is explicitly marked as fault tolerant, as in

f (x) else "undefined"

This has been merged with tail call flattening - rather than
throwing the result, an (expression, binding) thing is thrown
(I guess .NET'ers would call it an anonymous parameterless
delegate), and the expression is then evaluated after the throw.

Mimickally speaking, when a function body performs this
throw, it takes responsibility for getting the job done, and
if it fails, it will suffer the peril of having its guts exposed
in public by the error message window - much like certain
medieval penal systems. I will spare you for the gory details,
just let me add that to honor the demands of modern
bureaucracy, I added a "try the other office" feature so that
there are ways of getting things done without ever taking
responsibility.

Strangely, this all started 20 years ago as I struggled
implementing an early PILS version on an 8-bit Z80
processor, at a blazing 4 MHz. I needed a fast way of
escaping from a failing pattern match, and it turned
out the conditional return operation of this particular
processor was the fastest I could get. Somehow, the
concept of "if it returns, it's bad" crept into the language
design. I was puzzled by its expressiveness and the ease
of using it, only years later did I realize that its ease
of use came from the mimicking of responsibility.

I'm still puzzled that the notion of mimicking a cultural/
social concept came from a microprocessor instruction.
It seems like I - and perhaps computer language designers
in general - have a blind spot. We dig physical objects and
mathematical theories, and don't take hints from the
"soft sciences"...

Perhaps I'm over-generalizing, it just strikes me that the
dispute always seems to stand between math versus object
orientation, with seemingly no systematic attempts at
utilizing insigts from the study of languages and cultural
concepts. It's like as if COBOL and VB scared us from
ever considering the prospect of making programming
languages readable to the uninitiated.

 

[Pascal Costanza]

In a statically typed language that has a "dynamic" type, all
dynamically typed programs are straightforwardly expressible.

What about programs where the types change at runtime?


Pascal

 

[Pascal Costanza]

C and Java, certainly, but I'm wary these days about making
any statement about limitations on C++'s type system, for it is
subtle and quick to anger.

The noisy-apply function I think I understand; it's generic on the
entire arglist. In fact, if I read it correctly, it's even generic
on the *arity* of the function, which is actually pretty impressive.
True? This is an issue I've been wrestling with in my own type
system investigations: how to address genericity across arity.

Does noisy-apply get invoked the same way as other functions?
That would be cool.

As to the black hole function, could you explain it a bit? I apologize
for my lisp-ignorance. I am sure there is a world of significance
in the # ' on the third line, but I have no idea what it is.

You can ignore the #'. In Scheme this as follows:

(define blackhole (argument)
blackhole)

It just means that the function blackhole returns the function blackhole.


Pascal

 

[David Hopwood]

It isn't clear to me which programs we would have to give up, either.
I don't have much experience in sophisticated typed languages. It is
rather easy to find programs that baffle an unsophisticated typed
language (C, C++, Java, etc.).

Looking back in comp.lang.lisp, I see these examples:

(defun noisy-apply (f arglist)
(format t "I am now about to apply ~s to ~s" f arglist)
(apply f arglist))

'noisy-apply' is typeable using either of these systems:

<http://www.cs.jhu.edu/~pari/papers/fool2004/first-class_FOOL2004.pdf>
<http://www.coli.uni-saarland.de/publikationen/softcopies/Muller:1998:TIF.pdf>

(it should be easy to see the similarity to a message forwarder).

(defun blackhole (argument)
(declare (ignore argument))
#'blackhole)

This is typeable in any system with universally quantified types (including
most practical systems with parametric polymorphism); it has type
"forall a . a -> #'blackhole".

Certainly! As soon as you can reflect on the type system you can
construct programs that type-check iff they fail to type-check.

A program that causes the type checker not to terminate (which is the
effect of trying to construct such a thing in the type-reflective systems
I know about) is hardly useful.

In any case, I think the question implied the condition: "and that you
can write in a language with no static type checking."

[...]

I agree. The point of static checking is to *not* run the program. If
the type system gets too complicated, it may be a de-facto interpreter.

The following LtU post:

<http://lambda-the-ultimate.org/node/1085>

argues that types should be expressed in the same language that is being
typed. I am not altogether convinced, but I can see the writer's point.

There do exist practical languages in which types can be defined as
arbitrary predicates or coercion functions, for example E (www.erights.org).
E implementations currently perform type checking only at runtime, however,
although it was intended to allow static analysis for types that could be
expressed in a conventional static type system. I think the delay in
implementing this has more to do with the E developers' focus on other
(security and concurrency) issues, rather than an inherent difficulty.

 

[Joe Marshall]

Ah, how well I remember that thread, and how little I got from it.

My memories of that thread are
1) the troll who claimed that Java was unable to read two numbers from
standard input and add them together.
2) The fact that all the smart people agreed the blackhole
function indicated something profound.
3) The fact that I didn't understand the black hole function.

The noisy-apply function I think I understand; it's generic on the
entire arglist. In fact, if I read it correctly, it's even generic
on the *arity* of the function, which is actually pretty impressive.
True?
Yes.

This is an issue I've been wrestling with in my own type
system investigations: how to address genericity across arity.

Does noisy-apply get invoked the same way as other functions?
That would be cool.

Yes, but in testing I found an incompatability. Here's a better
definiton:

(defun noisy-apply (f &rest args)
(format t "~&Applying ~s to ~s." f (apply #'list* args))
(apply f (apply #'list* args)))

CL-USER> (apply #'+ '(2 3))
5

CL-USER> (noisy-apply #'+ '(2 3))
Applying #<function + 20113532> to (2 3).
5

The internal application of list* flattens the argument list. The
Common Lisp APPLY function has variable arity and this change makes my
NOISY-APPLY be identical.

As to the black hole function, could you explain it a bit?

It is a function that takes any argument and returns the function
itself.

I apologize
for my lisp-ignorance. I am sure there is a world of significance
in the # ' on the third line, but I have no idea what it is.

The #' is a namespace operator. Since functions and variables have
different namespaces, I'm indicating that I wish to return the function
named blackhole rather than any variable of the same name that might be
around.

 

[David Hopwood]

What about programs where the types change at runtime?

Staged compilation is perfectly compatible with static typing.
Static typing only requires that it be possible to prove absence
of some category of type errors when the types are known; it
does not require that all types are known before the first-stage
program is run.

There are, however, staged compilation systems that guarantee that
the generated program will be typeable if the first-stage program
is.

(It's clear that to compare the expressiveness of statically and
dynamically typed languages, the languages must be comparable in
other respects than their type system. Staged compilation is the
equivalent feature to 'eval'.)

 

[Joe Marshall]

Sorry, but can you elaborate on this last point a little? I think I
missed something.

This is just the halting problem lifted up into the type domain.

 

[Greg Buchholz]

That was interesting, but the authors' method still involves runtime
checking of the array bounds. IMO, all they really succeeded in doing
was turning the original recursion into CPS and making the code a
little bit clearer.

Hmm. There is a comparison in both the DML and Haskell code, but
that's just there to make the binary search terminate correctly. The
point of the exercise is the line in the DML code "val m = (hi + lo)
div 2", or the "bmiddle" function in the Haskell code. If you change
that line to something like "val m = (hi + lo)" you'll get a compiler
error complaining about an unsolved constraint. The point of the
Haskell code is to use the type system to ensure that array indices
have a know provenance. They're derived from and statically associated
with each individual array, so you can't use an index from one array
with a different array. You'll probably also enjoy the paper...

"Eliminating Array Bound Checking Through Dependent Types"
http://citeseer.ist.psu.edu/xi98eliminating.html

....and DML itself...

http://www.cs.bu.edu/~hwxi/DML/DML.html

Greg Buchholz

 

[Chris Smith]

You can ignore the #'. In Scheme this as follows:

(define blackhole (argument)
blackhole)

It just means that the function blackhole returns the function blackhole.

So, in other words, it's equivalent to (Y (\fa.f)) in lambda calculus,
where \ is lambda, and Y is the fixed point combinator?

 

[Greg Buchholz]

It isn't clear to me which programs we would have to give up, either.
I don't have much experience in sophisticated typed languages. It is
rather easy to find programs that baffle an unsophisticated typed
language (C, C++, Java, etc.).

Looking back in comp.lang.lisp, I see these examples:

(defun noisy-apply (f arglist)
(format t "I am now about to apply ~s to ~s" f arglist)
(apply f arglist))

Just for fun, here is how you might do "apply" in Haskell...

{-# OPTIONS -fglasgow-exts #-}

class Apply x y z | x y -> z where
apply :: x -> y -> z

instance Apply (a->b) a b where
apply f x = f x

instance Apply b as c => Apply (a->b) (a,as) c where
apply f (x,xs) = apply (f x) xs

f :: Int -> Double -> String -> Bool -> Int
f x y z True = x + floor y * length z
f x y z False= x * floor y + length z

args = (1::Int,(3.1415:ouble,("flub",True)))

main = print $ apply f args


....which depends on the fact that functions are automatically curried
in Haskell. You could do something similar for fully curried function
objects in C++. Also of possible interest...

Functions with the variable number of (variously typed) arguments
http://okmij.org/ftp/Haskell/types.html#polyvar-fn

....But now I'm curious about how to create the "apply" function in a
language like Scheme. I suppose you could do something like...

(define (apply fun args)
(eval (cons fun args)))

....but "eval" seems a little like overkill. Is there a better way?


Greg Buchholz

 

[Joe Marshall]

This is typeable in any system with universally quantified types (including
most practical systems with parametric polymorphism); it has type
"forall a . a -> #'blackhole".

The #' is just a namespace operator. The function accepts a single
argument and returns the function itself. You need a type that is a
fixed point (in addition to the universally quantified argument).

A program that causes the type checker not to terminate (which is the
effect of trying to construct such a thing in the type-reflective systems
I know about) is hardly useful.

In any case, I think the question implied the condition: "and that you
can write in a language with no static type checking."

Presumably the remainder of the program does something interesting!

The point is that there exists (by construction) programs that can
never be statically checked. The next question is whether such
programs are `interesting'. Certainly a program that is simply
designed to contradict the type checker is of limited entertainment
value, but there should be programs that are independently non
checkable against a sufficiently powerful type system.

 

[David Hopwood]

This is typeable in any system with universally quantified types (including
most practical systems with parametric polymorphism); it has type
"forall a . a -> #'blackhole".

Ignore this answer; I misinterpreted the code.

I believe this example requires recursive types. It can also be expressed
in a gradual typing system, but possibly only using an unknown ('?') type.

ISTR that O'Caml at one point (before version 1.06) supported general
recursive types, although I don't know whether it would have supported
this particular example.