Re: [racket-dev] math collection [was: Hyperbolic functions]
Ten minutes in, I've hit a snag. I'd like the stuff in math/functions to have precise types. For example, log1p could have the type (case-> (Zero -> Zero) (Float -> Float) (Real -> Real)) It was easy to get the implementation to typecheck, but when I tried to plot it in untyped Racket, I got this: Type Checker: The type of log1p cannot be converted to a contract in: log1p I really don't want to have two versions of the library. Could TR use the most general type (Real -> Real) as the contract? Or would that be unsound? Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
In this case, the contract could turn into a dependent one with the same semantics. Does it make sense for TR to allow a user to declare the equivalent contract? Robby On Tue, Jun 26, 2012 at 7:17 PM, Neil Toronto wrote: > Ten minutes in, I've hit a snag. I'd like the stuff in math/functions to > have precise types. For example, log1p could have the type > > (case-> (Zero -> Zero) > (Float -> Float) > (Real -> Real)) > > It was easy to get the implementation to typecheck, but when I tried to plot > it in untyped Racket, I got this: > > Type Checker: The type of log1p cannot be converted to a contract in: log1p > > I really don't want to have two versions of the library. Could TR use the > most general type (Real -> Real) as the contract? Or would that be unsound? > > Neil ⊥ > _ > Racket Developers list: > http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
How would you check soundness between a type and its contract? Types, like theorem provers, are addictive. The more expressivity they provide, the more programmers want to play with them. Use Real -> Real and you'll be fine. -- Matthias On Jun 26, 2012, at 8:37 PM, Robby Findler wrote: > In this case, the contract could turn into a dependent one with the > same semantics. Does it make sense for TR to allow a user to declare > the equivalent contract? > > Robby > > On Tue, Jun 26, 2012 at 7:17 PM, Neil Toronto wrote: >> Ten minutes in, I've hit a snag. I'd like the stuff in math/functions to >> have precise types. For example, log1p could have the type >> >> (case-> (Zero -> Zero) >> (Float -> Float) >> (Real -> Real)) >> >> It was easy to get the implementation to typecheck, but when I tried to plot >> it in untyped Racket, I got this: >> >> Type Checker: The type of log1p cannot be converted to a contract in: log1p >> >> I really don't want to have two versions of the library. Could TR use the >> most general type (Real -> Real) as the contract? Or would that be unsound? >> >> Neil ⊥ >> _ >> Racket Developers list: >> http://lists.racket-lang.org/dev > > _ > Racket Developers list: > http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
I'm addicted to optimizations. If I use Real -> Real, TR can't prove that (log1p 1.0) is Float and... hmm. I'll let Vincent explain why that's bad. :) Another option is to provide both log1p and fllog1p. I just wrote fllog1p anyway. Neil ⊥ On 06/26/2012 07:05 PM, Matthias Felleisen wrote: How would you check soundness between a type and its contract? Types, like theorem provers, are addictive. The more expressivity they provide, the more programmers want to play with them. Use Real -> Real and you'll be fine. -- Matthias On Jun 26, 2012, at 8:37 PM, Robby Findler wrote: In this case, the contract could turn into a dependent one with the same semantics. Does it make sense for TR to allow a user to declare the equivalent contract? Robby On Tue, Jun 26, 2012 at 7:17 PM, Neil Toronto wrote: Ten minutes in, I've hit a snag. I'd like the stuff in math/functions to have precise types. For example, log1p could have the type (case-> (Zero -> Zero) (Float -> Float) (Real -> Real)) It was easy to get the implementation to typecheck, but when I tried to plot it in untyped Racket, I got this: Type Checker: The type of log1p cannot be converted to a contract in: log1p I really don't want to have two versions of the library. Could TR use the most general type (Real -> Real) as the contract? Or would that be unsound? Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
On Jun 26, 2012, at 9:12 PM, Neil Toronto wrote: > I'm addicted to optimizations. If I use Real -> Real, TR can't prove that > (log1p 1.0) is Float and... hmm. I'll let Vincent explain why that's bad. :) > > Another option is to provide both log1p and fllog1p. I just wrote fllog1p > anyway. Sounds like the right solution -- and now you see how every type system forces you to duplicate code. -- Matthias _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
Well, you wouldn't. Are the implementations of the contracts proven to be equivalent currently? Or do you just have a theorem that matches up the ones in some model somewhere? Robby On Tue, Jun 26, 2012 at 8:05 PM, Matthias Felleisen wrote: > > How would you check soundness between a type and its contract? > > Types, like theorem provers, are addictive. The more expressivity > they provide, the more programmers want to play with them. > > Use Real -> Real and you'll be fine. -- Matthias > > > > On Jun 26, 2012, at 8:37 PM, Robby Findler wrote: > >> In this case, the contract could turn into a dependent one with the >> same semantics. Does it make sense for TR to allow a user to declare >> the equivalent contract? >> >> Robby >> >> On Tue, Jun 26, 2012 at 7:17 PM, Neil Toronto wrote: >>> Ten minutes in, I've hit a snag. I'd like the stuff in math/functions to >>> have precise types. For example, log1p could have the type >>> >>> (case-> (Zero -> Zero) >>> (Float -> Float) >>> (Real -> Real)) >>> >>> It was easy to get the implementation to typecheck, but when I tried to plot >>> it in untyped Racket, I got this: >>> >>> Type Checker: The type of log1p cannot be converted to a contract in: log1p >>> >>> I really don't want to have two versions of the library. Could TR use the >>> most general type (Real -> Real) as the contract? Or would that be unsound? >>> >>> Neil ⊥ >>> _ >>> Racket Developers list: >>> http://lists.racket-lang.org/dev >> >> _ >> Racket Developers list: >> http://lists.racket-lang.org/dev > _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
This sounds like a terrible solution. There are lots of places in our system where we just declare facts and don't prove them and then use them for lots of things (often optimizations). Why should this one be special? Robby On Tue, Jun 26, 2012 at 8:16 PM, Matthias Felleisen wrote: > > On Jun 26, 2012, at 9:12 PM, Neil Toronto wrote: > >> I'm addicted to optimizations. If I use Real -> Real, TR can't prove that >> (log1p 1.0) is Float and... hmm. I'll let Vincent explain why that's bad. :) >> >> Another option is to provide both log1p and fllog1p. I just wrote fllog1p >> anyway. > > > Sounds like the right solution -- and now you see how every type system > forces you to duplicate code. -- Matthias > _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
Huh? On Jun 26, 2012, at 9:27 PM, Robby Findler wrote: > Well, you wouldn't. Are the implementations of the contracts proven to > be equivalent currently? Or do you just have a theorem that matches up > the ones in some model somewhere? > > Robby > > On Tue, Jun 26, 2012 at 8:05 PM, Matthias Felleisen > wrote: >> >> How would you check soundness between a type and its contract? >> >> Types, like theorem provers, are addictive. The more expressivity >> they provide, the more programmers want to play with them. >> >> Use Real -> Real and you'll be fine. -- Matthias >> >> >> >> On Jun 26, 2012, at 8:37 PM, Robby Findler wrote: >> >>> In this case, the contract could turn into a dependent one with the >>> same semantics. Does it make sense for TR to allow a user to declare >>> the equivalent contract? >>> >>> Robby >>> >>> On Tue, Jun 26, 2012 at 7:17 PM, Neil Toronto >>> wrote: Ten minutes in, I've hit a snag. I'd like the stuff in math/functions to have precise types. For example, log1p could have the type (case-> (Zero -> Zero) (Float -> Float) (Real -> Real)) It was easy to get the implementation to typecheck, but when I tried to plot it in untyped Racket, I got this: Type Checker: The type of log1p cannot be converted to a contract in: log1p I really don't want to have two versions of the library. Could TR use the most general type (Real -> Real) as the contract? Or would that be unsound? Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev >>> >>> _ >>> Racket Developers list: >>> http://lists.racket-lang.org/dev >> _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
Because the point of types is to have something proven. On Jun 26, 2012, at 9:29 PM, Robby Findler wrote: > This sounds like a terrible solution. > > There are lots of places in our system where we just declare facts and > don't prove them and then use them for lots of things (often > optimizations). Why should this one be special? > > Robby > > On Tue, Jun 26, 2012 at 8:16 PM, Matthias Felleisen > wrote: >> >> On Jun 26, 2012, at 9:12 PM, Neil Toronto wrote: >> >>> I'm addicted to optimizations. If I use Real -> Real, TR can't prove that >>> (log1p 1.0) is Float and... hmm. I'll let Vincent explain why that's bad. :) >>> >>> Another option is to provide both log1p and fllog1p. I just wrote fllog1p >>> anyway. >> >> >> Sounds like the right solution -- and now you see how every type system >> forces you to duplicate code. -- Matthias >> _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
I'm saying that people can make mistakes in Racket currently that undermine the guarantees of the type system. But lets continue the other line first. On Tue, Jun 26, 2012 at 8:28 PM, Matthias Felleisen wrote: > > Huh? > > On Jun 26, 2012, at 9:27 PM, Robby Findler wrote: > >> Well, you wouldn't. Are the implementations of the contracts proven to >> be equivalent currently? Or do you just have a theorem that matches up >> the ones in some model somewhere? >> >> Robby >> >> On Tue, Jun 26, 2012 at 8:05 PM, Matthias Felleisen >> wrote: >>> >>> How would you check soundness between a type and its contract? >>> >>> Types, like theorem provers, are addictive. The more expressivity >>> they provide, the more programmers want to play with them. >>> >>> Use Real -> Real and you'll be fine. -- Matthias >>> >>> >>> >>> On Jun 26, 2012, at 8:37 PM, Robby Findler wrote: >>> In this case, the contract could turn into a dependent one with the same semantics. Does it make sense for TR to allow a user to declare the equivalent contract? Robby On Tue, Jun 26, 2012 at 7:17 PM, Neil Toronto wrote: > Ten minutes in, I've hit a snag. I'd like the stuff in math/functions to > have precise types. For example, log1p could have the type > > (case-> (Zero -> Zero) > (Float -> Float) > (Real -> Real)) > > It was easy to get the implementation to typecheck, but when I tried to > plot > it in untyped Racket, I got this: > > Type Checker: The type of log1p cannot be converted to a contract in: > log1p > > I really don't want to have two versions of the library. Could TR use the > most general type (Real -> Real) as the contract? Or would that be > unsound? > > Neil ⊥ > _ > Racket Developers list: > http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev >>> > _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
Certainly the dependent contract approach will work, but the 'Real -> Real' contract is also safe, so I'll see about generating that. Sam On Jun 26, 2012 8:37 PM, "Robby Findler" wrote: > In this case, the contract could turn into a dependent one with the > same semantics. Does it make sense for TR to allow a user to declare > the equivalent contract? > > Robby > > On Tue, Jun 26, 2012 at 7:17 PM, Neil Toronto > wrote: > > Ten minutes in, I've hit a snag. I'd like the stuff in math/functions to > > have precise types. For example, log1p could have the type > > > > (case-> (Zero -> Zero) > > (Float -> Float) > > (Real -> Real)) > > > > It was easy to get the implementation to typecheck, but when I tried to > plot > > it in untyped Racket, I got this: > > > > Type Checker: The type of log1p cannot be converted to a contract in: > log1p > > > > I really don't want to have two versions of the library. Could TR use the > > most general type (Real -> Real) as the contract? Or would that be > unsound? > > > > Neil ⊥ > > _ > > Racket Developers list: > > http://lists.racket-lang.org/dev > > _ > Racket Developers list: > http://lists.racket-lang.org/dev > _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
I agree with that, to a point. Here were are now considering a very concrete tradeoff, however: asking the user to cope with code duplication in return for ... what? Very little, I claim. In particular, I think that TR already has lots of type+contracts that are asserted (not proven) to be equivalent. For example, + seems to have a pretty big type in the implementation--- has that contract been proven to match to the type? That is, what I'm trying to say is that there are currently a few people that can make these unproven assertions about types and contracts that match up. Why should they be the only ones? EVEN BETTER: we can use random testing to falsify these! Systematically! Vincent is already doing this a little bit and he has found bugs. If we make this an explicit thing to connect types to contracts and allow people to make more connections, then we can do a better job finding bugs in the currently untested/unproven ones! (random testing uber alles :) Robby On Tue, Jun 26, 2012 at 8:29 PM, Matthias Felleisen wrote: > > Because the point of types is to have something proven. > > > On Jun 26, 2012, at 9:29 PM, Robby Findler wrote: > >> This sounds like a terrible solution. >> >> There are lots of places in our system where we just declare facts and >> don't prove them and then use them for lots of things (often >> optimizations). Why should this one be special? >> >> Robby >> >> On Tue, Jun 26, 2012 at 8:16 PM, Matthias Felleisen >> wrote: >>> >>> On Jun 26, 2012, at 9:12 PM, Neil Toronto wrote: >>> I'm addicted to optimizations. If I use Real -> Real, TR can't prove that (log1p 1.0) is Float and... hmm. I'll let Vincent explain why that's bad. :) Another option is to provide both log1p and fllog1p. I just wrote fllog1p anyway. >>> >>> >>> Sounds like the right solution -- and now you see how every type system >>> forces you to duplicate code. -- Matthias >>> > _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
The safety in this case doesn't generalize to contracts like the one Neil is suggesting when you go from an untyped value to a typed one, tho, right? Robby On Tue, Jun 26, 2012 at 8:32 PM, Sam Tobin-Hochstadt wrote: > Certainly the dependent contract approach will work, but the 'Real -> Real' > contract is also safe, so I'll see about generating that. > > Sam > > On Jun 26, 2012 8:37 PM, "Robby Findler" > wrote: >> >> In this case, the contract could turn into a dependent one with the >> same semantics. Does it make sense for TR to allow a user to declare >> the equivalent contract? >> >> Robby >> >> On Tue, Jun 26, 2012 at 7:17 PM, Neil Toronto >> wrote: >> > Ten minutes in, I've hit a snag. I'd like the stuff in math/functions to >> > have precise types. For example, log1p could have the type >> > >> > (case-> (Zero -> Zero) >> > (Float -> Float) >> > (Real -> Real)) >> > >> > It was easy to get the implementation to typecheck, but when I tried to >> > plot >> > it in untyped Racket, I got this: >> > >> > Type Checker: The type of log1p cannot be converted to a contract in: >> > log1p >> > >> > I really don't want to have two versions of the library. Could TR use >> > the >> > most general type (Real -> Real) as the contract? Or would that be >> > unsound? >> > >> > Neil ⊥ >> > _ >> > Racket Developers list: >> > http://lists.racket-lang.org/dev >> >> _ >> Racket Developers list: >> http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
If even the few people who understand the type basis properly get types wrong, why should you have programmers open up loopholes into types that are supposed to "harden" their programs? When I have just a few implementors manipulate the type base I can stick to the allusion that the language is perfect and its implementation flawed, but fixable. When everyone can open loopholes, I need to question every single decision I made concerning such loopholes. (If we base optimizations on them, we might descend into the C++ pit.) -- Matthias On Jun 26, 2012, at 9:34 PM, Robby Findler wrote: > I agree with that, to a point. Here were are now considering a very > concrete tradeoff, however: asking the user to cope with code > duplication in return for ... what? Very little, I claim. In > particular, I think that TR already has lots of type+contracts that > are asserted (not proven) to be equivalent. For example, + seems to > have a pretty big type in the implementation--- has that contract been > proven to match to the type? > > That is, what I'm trying to say is that there are currently a few > people that can make these unproven assertions about types and > contracts that match up. Why should they be the only ones? > > EVEN BETTER: we can use random testing to falsify these! > Systematically! Vincent is already doing this a little bit and he has > found bugs. If we make this an explicit thing to connect types to > contracts and allow people to make more connections, then we can do a > better job finding bugs in the currently untested/unproven ones! > > (random testing uber alles :) _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
Do you only use code that uses the FFI that people you trust wrote? How about code in the runtime system? Both of these have lots of people contributing code that can (and does) easily undermine basic Racket guarantees, and you don't complain about that. Do you care about type system guarantees more than basic safety guarantees? Stepping back, I don't like this general philosophy. Relying on "proof by smart implementer" is borderline immoral to me. I think have a declarative language that programmers can program to specify what they want to specify is the right approach to most everything, including the specification of optimization opportunities and typed/untyped boundaries, and whatever else. (I think we don't do this for inlining-type optimization is that generalizing to a language is hard, not because we don't want to do it.) I do think that we have to rely on people being responsible for their code and I don't mean to imply otherwise, but throwing up arbitrary boundaries like this doesn't (in my opinion) actually help anyone guarantee anything in practice. Robby Technical note: I was wrong below -- I only know of bugs Vincent found between the type declarations and the untyped implementation, but I think both of our comments still stand in light of that revision. On Tue, Jun 26, 2012 at 8:42 PM, Matthias Felleisen wrote: > > If even the few people who understand the type basis properly > get types wrong, why should you have programmers open up loopholes > into types that are supposed to "harden" their programs? When I have > just a few implementors manipulate the type base I can stick to the > allusion that the language is perfect and its implementation flawed, > but fixable. When everyone can open loopholes, I need to question > every single decision I made concerning such loopholes. (If we base > optimizations on them, we might descend into the C++ pit.) > > -- Matthias > > > > On Jun 26, 2012, at 9:34 PM, Robby Findler wrote: > >> I agree with that, to a point. Here were are now considering a very >> concrete tradeoff, however: asking the user to cope with code >> duplication in return for ... what? Very little, I claim. In >> particular, I think that TR already has lots of type+contracts that >> are asserted (not proven) to be equivalent. For example, + seems to >> have a pretty big type in the implementation--- has that contract been >> proven to match to the type? >> >> That is, what I'm trying to say is that there are currently a few >> people that can make these unproven assertions about types and >> contracts that match up. Why should they be the only ones? >> >> EVEN BETTER: we can use random testing to falsify these! >> Systematically! Vincent is already doing this a little bit and he has >> found bugs. If we make this an explicit thing to connect types to >> contracts and allow people to make more connections, then we can do a >> better job finding bugs in the currently untested/unproven ones! >> >> (random testing uber alles :) > _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
On Tue, Jun 26, 2012 at 9:36 PM, Robby Findler wrote: > The safety in this case doesn't generalize to contracts like the one > Neil is suggesting when you go from an untyped value to a typed one, > tho, right? Right, if we have an untyped value which we'd like to give the `case->` type that Neil described, we'd need to use a dependent contract, as you suggested. That's on the longer-term todo list. For the typed->untyped case, when the arguments and results are all first-order, the algorithm that Vincent uses for printing `case->` types will also work for generating appropriate simpler contracts, such as `(-> real? real?)`. Sam > Robby > > On Tue, Jun 26, 2012 at 8:32 PM, Sam Tobin-Hochstadt > wrote: >> Certainly the dependent contract approach will work, but the 'Real -> Real' >> contract is also safe, so I'll see about generating that. >> >> Sam >> >> On Jun 26, 2012 8:37 PM, "Robby Findler" >> wrote: >>> >>> In this case, the contract could turn into a dependent one with the >>> same semantics. Does it make sense for TR to allow a user to declare >>> the equivalent contract? >>> >>> Robby >>> >>> On Tue, Jun 26, 2012 at 7:17 PM, Neil Toronto >>> wrote: >>> > Ten minutes in, I've hit a snag. I'd like the stuff in math/functions to >>> > have precise types. For example, log1p could have the type >>> > >>> > (case-> (Zero -> Zero) >>> > (Float -> Float) >>> > (Real -> Real)) >>> > >>> > It was easy to get the implementation to typecheck, but when I tried to >>> > plot >>> > it in untyped Racket, I got this: >>> > >>> > Type Checker: The type of log1p cannot be converted to a contract in: >>> > log1p >>> > >>> > I really don't want to have two versions of the library. Could TR use >>> > the >>> > most general type (Real -> Real) as the contract? Or would that be >>> > unsound? >>> > >>> > Neil ⊥ >>> > _ >>> > Racket Developers list: >>> > http://lists.racket-lang.org/dev >>> >>> _ >>> Racket Developers list: >>> http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler wrote: > This sounds like a terrible solution. > > There are lots of places in our system where we just declare facts and > don't prove them and then use them for lots of things (often > optimizations). Why should this one be special? I don't know of any places like this in Racket. What are you thinking of? Certainly, Typed Racket is intended to be sound in the same sense that Racket is safe, and that Haskell, OCaml, and Java are safe as well: if you don't use specifically-marked unsafe features (such as the FFI and `racket/unsafe/ops`), then you get a guarantee that depends only on the correctness of the runtime system/compiler, not on the correctness of any user code. I think this a very important guarantee: we've seen far too often that trusting user code in languages like C and C++ was a big mistake in many contexts. Sam > On Tue, Jun 26, 2012 at 8:16 PM, Matthias Felleisen > wrote: >> >> On Jun 26, 2012, at 9:12 PM, Neil Toronto wrote: >> >>> I'm addicted to optimizations. If I use Real -> Real, TR can't prove that >>> (log1p 1.0) is Float and... hmm. I'll let Vincent explain why that's bad. :) >>> >>> Another option is to provide both log1p and fllog1p. I just wrote fllog1p >>> anyway. >> >> >> Sounds like the right solution -- and now you see how every type system >> forces you to duplicate code. -- Matthias >> > _ > Racket Developers list: > http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
On Tue, Jun 26, 2012 at 9:25 PM, Sam Tobin-Hochstadt wrote: > On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler > wrote: >> This sounds like a terrible solution. >> >> There are lots of places in our system where we just declare facts and >> don't prove them and then use them for lots of things (often >> optimizations). Why should this one be special? > > I don't know of any places like this in Racket. What are you thinking of? The inliner and the JIT compiler and that whole interaction are the ones I thought of. I should have said "lots of facts" not "lots of places", tho. Sorry about that. > Certainly, Typed Racket is intended to be sound in the same sense that > Racket is safe, and that Haskell, OCaml, and Java are safe as well: if > you don't use specifically-marked unsafe features (such as the FFI and > `racket/unsafe/ops`), then you get a guarantee that depends only on > the correctness of the runtime system/compiler, not on the correctness > of any user code. Of course I understand this. I'm pointing out that this is not a significant guarantee, in and of itself (see last para below for an elaboration here). > I think this a very important guarantee: we've seen > far too often that trusting user code in languages like C and C++ was > a big mistake in many contexts. I don't think this is an either/or. Indeed, just to continue with C: if everyone understood that the types were really just size markers and nothing else, then lots of the seeming unsoundness goes away in C (not all, of course, and as I've been learning from Regehr's blog, there are lots of other dark corners). But no one is suggesting we remove checks from array bounds, which is what really cost society money wrt to C and, IMO, the kind of invariant that matters. That is, what should guide is is NOT "do we have a theorem like some other big popular (or not so popular I guess) language?" but "what invariants should I help programmers that read my code be aware of?". While these are similar kinds of things, they are not just the same as "types = where invariants go" or "type soundness is what we need". As a concrete example: I think that our elimination of mutable cons cells was a change we made that made it far easier to reason about the correctness of our multithreaded code and this has nothing to do with types. (And just to be sure I'm being clear: types are a great way to get all kinds of invariants. I like that.) So, just to be sure we're all on the same page here: I'm writing all this as a counter argument to Matthias's claim about whether or not it is a good idea to allow users of TR to declare that specific types match up to specific contracts. I mean for all this email spooge to be considered only in that context, not in some more general way. Robby _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
On Tue, Jun 26, 2012 at 10:44 PM, Robby Findler wrote: > On Tue, Jun 26, 2012 at 9:25 PM, Sam Tobin-Hochstadt > wrote: >> On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler >> wrote: >>> This sounds like a terrible solution. >>> >>> There are lots of places in our system where we just declare facts and >>> don't prove them and then use them for lots of things (often >>> optimizations). Why should this one be special? >> >> I don't know of any places like this in Racket. What are you thinking of? > > The inliner and the JIT compiler and that whole interaction are the > ones I thought of. I should have said "lots of facts" not "lots of > places", tho. Sorry about that. I'm still not sure what you're thinking of. What operation does the inliner or JIT perform that is justified by a programmer-declared-but-not-checked fact? >> Certainly, Typed Racket is intended to be sound in the same sense that >> Racket is safe, and that Haskell, OCaml, and Java are safe as well: if >> you don't use specifically-marked unsafe features (such as the FFI and >> `racket/unsafe/ops`), then you get a guarantee that depends only on >> the correctness of the runtime system/compiler, not on the correctness >> of any user code. > > Of course I understand this. I'm pointing out that this is not a > significant guarantee, in and of itself (see last para below for an > elaboration here). > >> I think this a very important guarantee: we've seen >> far too often that trusting user code in languages like C and C++ was >> a big mistake in many contexts. > > I don't think this is an either/or. Indeed, just to continue with C: > if everyone understood that the types were really just size markers > and nothing else, then lots of the seeming unsoundness goes away in C > (not all, of course, and as I've been learning from Regehr's blog, > there are lots of other dark corners). But no one is suggesting we > remove checks from array bounds, which is what really cost society > money wrt to C and, IMO, the kind of invariant that matters. I don't think the distinction that you're trying to draw here is meaningful. In particular, to return to our earlier example, if you assert the type Neil gave for an untyped value, backed up with the contract `(-> real? real?)`, then Typed Racket's type system can be off by arbitrarily much -- no claim it makes can be trusted. Further, the optimizer will happily transform your program from one that behaves one way to a different program, and cause the entire Racket runtime to segfault. So if we went the route that you're suggesting, Typed Racket might serve the "what invariants should I help programmers that read my code be aware of?" role, but we'd have to take out the optimizer, and the claims that if Typed Racket tells you something, then you know it to be true (modulo the extensive caveats about bugs in TR, Racket, GCC, Linux, Intel, etc). I don't think that's the right trade to make. Sam > That is, what should guide is is NOT "do we have a theorem like some > other big popular (or not so popular I guess) language?" but "what > invariants should I help programmers that read my code be aware of?". > While these are similar kinds of things, they are not just the same as > "types = where invariants go" or "type soundness is what we need". > > As a concrete example: I think that our elimination of mutable cons > cells was a change we made that made it far easier to reason about the > correctness of our multithreaded code and this has nothing to do with > types. (And just to be sure I'm being clear: types are a great way to > get all kinds of invariants. I like that.) > > So, just to be sure we're all on the same page here: I'm writing all > this as a counter argument to Matthias's claim about whether or not it > is a good idea to allow users of TR to declare that specific types > match up to specific contracts. I mean for all this email spooge to be > considered only in that context, not in some more general way. > > Robby _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
On Tue, Jun 26, 2012 at 10:08 PM, Sam Tobin-Hochstadt wrote: > On Tue, Jun 26, 2012 at 10:44 PM, Robby Findler > wrote: >> On Tue, Jun 26, 2012 at 9:25 PM, Sam Tobin-Hochstadt >> wrote: >>> On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler >>> wrote: This sounds like a terrible solution. There are lots of places in our system where we just declare facts and don't prove them and then use them for lots of things (often optimizations). Why should this one be special? >>> >>> I don't know of any places like this in Racket. What are you thinking of? >> >> The inliner and the JIT compiler and that whole interaction are the >> ones I thought of. I should have said "lots of facts" not "lots of >> places", tho. Sorry about that. > > I'm still not sure what you're thinking of. What operation does the > inliner or JIT perform that is justified by a > programmer-declared-but-not-checked fact? There are many operations that are implemented partially in JIT and wholly in the runtime system. The JIT generated version gets used unless certain conditions hold, in which case the runtime system version gets used. The programmer declared fact is embedded into the code and not specified as a fact per se, but for example, there is one such fact saying "this pile of assembly instructions is equivalent to the C implementation of list-ref, under the condition that the number argument is a fixnum less than 10,000 and we don't run out of pairs too soon" (roughly). There are large pile of such things. Another one you're probably more familiar with: "this pile of assembly instructions is equivalent to + when the arguments are both fixnums or both flonums". There is another pile of such invariants in the (pre-bytecode level) inliner. It relies on beta substitution and the ability to run certain primitives at compile time. (I don't know as much about that one, so probably there are more things it relies on than that.) >>> Certainly, Typed Racket is intended to be sound in the same sense that >>> Racket is safe, and that Haskell, OCaml, and Java are safe as well: if >>> you don't use specifically-marked unsafe features (such as the FFI and >>> `racket/unsafe/ops`), then you get a guarantee that depends only on >>> the correctness of the runtime system/compiler, not on the correctness >>> of any user code. >> >> Of course I understand this. I'm pointing out that this is not a >> significant guarantee, in and of itself (see last para below for an >> elaboration here). >> >>> I think this a very important guarantee: we've seen >>> far too often that trusting user code in languages like C and C++ was >>> a big mistake in many contexts. >> >> I don't think this is an either/or. Indeed, just to continue with C: >> if everyone understood that the types were really just size markers >> and nothing else, then lots of the seeming unsoundness goes away in C >> (not all, of course, and as I've been learning from Regehr's blog, >> there are lots of other dark corners). But no one is suggesting we >> remove checks from array bounds, which is what really cost society >> money wrt to C and, IMO, the kind of invariant that matters. > > I don't think the distinction that you're trying to draw here is > meaningful. In particular, to return to our earlier example, if you > assert the type Neil gave for an untyped value, backed up with the > contract `(-> real? real?)`, then Typed Racket's type system can be > off by arbitrarily much -- no claim it makes can be trusted. I think you're making this out to be a boogey man, when it really isn't. But why doesn't your argument apply to any program that uses the FFI? It also invalidates all of the guarantees that TR makes. (And there are essentially no programs that don't use the FFI anymore.) And anyways, I think that TR actually makes *no* guarantees in a precise technical sense. Even if I accept the proofs about the models in your papers then (as I said earlier) we are not running your models. Why should you be the only allowed to introduce these particular bugs? I'm allowed to introduce other bugs, for example. > Further, > the optimizer will happily transform your program from one that > behaves one way to a different program, and cause the entire Racket > runtime to segfault. So if we went the route that you're suggesting, > Typed Racket might serve the "what invariants should I help > programmers that read my code be aware of?" role, but we'd have to > take out the optimizer, and the claims that if Typed Racket tells you > something, then you know it to be true (modulo the extensive caveats > about bugs in TR, Racket, GCC, Linux, Intel, etc). I don't think > that's the right trade to make. (I don't really get what you're saying here at all, but I also think it isn't really an argument against my argument.) But I'll note that you forgot perl in your list. I'm sure it is used in the build process of one of those tools that we rely on. Everything is hopeless. Robby __
Re: [racket-dev] math collection [was: Hyperbolic functions]
I haven't got a clue what you two are arguing about anymore. If you both stop, maybe Sam can implement that perfectly safe change to the typed -> untyped contract barrier that he said he could do. That would be nice. ;) Neil ⊥ On 06/26/2012 09:23 PM, Robby Findler wrote: On Tue, Jun 26, 2012 at 10:08 PM, Sam Tobin-Hochstadt wrote: On Tue, Jun 26, 2012 at 10:44 PM, Robby Findler wrote: On Tue, Jun 26, 2012 at 9:25 PM, Sam Tobin-Hochstadt wrote: On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler wrote: This sounds like a terrible solution. There are lots of places in our system where we just declare facts and don't prove them and then use them for lots of things (often optimizations). Why should this one be special? I don't know of any places like this in Racket. What are you thinking of? The inliner and the JIT compiler and that whole interaction are the ones I thought of. I should have said "lots of facts" not "lots of places", tho. Sorry about that. I'm still not sure what you're thinking of. What operation does the inliner or JIT perform that is justified by a programmer-declared-but-not-checked fact? There are many operations that are implemented partially in JIT and wholly in the runtime system. The JIT generated version gets used unless certain conditions hold, in which case the runtime system version gets used. The programmer declared fact is embedded into the code and not specified as a fact per se, but for example, there is one such fact saying "this pile of assembly instructions is equivalent to the C implementation of list-ref, under the condition that the number argument is a fixnum less than 10,000 and we don't run out of pairs too soon" (roughly). There are large pile of such things. Another one you're probably more familiar with: "this pile of assembly instructions is equivalent to + when the arguments are both fixnums or both flonums". There is another pile of such invariants in the (pre-bytecode level) inliner. It relies on beta substitution and the ability to run certain primitives at compile time. (I don't know as much about that one, so probably there are more things it relies on than that.) Certainly, Typed Racket is intended to be sound in the same sense that Racket is safe, and that Haskell, OCaml, and Java are safe as well: if you don't use specifically-marked unsafe features (such as the FFI and `racket/unsafe/ops`), then you get a guarantee that depends only on the correctness of the runtime system/compiler, not on the correctness of any user code. Of course I understand this. I'm pointing out that this is not a significant guarantee, in and of itself (see last para below for an elaboration here). I think this a very important guarantee: we've seen far too often that trusting user code in languages like C and C++ was a big mistake in many contexts. I don't think this is an either/or. Indeed, just to continue with C: if everyone understood that the types were really just size markers and nothing else, then lots of the seeming unsoundness goes away in C (not all, of course, and as I've been learning from Regehr's blog, there are lots of other dark corners). But no one is suggesting we remove checks from array bounds, which is what really cost society money wrt to C and, IMO, the kind of invariant that matters. I don't think the distinction that you're trying to draw here is meaningful. In particular, to return to our earlier example, if you assert the type Neil gave for an untyped value, backed up with the contract `(-> real? real?)`, then Typed Racket's type system can be off by arbitrarily much -- no claim it makes can be trusted. I think you're making this out to be a boogey man, when it really isn't. But why doesn't your argument apply to any program that uses the FFI? It also invalidates all of the guarantees that TR makes. (And there are essentially no programs that don't use the FFI anymore.) And anyways, I think that TR actually makes *no* guarantees in a precise technical sense. Even if I accept the proofs about the models in your papers then (as I said earlier) we are not running your models. Why should you be the only allowed to introduce these particular bugs? I'm allowed to introduce other bugs, for example. Further, the optimizer will happily transform your program from one that behaves one way to a different program, and cause the entire Racket runtime to segfault. So if we went the route that you're suggesting, Typed Racket might serve the "what invariants should I help programmers that read my code be aware of?" role, but we'd have to take out the optimizer, and the claims that if Typed Racket tells you something, then you know it to be true (modulo the extensive caveats about bugs in TR, Racket, GCC, Linux, Intel, etc). I don't think that's the right trade to make. (I don't really get what you're saying here at all, but I also think it isn't really an argument against my argument.) But I'll note that you forgot perl
Re: [racket-dev] math collection [was: Hyperbolic functions]
Consider me done! Robby On Tue, Jun 26, 2012 at 11:05 PM, Neil Toronto wrote: > I haven't got a clue what you two are arguing about anymore. If you both > stop, maybe Sam can implement that perfectly safe change to the typed -> > untyped contract barrier that he said he could do. That would be nice. > > ;) > > Neil ⊥ > > > On 06/26/2012 09:23 PM, Robby Findler wrote: >> >> On Tue, Jun 26, 2012 at 10:08 PM, Sam Tobin-Hochstadt >> wrote: >>> >>> On Tue, Jun 26, 2012 at 10:44 PM, Robby Findler >>> wrote: On Tue, Jun 26, 2012 at 9:25 PM, Sam Tobin-Hochstadt wrote: > > On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler > wrote: >> >> This sounds like a terrible solution. >> >> There are lots of places in our system where we just declare facts and >> don't prove them and then use them for lots of things (often >> optimizations). Why should this one be special? > > > I don't know of any places like this in Racket. What are you thinking > of? The inliner and the JIT compiler and that whole interaction are the ones I thought of. I should have said "lots of facts" not "lots of places", tho. Sorry about that. >>> >>> >>> I'm still not sure what you're thinking of. What operation does the >>> inliner or JIT perform that is justified by a >>> programmer-declared-but-not-checked fact? >> >> >> There are many operations that are implemented partially in JIT and >> wholly in the runtime system. The JIT generated version gets used >> unless certain conditions hold, in which case the runtime system >> version gets used. The programmer declared fact is embedded into the >> code and not specified as a fact per se, but for example, there is one >> such fact saying "this pile of assembly instructions is equivalent to >> the C implementation of list-ref, under the condition that the number >> argument is a fixnum less than 10,000 and we don't run out of pairs >> too soon" (roughly). There are large pile of such things. Another one >> you're probably more familiar with: "this pile of assembly >> instructions is equivalent to + when the arguments are both fixnums or >> both flonums". >> >> There is another pile of such invariants in the (pre-bytecode level) >> inliner. It relies on beta substitution and the ability to run certain >> primitives at compile time. (I don't know as much about that one, so >> probably there are more things it relies on than that.) >> > Certainly, Typed Racket is intended to be sound in the same sense that > Racket is safe, and that Haskell, OCaml, and Java are safe as well: if > you don't use specifically-marked unsafe features (such as the FFI and > `racket/unsafe/ops`), then you get a guarantee that depends only on > the correctness of the runtime system/compiler, not on the correctness > of any user code. Of course I understand this. I'm pointing out that this is not a significant guarantee, in and of itself (see last para below for an elaboration here). > I think this a very important guarantee: we've seen > far too often that trusting user code in languages like C and C++ was > a big mistake in many contexts. I don't think this is an either/or. Indeed, just to continue with C: if everyone understood that the types were really just size markers and nothing else, then lots of the seeming unsoundness goes away in C (not all, of course, and as I've been learning from Regehr's blog, there are lots of other dark corners). But no one is suggesting we remove checks from array bounds, which is what really cost society money wrt to C and, IMO, the kind of invariant that matters. >>> >>> >>> I don't think the distinction that you're trying to draw here is >>> meaningful. In particular, to return to our earlier example, if you >>> assert the type Neil gave for an untyped value, backed up with the >>> contract `(-> real? real?)`, then Typed Racket's type system can be >>> off by arbitrarily much -- no claim it makes can be trusted. >> >> >> I think you're making this out to be a boogey man, when it really isn't. >> >> But why doesn't your argument apply to any program that uses the FFI? >> It also invalidates all of the guarantees that TR makes. (And there >> are essentially no programs that don't use the FFI anymore.) >> >> And anyways, I think that TR actually makes *no* guarantees in a >> precise technical sense. Even if I accept the proofs about the models >> in your papers then (as I said earlier) we are not running your >> models. Why should you be the only allowed to introduce these >> particular bugs? I'm allowed to introduce other bugs, for example. >> >>> Further, >>> the optimizer will happily transform your program from one that >>> behaves one way to a different program, and cause the entire Racket >>> runtime to segfault. So if we went the route that you're suggesting, >>> Typed Racket m
Re: [racket-dev] math collection [was: Hyperbolic functions]
FWIW, I agree with Robby and have had similar conversations with Sam in person. (Although for me it is that I wish I had the ability to claim that macro pieces had certain types regardless of what TR could infer from the generated code.) I think a big part of the Racket philosophy is that the programming language implementer is not a member of an elite, enlightened caste that can make choices mere mortals cannot. This philosophy is the root of what I find beautiful about macros, continuations, first-class synchronization, and structure type properties, for example. Although I am not directly writing anything for the TR implementation, I have opinions about the goal of that project. To me, it is not "figure out a type system that is passable for Racket programs" but "make a type system that is to existing type systems as Racket is to pedestrian languages" in particularly, by allowing more extensions (type or otherwise) to be done in language. I see Robby's point about contract / type isomorphism and mine about more powerful type macros as steps in that direction. <3 Jay On Tue, Jun 26, 2012 at 10:10 PM, Robby Findler wrote: > Consider me done! > > Robby > > On Tue, Jun 26, 2012 at 11:05 PM, Neil Toronto wrote: >> I haven't got a clue what you two are arguing about anymore. If you both >> stop, maybe Sam can implement that perfectly safe change to the typed -> >> untyped contract barrier that he said he could do. That would be nice. >> >> ;) >> >> Neil ⊥ >> >> >> On 06/26/2012 09:23 PM, Robby Findler wrote: >>> >>> On Tue, Jun 26, 2012 at 10:08 PM, Sam Tobin-Hochstadt >>> wrote: On Tue, Jun 26, 2012 at 10:44 PM, Robby Findler wrote: > > On Tue, Jun 26, 2012 at 9:25 PM, Sam Tobin-Hochstadt > wrote: >> >> On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler >> wrote: >>> >>> This sounds like a terrible solution. >>> >>> There are lots of places in our system where we just declare facts and >>> don't prove them and then use them for lots of things (often >>> optimizations). Why should this one be special? >> >> >> I don't know of any places like this in Racket. What are you thinking >> of? > > > The inliner and the JIT compiler and that whole interaction are the > ones I thought of. I should have said "lots of facts" not "lots of > places", tho. Sorry about that. I'm still not sure what you're thinking of. What operation does the inliner or JIT perform that is justified by a programmer-declared-but-not-checked fact? >>> >>> >>> There are many operations that are implemented partially in JIT and >>> wholly in the runtime system. The JIT generated version gets used >>> unless certain conditions hold, in which case the runtime system >>> version gets used. The programmer declared fact is embedded into the >>> code and not specified as a fact per se, but for example, there is one >>> such fact saying "this pile of assembly instructions is equivalent to >>> the C implementation of list-ref, under the condition that the number >>> argument is a fixnum less than 10,000 and we don't run out of pairs >>> too soon" (roughly). There are large pile of such things. Another one >>> you're probably more familiar with: "this pile of assembly >>> instructions is equivalent to + when the arguments are both fixnums or >>> both flonums". >>> >>> There is another pile of such invariants in the (pre-bytecode level) >>> inliner. It relies on beta substitution and the ability to run certain >>> primitives at compile time. (I don't know as much about that one, so >>> probably there are more things it relies on than that.) >>> >> Certainly, Typed Racket is intended to be sound in the same sense that >> Racket is safe, and that Haskell, OCaml, and Java are safe as well: if >> you don't use specifically-marked unsafe features (such as the FFI and >> `racket/unsafe/ops`), then you get a guarantee that depends only on >> the correctness of the runtime system/compiler, not on the correctness >> of any user code. > > > Of course I understand this. I'm pointing out that this is not a > significant guarantee, in and of itself (see last para below for an > elaboration here). > >> I think this a very important guarantee: we've seen >> far too often that trusting user code in languages like C and C++ was >> a big mistake in many contexts. > > > I don't think this is an either/or. Indeed, just to continue with C: > if everyone understood that the types were really just size markers > and nothing else, then lots of the seeming unsoundness goes away in C > (not all, of course, and as I've been learning from Regehr's blog, > there are lots of other dark corners). But no one is suggesting we > remove checks from array bounds, which is what really cost society > money wrt to C and, IMO, the kind of invariant that matters.
Re: [racket-dev] math collection [was: Hyperbolic functions]
I found your message strange and I contemplated whether I should reply on 'dev' at all. In the interest of sharing and evolving the Racket idea, I am going with a response on 'dev'. Your central claim is that "the programming language implementer is not a member of an elite, enlightened caste that can make choices mere mortals cannot." Without any constraint this claim is plain wrong (like many general claims). You simply do not want every programmer to plug code into the JIT easily. You do not want #%plaiin-module-begin change meaning on you. You do not want to specify types so that the compiler randomly mangles bits for you and claims that they are the result. You can see that this is wrong with all the security that Matthew carefully adds to the implementation (not to speak of the design idea, which is abstract anyway). If we didn't want to restrict access to certain pieces in certain ways, why bother with inspectors and armed syntax and generative structs for basic forms. Why not allow (closure-environment (lambda (x) x)) to expose the pointer to the environment? (Which you can do in MIT Scheme, though there is called cadr.) I think the closest we have come to your claim is that we wish to push back the boundaries without giving up safety and security. Finding this middle ground of a high degree of expressivity with good constraints imposed on it is the purpose Racket and PLT. And we have done really well with it for a long time -- Matthias On Jun 27, 2012, at 2:12 PM, Jay McCarthy wrote: > FWIW, I agree with Robby and have had similar conversations with Sam > in person. (Although for me it is that I wish I had the ability to > claim that macro pieces had certain types regardless of what TR could > infer from the generated code.) > > I think a big part of the Racket philosophy is that the programming > language implementer is not a member of an elite, enlightened caste > that can make choices mere mortals cannot. This philosophy is the root > of what I find beautiful about macros, continuations, first-class > synchronization, and structure type properties, for example. > > Although I am not directly writing anything for the TR implementation, > I have opinions about the goal of that project. To me, it is not > "figure out a type system that is passable for Racket programs" but > "make a type system that is to existing type systems as Racket is to > pedestrian languages" in particularly, by allowing more > extensions (type or otherwise) to be done in language. > > I see Robby's point about contract / type isomorphism and mine about > more powerful type macros as steps in that direction. > > <3 > > Jay > > On Tue, Jun 26, 2012 at 10:10 PM, Robby Findler > wrote: >> Consider me done! >> >> Robby >> >> On Tue, Jun 26, 2012 at 11:05 PM, Neil Toronto >> wrote: >>> I haven't got a clue what you two are arguing about anymore. If you both >>> stop, maybe Sam can implement that perfectly safe change to the typed -> >>> untyped contract barrier that he said he could do. That would be nice. >>> >>> ;) >>> >>> Neil ⊥ >>> >>> >>> On 06/26/2012 09:23 PM, Robby Findler wrote: On Tue, Jun 26, 2012 at 10:08 PM, Sam Tobin-Hochstadt wrote: > > On Tue, Jun 26, 2012 at 10:44 PM, Robby Findler > wrote: >> >> On Tue, Jun 26, 2012 at 9:25 PM, Sam Tobin-Hochstadt >> wrote: >>> >>> On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler >>> wrote: This sounds like a terrible solution. There are lots of places in our system where we just declare facts and don't prove them and then use them for lots of things (often optimizations). Why should this one be special? >>> >>> >>> I don't know of any places like this in Racket. What are you thinking >>> of? >> >> >> The inliner and the JIT compiler and that whole interaction are the >> ones I thought of. I should have said "lots of facts" not "lots of >> places", tho. Sorry about that. > > > I'm still not sure what you're thinking of. What operation does the > inliner or JIT perform that is justified by a > programmer-declared-but-not-checked fact? There are many operations that are implemented partially in JIT and wholly in the runtime system. The JIT generated version gets used unless certain conditions hold, in which case the runtime system version gets used. The programmer declared fact is embedded into the code and not specified as a fact per se, but for example, there is one such fact saying "this pile of assembly instructions is equivalent to the C implementation of list-ref, under the condition that the number argument is a fixnum less than 10,000 and we don't run out of pairs too soon" (roughly). There are large pile of such things. Another one you're probably more familiar with: "this pile o
Re: [racket-dev] math collection [was: Hyperbolic functions]
Thanks for your correction. I think we're saying the same thing. Although I think that the safety we claim to have isn't really there with unsafe ops and the FFI. I can copy the definition of a closure out of the C headers into an FFI struct, cast the _racket pointer to a _closure-pointer, and read out the values. Here's an example: #lang racket/base (require ffi/unsafe rackunit) (define-values (one two f) (let () (define one (cons 1 null)) (define two (cons 2 null)) (values one two (λ (x) (cons x one) (check-equal? (f 1) (list 1 1)) (ptr-set! (cast f _racket _pointer) _intptr 2 (cast two _racket _intptr)) (check-equal? (f 2) (list 2 2)) This is something where it is normal to say we can ignore it, because no one would really do that. But on the other hand, the Arc uses a very similar thing to make conses mutable again (implemented for them by Eli.) I see the connection between types and contracts to be at a similar level to the FFI/unsafe. I don't think everyone should do it, but I think it should be "easy" to opt-in to such a connection. I also would like to see a macro-like compiler extension API for hooking into optimizations and different specialized JITing. Things like that are a very effective use of template meta-programming in C++ that I think we could do better. I think your restatement of my claim is excellent, that we have done a great job so far, and we should continue doing a great job. Jay On Thu, Jun 28, 2012 at 9:50 AM, Matthias Felleisen wrote: > > I found your message strange and I contemplated whether I should reply on > 'dev' at all. > > In the interest of sharing and evolving the Racket idea, I am going with a > response on 'dev'. Your central claim is that "the programming language > implementer is not a member of an elite, enlightened caste that can make > choices mere mortals cannot." Without any constraint this claim is plain > wrong (like many general claims). You simply do not want every programmer to > plug code into the JIT easily. You do not want #%plaiin-module-begin change > meaning on you. You do not want to specify types so that the compiler > randomly mangles bits for you and claims that they are the result. You can > see that this is wrong with all the security that Matthew carefully adds to > the implementation (not to speak of the design idea, which is abstract > anyway). If we didn't want to restrict access to certain pieces in certain > ways, why bother with inspectors and armed syntax and generative structs for > basic forms. Why not allow (closure-environment (lambda (x) x)) to expose the > pointer to the environment? (Which you can do in MIT Scheme, though there is > called cadr.) > > I think the closest we have come to your claim is that > > we wish to push back the boundaries without giving up safety and security. > > Finding this middle ground of a high degree of expressivity with good > constraints imposed on it is the purpose Racket and PLT. And we have done > really well with it for a long time > > -- Matthias > > > > > > > > > On Jun 27, 2012, at 2:12 PM, Jay McCarthy wrote: > >> FWIW, I agree with Robby and have had similar conversations with Sam >> in person. (Although for me it is that I wish I had the ability to >> claim that macro pieces had certain types regardless of what TR could >> infer from the generated code.) >> >> I think a big part of the Racket philosophy is that the programming >> language implementer is not a member of an elite, enlightened caste >> that can make choices mere mortals cannot. This philosophy is the root >> of what I find beautiful about macros, continuations, first-class >> synchronization, and structure type properties, for example. >> >> Although I am not directly writing anything for the TR implementation, >> I have opinions about the goal of that project. To me, it is not >> "figure out a type system that is passable for Racket programs" but >> "make a type system that is to existing type systems as Racket is to >> pedestrian languages" in particularly, by allowing more >> extensions (type or otherwise) to be done in language. >> >> I see Robby's point about contract / type isomorphism and mine about >> more powerful type macros as steps in that direction. >> >> <3 >> >> Jay >> >> On Tue, Jun 26, 2012 at 10:10 PM, Robby Findler >> wrote: >>> Consider me done! >>> >>> Robby >>> >>> On Tue, Jun 26, 2012 at 11:05 PM, Neil Toronto >>> wrote: I haven't got a clue what you two are arguing about anymore. If you both stop, maybe Sam can implement that perfectly safe change to the typed -> untyped contract barrier that he said he could do. That would be nice. ;) Neil ⊥ On 06/26/2012 09:23 PM, Robby Findler wrote: > > On Tue, Jun 26, 2012 at 10:08 PM, Sam Tobin-Hochstadt > wrote: >> >> On Tue, Jun 26, 2012 at 10:44 PM, Robby Findler >> wrote: >>> >>> On Tue,
Re: [racket-dev] math collection [was: Hyperbolic functions]
On Thu, Jun 28, 2012 at 10:21 AM, Jay McCarthy wrote: > I also would like to see a macro-like compiler extension API for > hooking into optimizations and different specialized JITing. Things > like that are a very effective use of template meta-programming in C++ > that I think we could do better. We also have something very similar to this already that lets you drop in ASM implemented functions generated from with Racket: https://github.com/noelwelsh/assembler/blob/master/test.ss Jay -- Jay McCarthy Assistant Professor / Brigham Young University http://faculty.cs.byu.edu/~jay "The glory of God is Intelligence" - D&C 93 _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
One more comment (even tho I promised not (and even worse this is a kind of repetition)): I think it is easy to fall into the trap of thinking "well, I want to limit access to this because I know that X writes this code and thus can I can be sure that things work"; we should really be thinking about technical ways to ensure that things work, instead of relying on "smart" people. (One look at the correlation between good developer and number of open bugs suggests that even if we wanted to rely only on good developers, we'd be in trouble.) I think we also already do a lot of work in this sense and this is not, generally speaking, an easy set of problems, but I think it is a set where we can offer something and so we should be seeking out such places, opening them up to anyone and putting _technical_ barriers in place (when possible) to keep our invariants preserved. In the specific example that started this thread, I think that trying something like random testing can be an effective way to make sure that contracts and types match up. For example. Robby On Thu, Jun 28, 2012 at 11:21 AM, Jay McCarthy wrote: > Thanks for your correction. I think we're saying the same thing. > > Although I think that the safety we claim to have isn't really there > with unsafe ops and the FFI. I can copy the definition of a closure > out of the C headers into an FFI struct, cast the _racket pointer to a > _closure-pointer, and read out the values. > > Here's an example: > > #lang racket/base > (require ffi/unsafe > rackunit) > > (define-values (one two f) > (let () > (define one (cons 1 null)) > (define two (cons 2 null)) > (values one two > (λ (x) (cons x one) > > (check-equal? (f 1) (list 1 1)) > > (ptr-set! (cast f _racket _pointer) _intptr 2 > (cast two _racket _intptr)) > > (check-equal? (f 2) (list 2 2)) > > This is something where it is normal to say we can ignore it, because > no one would really do that. But on the other hand, the Arc uses a > very similar thing to make conses mutable again (implemented for them > by Eli.) > > I see the connection between types and contracts to be at a similar > level to the FFI/unsafe. I don't think everyone should do it, but I > think it should be "easy" to opt-in to such a connection. > > I also would like to see a macro-like compiler extension API for > hooking into optimizations and different specialized JITing. Things > like that are a very effective use of template meta-programming in C++ > that I think we could do better. > > I think your restatement of my claim is excellent, that we have done a > great job so far, and we should continue doing a great job. > > Jay > > On Thu, Jun 28, 2012 at 9:50 AM, Matthias Felleisen > wrote: >> >> I found your message strange and I contemplated whether I should reply on >> 'dev' at all. >> >> In the interest of sharing and evolving the Racket idea, I am going with a >> response on 'dev'. Your central claim is that "the programming language >> implementer is not a member of an elite, enlightened caste that can make >> choices mere mortals cannot." Without any constraint this claim is plain >> wrong (like many general claims). You simply do not want every programmer to >> plug code into the JIT easily. You do not want #%plaiin-module-begin change >> meaning on you. You do not want to specify types so that the compiler >> randomly mangles bits for you and claims that they are the result. You can >> see that this is wrong with all the security that Matthew carefully adds to >> the implementation (not to speak of the design idea, which is abstract >> anyway). If we didn't want to restrict access to certain pieces in certain >> ways, why bother with inspectors and armed syntax and generative structs for >> basic forms. Why not allow (closure-environment (lambda (x) x)) to expose >> the pointer to the environment? (Which you can do in MIT Scheme, though >> there is called cadr.) >> >> I think the closest we have come to your claim is that >> >> we wish to push back the boundaries without giving up safety and security. >> >> Finding this middle ground of a high degree of expressivity with good >> constraints imposed on it is the purpose Racket and PLT. And we have done >> really well with it for a long time >> >> -- Matthias >> >> >> >> >> >> >> >> >> On Jun 27, 2012, at 2:12 PM, Jay McCarthy wrote: >> >>> FWIW, I agree with Robby and have had similar conversations with Sam >>> in person. (Although for me it is that I wish I had the ability to >>> claim that macro pieces had certain types regardless of what TR could >>> infer from the generated code.) >>> >>> I think a big part of the Racket philosophy is that the programming >>> language implementer is not a member of an elite, enlightened caste >>> that can make choices mere mortals cannot. This philosophy is the root >>> of what I find beautiful about macros, continuations, first-class >>> synchronization, and structure type proper
Re: [racket-dev] math collection [was: Hyperbolic functions]
On 06/28/2012 01:52 PM, Robby Findler wrote: One more comment (even tho I promised not (and even worse this is a kind of repetition)): I think it is easy to fall into the trap of thinking "well, I want to limit access to this because I know that X writes this code and thus can I can be sure that things work"; we should really be thinking about technical ways to ensure that things work, instead of relying on "smart" people. (One look at the correlation between good developer and number of open bugs suggests that even if we wanted to rely only on good developers, we'd be in trouble.) I think we also already do a lot of work in this sense and this is not, generally speaking, an easy set of problems, but I think it is a set where we can offer something and so we should be seeking out such places, opening them up to anyone and putting _technical_ barriers in place (when possible) to keep our invariants preserved. In the specific example that started this thread, I think that trying something like random testing can be an effective way to make sure that contracts and types match up. For example. Okay, now I finally understand what all you guys are on about. Also, I think that's a great idea. Currently, randomized testing only tests *preservation* for numeric primitives, by ensuring that the type of an expression's value (as computed by `eval') is a subtype of the expression's type according to TR. In principle, the primitives' giant case-> types could be proved correct, but: 1) They would only be proved for an ideal implementation 2) It would still take too much friggin' work 3) Vincent would still have to *identify* the right types (theorems). Randomized testing 1) tests the actual implementation; 2) moves the work to the machine; and 3) can find counterexamples quickly to make identifying the right types easier. So... what I thought was a great idea was extending randomized testing to the contract boundary. Also, I just had an idea. Vincent, how hard would it be to use something like the current randomized testing to *search* for a more precise type? I'm thinking of an algorithm that iteratively 1) makes a type like (Real -> Real) more precise (e.g. (case -> (Float -> Float) (Real -> Real))), then 2) tests it on random inputs. It would backtrack if testing finds preservation counterexamples, and repeat until it can't refine the type anymore. Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
At Thu, 28 Jun 2012 14:24:04 -0600, Neil Toronto wrote: > Also, I just had an idea. Vincent, how hard would it be to use something > like the current randomized testing to *search* for a more precise type? > I'm thinking of an algorithm that iteratively 1) makes a type like (Real > -> Real) more precise (e.g. (case -> (Float -> Float) (Real -> Real))), > then 2) tests it on random inputs. It would backtrack if testing finds > preservation counterexamples, and repeat until it can't refine the type > anymore. Using random generation to find potential additions to existing types (then adding them manually) sounds interesting. I'm less comfortable with the idea of using random generation to generate types from scratch. A lot of numeric types have symmetries and/or patterns (e.g. behavior on `Byte', `Index' and `Nonnegative-Fixnum' usually follows the same patterns) that depend a lot on the specific operation. Random generation would likely generate irregular types, which would lead to inconsistent behavior across "similar" types. Vincent _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
On Jun 28, 2012, at 3:52 PM, Robby Findler wrote: > "well, I want to limit access to this because I know that X writes this code > and thus can I can be sure that things work This is of course a caricature of what I am saying, a strawman at best, and not worth discussing any further -- Matthias _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] math collection [was: Hyperbolic functions]
Sorry. On Thu, Jun 28, 2012 at 3:51 PM, Matthias Felleisen wrote: > > On Jun 28, 2012, at 3:52 PM, Robby Findler wrote: > >> "well, I want to limit access to this because I know that X writes this code >> and thus can I can be sure that things work > > This is of course a caricature of what I am saying, a strawman at best, and > not worth discussing any further -- Matthias > _ Racket Developers list: http://lists.racket-lang.org/dev
