<br><div><span class="gmail_quote">On 6/11/07, <b class="gmail_sendername">Carl Eastlund</b> <<a href="mailto:email@example.com">firstname.lastname@example.org</a>> wrote:</span><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<br>> could be real -> real, or number -> number. On the other hand, a<br>> general number -> number function is not acceptable as int -> int
<br>> because it might return a non-int, and add1 is a valid int -> int<br>> function, so no one of these specifications is adequate for it.</blockquote><div><br>Ah - I misread add1's definition, thanks for the correction.
<br><br>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? <br><br></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<br>> non-numeric value and run the code. It may raise an exception, but<br>> there's nothing wrong with that. In fact, even statically typed
<br>> languages like ML allow programs to raise an exception, and -- here's<br>> the fun part -- this behavior is generally allowed to have any return<br>> type. So add1 can also be assigned the type any -> any, and if you
<br>> really want to you could assign it types like string -> symbol or<br>> list-of-vector -> vector-of-list. (The funny logic goes: because it<br>> will never return a value on those inputs, every value it does return
<br>> vacuously belongs to the type symbol or vector-of-list.)</blockquote><div><br>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?
<br><br>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.
<br></div><br><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<br>> many different, complicated types. Assigning a single one is a
<br>> shortcut used by some static type systems to simplify their job, thus<br>> restricting the use of such functions to that single type. PLT Scheme<br>> lets you use add1 as any of the above types, thus it cannot tell you
<br>> which type the function has. Its type is any and all of the above.</blockquote><div><br>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.
<br><br>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? <br><br>Thanks,<br>yc<br><br></div></div>