Some Notes on Type
Last updated at 4:54 pm UTC on 16 January 2006
The following email raises some interesting topics that could lead to some more thouroughly worked out notes (anybody is invited to write them here)
From: Scott A Crosby
Subject: Re: Generalized Object Modules Design
Date: Thu, 7 Mar 2002 02:48:29 -0500 (EST)
On Wed, 6 Mar 2002, Lex Spoon wrote:
> > We could make up a term called "congruence" for some better way
> > to establish degrees of equivalence than signatures or interfaces.
> > There needs to be more semantics in congruence than the simple
> > matching that most systems do now.
> >
> > What are some good ways to do this?
> >
>
> A can of worms indeed! But it's an important part of programming
> languages, and it needs to be cracked some day or another.
putting on a small type-theory hat: I'm more usd to static and formal
type systems, barel complicated enough to underly realistic programming
languages, and not enough on subtyping systems, but I'll take a stab at
this.
All objects in any system have a type.
THe question is, is the type a function of the declared type of the
reference pointing to the object (static typing). Or explicit in the
actual object itself. (tag bits in the header), commonly called dynamic
typing.
In the first case, the type is known at compile time, so the compiler
just implicitly 'knows' the bits at that address stand for a particular
type.
Assuming a not-broken type system, in both cases, we can have strong
typing.
>
> Let me suggest two key ideas, and then toss them around a little:
>
> 1. Don't have the computer check the types.
You have to. :) Try passing a #color message to Integer :)
> 2. Types are attached to objects, not to modules or to classes. In
> fact, let's call them "dynamic types", and let's note that classes are
> dynamic types. Thus, we are really talking about the next generation of
> classes. :)
You can think of types as either being the classes themselvs, or the
interface of the classes (the vector of external messages that a class
allows. See SML-NJ's module signatures scheme).
>
> The first issue I have taken as common sense for a while now. Computer
> type systems are increasingly baroque as they attempt to describe larger
> classes of programs. Even so, I don't think there is any type system in
I'd say its more like they wish to get more flexible. Contrast Java's
collections which require everything to be cast to Object with C++'s
templates (similar to SML's polymorphic functions) which can be more
clear. The type indicates what is stored in the array, and can catch the
wrong thing being stored immediately, rather than a long time later.
Also, especially for complicated higher order functions or things that use
closures, there can be really nasty bugs, say, where you pass a closure
needing 2 arguments to a function that wants a closure needing 1 object..
(In squeak, something comparable would be imagining a bunch of code that
passed around and stored 0,1,2&3 argument blocks, where some blocks are
taking other blocks as arguments.)
> common use that can handle the arithmetic operations in Squeak's
> collection hierarchy: they are parametric by the number of dimensions of
> nested collections! It's not even a big loss to drop the computer
> checks; consider that most code has bugs, and thus that most code isn't
> even correct. How useful is it to have a formal proof that one
> incorrect module is substitutable for another module that is incorrect
> in different ways?
>
> The second issue came together as I wrote the first version of this
> email, and it prompted me to rewrite it. :) It combines ideas from
> many directions: static typing, the idea of classes being dynamic
> entities, and the ideas Nathanael and others have been batting around
> involving mixing classes together. Why should an object have just one
> type?
If you think of objects (blocks of memory) as being parameterized by
types, each object has only one type. But, types may be parameterized by
what interfaces they support... IE, think if
object is of type FOO
FOO is an interface of kind BAR.
In this case, two types of the same kind are replaceable.
So, for example, adding an unused field to an object changes the type of
that object, but it retains the same interface.
> It also plays into the static vs. dynamic languages idea. In a static
> language, you spend a lot of effort reasoning about the program before
> you run it. In a dynamic language, you just put it together and fire it
> up. Dynamic languages have simple and probably more natural reasoning,
> but they delay the detection of any problems.
But as they also have strong typing, they are not inherently less safe.
> And also, many language theorists say there is no such thing as a
> "dynamic type", and procede to talk about types in a way that indeed
mm Not sure what they mean here.
> makes no sense with respect to this thread. Well, of course those
> theorists are simply talking about "static types". Our dynamic types
> make perfect sense once you ignore certain assumptions such as "the
> compiler will prove the assertions". :)
>
> Okay, let's get a little more specific.
>
> Static and dynamic guys agree that types should be named by humans.
> Even if you have the computer doing lots of checks for you, the human is
> the only one who can know what types are interesting to reason about.
> The difference here is that the types won't be checked. If the silly
> human says "pi are PerfectSquare", then the computer should let it pass.
>
> Putting types on the objects instead of the classes is not only useful,
We already have that. 'foo class' :)
I guess you might consider 'foo species' to be a way to get the kind of an
object (which might be stated as 'foo class kind')
Semantically aweful, as kinds are not types, but oh well.
Its hard to get into this without defining and using a metalangauge to
describe everything.. In a metalangauge, types and kinds in an object
language are types in the metalanguage. :)
> but sometimes necessary. The simplest example I know is: "An Array of X
> is of type Comparable, if and only if X is of type Comparable". This
That'd be a second order type.. I believe that that haskell type
system has this.. (Damn I do need to learn haskell)
> typing pattern shows up a lot in Smalltalk. To generalize, any generic
> object can have functionality that is only present when its elements
> have certain functionality. In Smalltalk you implement this in the most
> natural way of writing a method and supposing that the elements meet
> whatever precondition you need; in statically typed languages you either
> don't write them or you write your program in a way that will have lots
> of dynamic type checks.
I'm pretty sure haskell's static type system can handle this.
Usually the problem isn't per-se the type system, but rather having a type
system that doesn't require the users to annotate every freakin thing.
>
> Finally, since this is Smalltalk, the types would surely be objects.
They are.. You might want to check out LF (Logical Framework).
Scott
