Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

On Friday, December 11, 2015 at 1:21:04 AM UTC+1, Matthias Felleisen wrote: > On Dec 10, 2015, at 3:04 PM, Klaus Ostermann wrote: > > > Thanks for the clarification, Sam. What you write makes sense. > > > > However, since the default case (without explicit annotations) is that I > > get these

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

On Dec 11, 2015, at 6:36 AM, Paolo Giarrusso wrote: > On Friday, December 11, 2015 at 1:21:04 AM UTC+1, Matthias Felleisen wrote: >> On Dec 10, 2015, at 3:04 PM, Klaus Ostermann wrote: >> >>> Thanks for the clarification, Sam. What you write makes sense. >>> >>>

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

> You don't use types as abstraction barriers. > > You use modules aas abstraction barriers. > And in your module system you specify explicitly how much type > information is exported to be used to type-check the module user. > > Modules are not types. But they can contain type definitions.

[racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

This Typed Racket term is well-typed: (+ 1 (if (= 0 (- 1 1)) 1 "x")) This one isn't: (+ 1 (if (= 0 (- 2 2)) 1 "x")) This looks a bit strange to me, because usually one would expect well-typedness to be not destroyed by replacing "equals with equals". I'd like to know the rationale for this

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

On Thu, Dec 10, 2015 at 2:26 PM 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

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

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

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

Thanks for the clarification, Sam. What you write makes sense. However, since the default case (without explicit annotations) is that I get these very (too?) precise singleton types, I have the impression that reasoning about (typed) program equivalence is more difficult in TR than in standard

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

> 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

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

On Dec 10, 2015, at 3:04 PM, Klaus Ostermann wrote: > Thanks for the clarification, Sam. What you write makes sense. > > However, since the default case (without explicit annotations) is that I get > these very (too?) precise singleton types, I have the impression that >

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

On Thu, Dec 10, 2015 at 07:22:40PM -0500, Matthias Felleisen wrote: > > On Dec 10, 2015, at 3:04 PM, Klaus Ostermann wrote: > > > Thanks for the clarification, Sam. What you write makes sense. > > > > However, since the default case (without explicit annotations) is that I

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

> On Dec 10, 2015, at 4:47 PM, Hendrik Boom wrote: > > On Thu, Dec 10, 2015 at 07:22:40PM -0500, Matthias Felleisen wrote: >> >> On Dec 10, 2015, at 3:04 PM, Klaus Ostermann wrote: >> >>> Thanks for the clarification, Sam. What you write makes

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

> On Dec 10, 2015, at 9:26 AM, Klaus Ostermann wrote: > > This Typed Racket term is well-typed: > > (+ 1 (if (= 0 (- 1 1)) 1 "x")) > > This one isn't: > > (+ 1 (if (= 0 (- 2 2)) 1 "x")) > > This looks a bit strange to me, because usually one would expect >

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

On Thu, Dec 10, 2015 at 11:26 AM, Klaus Ostermann wrote: > This looks a bit strange to me, because usually one would expect > well-typedness to be not destroyed by replacing "equals with equals". I don't think any typed language respects this. For example: (if (= 1 1) #f

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

In typed racket (- 1 1) and (- 2 2) are equal at runtime, but the type checker doesn't necessarily know that at compile time. It knows that (- 1 1) is zero because that's a special case in the type system. But it doesn't have a special case for (- 2 2), so it only knows that that's a Fixnum.

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

On Thu, Dec 10, 2015 at 08:25:11PM -0500, Matthias Felleisen wrote: > > > > On Dec 10, 2015, at 4:47 PM, Hendrik Boom wrote: > > > > On Thu, Dec 10, 2015 at 07:22:40PM -0500, Matthias Felleisen wrote: > >> > >> On Dec 10, 2015, at 3:04 PM, Klaus Ostermann

Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

You may want to read our papers on Units, Harper/Lillibridge and Leroy both from POPL ’94 and chase the citations forward. But perhaps Reynolds’s old saying “type structure is a syntactic discipline for enforcing levels of abstraction” suffices — Matthias (yes, I have studied all of this too