[plt-scheme] (typeof obj)

On 6/11/07, YC <yinso.chen at gmail.com> wrote:
>
> On the other hand, if int is a subtype of number, shouldn't a number ->
> number function suffice as its definition as it can return int -> int as
> well?

Not at all.  The function (lambda (x) 3.7) qualifies as a number ->
number function, but it is not int -> int.  Calling add1 a number ->
number function throws away valuable information about how it can be
used on integers, positive numbers, and so forth.

> But raising exception here means the type of the parameter is incorrect -
> i.e. it still has a type semantics, even though checking is deferred to
> runtime rather than compile time, right?

Raising an exception means control passes to the nearest dynamically
installed exception handler, nothing more or less.  Programs and
semantics don't make value judgments.  Programs often raise exceptions
when nothing "incorrect" has happened.

As for the "type semantics" of raising an exception, as I said, many
static type systems treat expressions known to raise exceptions as
having any type.  Hence my statement that add1, which raises an
exception on large classes of inputs, has many different return types
for those inputs.  If you want to assign a different "type semantics"
to exceptions, you'll have to describe your type system in greater
detail.

> Just to be clear, I am not looking for a static type system (although some
> of its properties are nice).  I am "okay" with run-time type checking rather
> than compile time, I just find it more cumbersome to do type-based
> dispatching.

You can still do some kinds of dispatching, but because no static
analysis is performed, you won't get details such as input and output
types for functions.  In Scheme, all you'll get are type tags, such as
procedure or number or cons cell.

> I understand typing is not easy, and that's why many languages come with a
> type system and developers just use it rather than inventing their own.  My
> take here is that scheme also has a type system (at least for the value
> objects) but type is not a first class citizen like lambda or continuation,
> and hence make type-based programming more effort.

Do you mean conceptually, as in "we can imagine the type int -> int
for add1"?  Or do you mean actually, in that "Scheme knows that add1
is a procedure"?  Of course in the former sense, we can apply most
type systems to just about any language.  In the latter, Scheme has a
type system, but not a very detailed one.

> It does seem that most of the responses are about that you cannot type them
> all and hence there isn't a complete type system that can do (typeof obj) -
> is this a correct assessment?  Is this a done subject (i.e . there are
> proofs that one cannot type everything that can be computed) or is this just
> the current state of art?

Depends on what you mean.  Of course, in Scheme you can assign a type
to everything, but "Scheme value" is not a very useful type.  On the
other hand, if your type system uses "int -> int" to designate
"functions which, when given an integer input, always terminate and
yield an integer result", then yes you will run into problems trying
to typecheck some functions, partly because of that "always terminate"
clause.  There are some things type systems can't do.

--
Carl Eastlund