> 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.
But in statically typed languages you usually have a typed equivalence relation like \Gamma |- t1 == t2 : T Your example would not be well-typed in standard statically typed languages, hence one would not reason that it is equal to #f. So I think my argument that usually you can replace "equals by equals" according to the typed equivalence relation holds. Presumably the property still holds in Typed Racket, but with regard to a much smaller equality relation in which many equations that one would intuitively expect to be true are not true. > 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. I agree that that's not true, but usually I would expect a statically typed language to have a typed equivalence relation |- t1 == t2 : T such that if E is an evaluation context, then E[t1] is welltyped iff E[t2] is welltyped. I think you can also define that equivalence relation for Typed Racket, but it would be rather small. So there is a price to be paid for the fancy (singleton and other) types in TypedRacket - which is fine if I get something else in return, but it is not clear to me right now what it is that is worth this price. -- 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.
