[plt-scheme] (typeof obj)

On 6/11/07, Carl Eastlund <cce at ccs.neu.edu> wrote:
>
> > You say add1 is int -> int, but it accepts real numbers too, so it
> > could be real -> real, or number -> number.  On the other hand, a
> > general number -> number function is not acceptable as int -> int
> > because it might return a non-int, and add1 is a valid int -> int
> > function, so no one of these specifications is adequate for it.


Ah - I misread add1's definition, thanks for the correction.

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?

> But wait, there's more.  In PLT Scheme, you can apply add1 to a
> > non-numeric value and run the code.  It may raise an exception, but
> > there's nothing wrong with that.  In fact, even statically typed
> > languages like ML allow programs to raise an exception, and -- here's
> > the fun part -- this behavior is generally allowed to have any return
> > type.  So add1 can also be assigned the type any -> any, and if you
> > really want to you could assign it types like string -> symbol or
> > list-of-vector -> vector-of-list.  (The funny logic goes: because it
> > will never return a value on those inputs, every value it does return
> > vacuously belongs to the type symbol or vector-of-list.)


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?

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.

> As you can see, even apparently simple functions like add1 can have
> > many different, complicated types.  Assigning a single one is a
> > shortcut used by some static type systems to simplify their job, thus
> > restricting the use of such functions to that single type.  PLT Scheme
> > lets you use add1 as any of the above types, thus it cannot tell you
> > which type the function has.  Its type is any and all of the above.


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.

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?

Thanks,
yc
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20070611/32b6aeae/attachment.html>