[racket] Typed Racket: Command-line parsing problems

The type error is real and predicts a potential bug in your code. 

First, here is how to fix it: 

#lang typed/racket

(define: mystringlistlist : (Listof (cons String (Listof String))) (list (list "a" "b") (list "c" "d")))

(define: mystringpairlist : (Listof (Pairof String String)) (list (cons "a" "b") (cons "c" "d")))

; Works!
(assoc "a" mystringpairlist)

;; Works like a charm: 
(assoc "a" mystringlistlist)

Second, here is why your code is potentially buggy. Suppose you used the type of your mystringlistlist as an argument type to f. You could then apply f to '( () ), which is a list of list of strings. If this argument flows to assoc, you violate the primitives basic constraint, namely, that each item on the list consists of at least one cons cell. By saying (cons String (Listof String)) you are saying list of non-empty list of strings, which fits the assoc type signature fine. 

Third, the reason your code doesn't have a run-time error -- i.e. the type error is conservative and the 'potential' is needed -- is because your specific list consists of non-empty lists of strings. Even though TR can infer this type, your type assignment to this identifier overrides TR's capabilities. 

-- Matthias







On Jun 24, 2013, at 4:40 AM, Tim K. wrote:

> Sam Tobin-Hochstadt <samth at ...> writes:
> 
>> Can you say more about the problem here?  The type of `assoc` mentions
>> pairs, but you should be able to use it with lists, since they're made
>> of pairs.
> 
> Yeah, that's what I had expected as well. This code produces type errors (in
> 5.3.3, too):
> 
>    ;; Definitions
>    (define: mystringlistlist : (Listof (Listof String)) (list (list "a"
> "b") (list "c" "d")))
>    (define: mystringpairlist : (Listof (Pairof String String)) (list (cons
> "a" "b") (cons "c" "d")))
> 
>    ; Works!
>    (assoc "a" mystringpairlist)
>    => '("a" . "b")
> 
>    ; Type error
>    (assoc "a" mystringlistlist)
> 
>    Type Checker: Polymorphic function assoc could not be applied to arguments:
>    Argument 1:
>      Expected: a
>      Given:    String
>    Argument 2:
>      Expected: (Listof (Pairof a b))
>      Given:    (Listof (Listof String))
>     in: (assoc "a" mystringlistlist)
> 
> 
> I thought that Racket maybe didn't accept "a" as a String, so I defined it
> as one and called assoc with that, but the error is exactly the same.
> 
> 
> 
>> Here's a version that type checks: https://gist.github.com/samth/5847063
>> 
>> The key is giving a type annotation to `fname` using the #{} syntax.
>> Typed Racket can figure out how to typecheck the expansion only if you
>> give it that hint.  And the #{} syntax is for adding such hints with
>> macros like `command-line` that didn't anticipate Typed Racket.
> 
> Ah, that works, thank you :)
> Did I not see that in the documentation or is this feature "experimental"?
> 
> 
> Best Regards,
> Tim
> 
> 
> 
> 
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users