headers
Matthias Felleisen | 28 Jun 2012 17:50
Favicon

Re: 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.)
(Continue reading)

Permalink | Reply |
headers
Jay McCarthy | 28 Jun 2012 18:21
Picon
Gravatar

Re: 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
(Continue reading)

Permalink | Reply |
headers
Jay McCarthy | 28 Jun 2012 19:56
Picon
Gravatar

Re: math collection [was: Hyperbolic functions]

On Thu, Jun 28, 2012 at 10:21 AM, Jay McCarthy
<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 <jay@...>
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
Permalink | Reply |
headers
Robby Findler | 28 Jun 2012 21:52
Gravatar

Re: 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 <jay.mccarthy <at> gmail.com> 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.
>
(Continue reading)

Permalink | Reply |
headers
Neil Toronto | 28 Jun 2012 22:24
Picon
Gravatar

Re: 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
(Continue reading)

Permalink | Reply |
headers
Vincent St-Amour | 28 Jun 2012 22:45
Favicon

Re: 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
Permalink | Reply |
headers
Matthias Felleisen | 28 Jun 2012 22:51
Favicon

Re: 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
Permalink | Reply |
headers
Robby Findler | 28 Jun 2012 22:59
Gravatar

Re: math collection [was: Hyperbolic functions]

Sorry.

On Thu, Jun 28, 2012 at 3:51 PM, Matthias Felleisen
<matthias@...> 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
Permalink | Reply |

Gmane