[plt-scheme] (typeof obj)

On 6/11/07, YC <yinso.chen at gmail.com> wrote:
>
> On 6/11/07, Shriram Krishnamurthi <sk at cs.brown.edu> wrote:
> > > What is the type of ADD1?  What is the type of CALL/CC?  How
> > > about of (lambda (x) x)?  Or
> >
> > >   (let ([x 3])
> > >     (lambda (y)
> > >       (when (= (random 2) 0)
> > >           (set! x y))
> > >      x))
> >
> > > ?
>
> Shouldn't mzscheme know the answer to these questions?  It seems possible
> within Haskell or Ocaml to infer the types - below is my attempt but I
> probably have the syntax wrong.
>
> add1 is int -> int
> (lambda (x) x) is any -> any
> I don't understand enough about call/cc so I won't attempt ;)
> (let ((x 3)) (lambda (y) (when (= (random 2) 0) (set! x y)) x)) can be void
> -> (any -> (union int any))
>
> And the contract system does allow such specifications manually - running
> (add1 "a") returns a run-time type mismatch error.

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.

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.)

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.

-- 
Carl Eastlund