On Thu, Dec 10, 2015 at 2:26 PM Klaus Ostermann <klaus...@gmail.com> wrote:
> > 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. > I don't think that's right. If we consider the equivalence relation you refer to at `Number`, then it's exactly as large as you expect. However, neither of the expressions in your first message are well-typed if we treat `t1` and `t2` as having the type `Number`. You can try this by annotating them with that type. What is happening here is that there are some terms from which Typed Racket derives the type `#false`, and others with type `0`, which _enlarges_ the set of typable terms to include programs like the ones you began with. Of course, the equivalence relation at `0` is smaller than at `Number`, leading to the result you see. As Robby pointed out, neither the set of terms with type Number, nor the set of terms with type `0`, nor the set of terms known to evaluate to #false, is closed under evaluation. As for the rationale for the current design of the numeric types in Typed Racket, you might be interested in our PADL 2012 paper, here: http://www.ccs.neu.edu/racket/pubs/padl12-stff.pdf -- 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.
