On Thursday, December 10, 2015 at 8:26:02 PM UTC+1, Klaus Ostermann 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 guess that typed equivalence is in fact bigger; what's different is a different relation. (Please prepend "I guess" to _all_ my claims in this email). 1. I think the results you're quoting (especially the second) are corollaries of the substitution lemma; to show that, get E[t1] and E[T2] through substitution from E[x], where x is fresh with type T. While Typed Racket is not standard, I'm going to assume it has a traditional substitution lemma. 2. Typed Racket has subtyping, so `|- (- 1 1) = (- 2 2) : Number` holds, as it would in a usual language. But we can't substitute a Number in the context of the original example: E[x] = (+ 1 (if (= 0 x) 1 "x")) There we need an instance of Zero, and `|- (- 1 1) = (- 2 2) : Zero` indeed fails. The equivalence which holds usually but not in TR is another one. Let's define relation R as `e_1 R e_2` iff expressions e_1 and e_2 receive the same strongest type (before evaluation) and evaluate to the same value. This relation isn't part of the usual presentation of typical type systems, unlike typed equivalence; I'm thinking of both Martin-Löf type theory and Barendregt's Pure Type Systems (and unlike the rest of this mail, I'm rather confident of this). To be fair, typed equivalence is often only introduced for type systems with a conversion rule (like dependent ones). Then (- 1 1) R (- 2 2) holds in most languages and fails in Typed Racket, because TR refines the type of (- 1 1) but not the type of (- 2 2). Cheers, Paolo -- 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.
