> 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 [email protected]. For more options, visit https://groups.google.com/d/optout.
