> On Dec 10, 2015, at 9:26 AM, Klaus Ostermann <klaus...@gmail.com> wrote: > > This Typed Racket term is well-typed: > > (+ 1 (if (= 0 (- 1 1)) 1 "x")) > > This one isn't: > > (+ 1 (if (= 0 (- 2 2)) 1 "x")) > > This looks a bit strange to me, because usually one would expect > well-typedness to be not destroyed by replacing "equals with equals”.
I think that your quotation marks here are well-placed; specifically, this is the crux of the argument: what’s “equal” in the eyes of the type checker? Put differently, what kinds of equality does the type checker encompass? In fact, there are *very few* type checkers that can reason about the fact that (- 1 1) is equal to zero; I’m confident that the type checkers associated with the 20 most popular languages today would simply discard this expression out of hand. However, you do point out a very important point about type checkers in general: it can be very important that *programmers* understand the system of logic associated with a type checker, because when a program fails to type check, a programmer must rewrite the program so that the type checker accepts it. If the type system is too complex—or “clever”—for the programmer to understand, she may be unable to replace the program with an equivalent one that the type checker approves of. John Clements > > I'd like to know the rationale for this design. It would be nice if one of > the designers could comment on this. > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
