<div>On 6/11/07, Carl Eastlund <<a href="mailto:cce@ccs.neu.edu">cce@ccs.neu.edu</a>> wrote:<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"> > 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.</blockquote><div> 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?  </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"> > 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.)</blockquote><div> 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. </div> <blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">> 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.</blockquote><div> 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 </div></div>