[racket] Typed Racket: Command-line parsing problems

On Mon, Jun 24, 2013 at 8:21 AM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> On Jun 23, 2013, at 8:34 PM, Sam Tobin-Hochstadt wrote:
>
>>>
>>> After porting nearly everything I was left with typing up the command-line
>>> parser. However, I am getting a type error at the following simplified part:
>>
>> 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.
>
>
> I think this answer is not fair.
>
> Because
>
> On Jun 23, 2013, at 2:21 PM, Tim K. wrote:
>
>> I wonder, why does fname have the "Any" type? Yes, I didn't explicitly give
>> fname a type, but I was hoping that the typed version of "command-line"
>> would do that
>
> is correct. command-line in a typed context should know that what flows into
> its world is a string.

This could mean one of two things.  One is that `command-line` could
be treated specially in Typed Racket (or there's a
`typed/racket/command-line` library), so that it's like those
identifiers were already given the type `String`. This would be
technically challenging (without requiring the extra library), and is,
I think, a bad idea.  The other is that Typed Racket could improve its
inference, so that it can just tell that only `String` is possible
there.  This is my preferred solution, but it will require some
significant work on improving inference in Typed Racket that I don't
think will happen in the very near future.

Sam