[plt-scheme] (typeof obj)

From: YC (yinso.chen at gmail.com)
Date: Mon Jun 11 18:28:28 EDT 2007

Thanks for the clear answer Carl - below are just some more thoughts...

On 6/11/07, Carl Eastlund <cce at ccs.neu.edu> wrote:
>
>
> > 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.


Okay - I understand your point now - thanks for clarification.

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


If you mean exceptions arising outside of programmer's control such as out
of disk space, etc., I see those as defensive programming techniques, that
from an end user's perspective, failure to handle the exceptions is
incorrect semantic ;)

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


This is where I see a general exception or condition or continuation
mechanism, while good as building blocks, loses the richer information that
you are alluding with the add1 example (i.e. using number -> number loses
the richer meaning of int -> int) - but I am
digressing here...

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


I didn't know what type info is available internally in mzscheme, but assume
at least the latter. I would assume the lack of a detailed type system is
not an inadvertent admission in scheme specification - right? ;) And if the
reason is to support research and experimentation, that's fine.  If the
reason is because one cannot describe all types that would terminate, that's
fine too ;)

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


Wondering what people think of Qi (http://www.lambdassociates.org/) that
features a type system that doesn't guarantee to terminate... ;)
Thanks,
yc
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20070611/29749bd2/attachment.html>

Posted on the users mailing list.