[racket] Typed racket problem

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