[racket] Typed racket problem

From: Manfred Lotz (manfred.lotz at arcor.de)
Date: Sun Nov 30 16:21:14 EST 2014

No I hadn't considered the variant using type?. Thanks for this. 

Not quite sure if I'm happy about it as I would prefer to have the type
checking at one place instead of providing a type each time I check/use
options.

-- 
Manfred





On Sun, 30 Nov 2014 14:36:26 -0500
Matthias Felleisen <matthias at ccs.neu.edu>
wrote:

> 
> Have you considered this: 
> 
> #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)))
> 
> ; This is a fake type, where the "filter" flows into the result 
> ; (: optval (-> Symbol OptList (-> Any Boolean : Type) Type))
> (define-syntax-rule
>   (optval v ol type?)
>   (let ([val (assoc v ol)])
>     (if (and val (type? (cdr val)))
>         (cdr val)
>         (error "Unexpected option encountered"))))
> 
> (: process (-> OptList Void))
> (define (process ol)
>   (define s (optval 'size ol integer?)) 
>   (if (<  s 0)
>       (displayln "wrong value")
>       (displayln "ok")))
> 
> (process olist)
> 
> 
> 
> On Nov 30, 2014, at 10:38 AM, Manfred Lotz wrote:
> 
> > 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
> >> 
> > 
> > 
> > 
> > ____________________
> >  Racket Users list:
> >  http://lists.racket-lang.org/users
> 
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
> 




Posted on the users mailing list.