On Thu, Dec 10, 2015 at 2:26 PM Klaus Ostermann <[email protected]> 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 [email protected]. For more options, visit https://groups.google.com/d/optout.
