[racket] Typed racket problem

On Sun, 30 Nov 2014 09:25:57 -0500
Sam Tobin-Hochstadt <samth at cs.indiana.edu>
wrote:

> I think this is exactly what you need. You could write (< (assert s
> integer?) 0) or (and s (integer? s) (< s 0)), which mostly do the same
> thing.
> 
> But the fundamental issue is that this program is well-typed:
> 
>     (process (list (cons 'size "hi")))
> 
> since that's a perfectly valid `OptList`. If you didn't have a dynamic
> check in `process`, you'd end up with (< "hi" 0) which is wrong.
> 
> If that's not what you want, what should the restrictions on
> `OptList` be?
> 

In my real program I have an OptList with 15 options or so, all known
at compile time. Don't know if this helps to make it simpler.

Actually, I had hoped to be able to put the cast into the optval
procedure but I wasn't successful in doing this. 

Or factoring it out in some way so that I do not need to write the cast
or assert? each time I use an option.

I played a bit and found this:


(define-syntax-rule (optval v ol)
   (let ([vv (_optval v ol)])
     (case v
       ['size  (cast vv Integer)]
       ['dir   (cast vv String)]
       ['verbose (cast vv Boolean)]
       [else (error "bad option")])))

by renaming previous optval to _optval. This works fine but I have two
questions:

1. You offered assert? as an alternative. Is this preferable in
comparison to cast?

2. My solution seems to be bad because the decision about the type
happens at runtime. 

It would be better I could redefine optval in a way that this will be
done at compile time as I always call optval with an explicit option
symbol.  

Is this possible? I'm afraid y knowledge about define-syntax-rule isn't
really good.


Thanks.


-- 
Manfred





> Sam
> 
> 
> 
> On Sun, Nov 30, 2014 at 8:46 AM, Manfred Lotz
> <manfred.lotz at arcor.de> wrote:
> > Well, I should have added that I've found this:
> >
> > (: process (-> OptList Void))
> > (define (process ol)
> >   (let ([s (optval 'size ol)])
> >     (if (and s (<  (cast s Integer) 0))
> >         (displayln "wrong value")
> >         (displayln "ok")))
> >     )
> >
> >
> > but I didn't find this really nice. Actually, I was hoping for
> > something more concise.
> >
> > --
> > Manfred
> >
> >
> > On Sun, 30 Nov 2014 10:13:48 +0100
> > Manfred Lotz <manfred.lotz at arcor.de> wrote:
> >
> >> Hi there,
> >> I've got another problem with typed racket.
> >>
> >> Let us say I have an assoc list with options for a program. These
> >> options could be of type String, Boolean, or Integer.
> >>
> >> Now in my program I want to check certain options but I don't know
> >> how to do without Typed Racket screaming at me.
> >>
> >> Here a minimal example:
> >>
> >> #lang typed/racket
> >>
> >> (define-type Myopt (U String Boolean Integer))
> >> (define-type OptList (Listof (Pairof Symbol Myopt)))
> >>
> >>
> >> (: olist OptList)
> >> (define olist (list '(dir . ".")
> >>                     '(verbose . #t)
> >>                     '(size . 12)))
> >>
> >> (: optval (-> Symbol OptList Myopt))
> >> (define (optval v ol)
> >>   (let ([val (assoc v ol)])
> >>     (if val
> >>       (cdr val)
> >>       (error "Unexpected option encountered"))))
> >>
> >> (: process (-> OptList Void))
> >> (define (process ol)
> >>   (if (<  (optval 'size ol) 0)
> >>       (displayln "wrong value")
> >>       (displayln "ok")))
> >>
> >>
> >> I get an error:
> >> Type Checker: type mismatch
> >>   expected: Real
> >>   given: Myopt
> >>   in: (optval (quote size) ol)
> >>
> >>
> >> How could I solve this?
> >>
> >>
> >
> >
> >
> > ____________________
> >   Racket Users list:
> >   http://lists.racket-lang.org/users
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>