On Thu, Dec 10, 2015 at 11:26 AM, Klaus Ostermann <klaus...@gmail.com> wrote: > This looks a bit strange to me, because usually one would expect > well-typedness to be not destroyed by replacing "equals with equals".
I don't think any typed language respects this. For example: (if (= 1 1) #f "not a boolean") is equal to #f, but many type systems do not let you replace #f with that expression. ML for example. Also, in ocaml, this expression: let f = fun x -> x in ((f f) 1) aka this expression: (let ([f (λ (x) x)]) ((f f) 1)) type checks, but this one: (fun f -> ((f f) 1)) (fun x -> x) aka this one: ((λ (f) ((f f) 1)) (λ (x) x)) does not type check, even tho these are equal to each other. In general, if you define "equals" in "replacing equals for equals" by reference to underlying observable equivalence relation induced by an untyped semantics, then you certainly cannot have this design principle. Robby -- 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.
