Re: [racket-users] How to type annotate for bindings in complex syntax forms
On Mon, 06 Mar 2017 23:50:38 -0600,
lu wrote:
>
> Awesome. Thanks! Where can I find the documentation for this TR reader syntax?
>
> Why is TR not able to figure out the type for these variables without
> human help? Does that mean the implementation of `command-line` is in
> TR and the types of those variables are inferred by the type system,
> or they are explicitly typed to be `Any` for simplicity?
`command-line` is a syntactic extension, which gets expanded away before
TR checks types. Its expansion is unfortunately too complex for TR's
inference to handle, hence why it needs your help.
Vincent
> On Monday, March 6, 2017 at 2:48:15 PM UTC-8, Sam Tobin-Hochstadt wrote:
> > You can use the #{x : T} reader syntax to annotate variables in macros
> > like `command-line`. Here's a working version of your code:
> >
> > ```
> > #lang typed/racket
> >
> > (define *channel* (make-parameter "#general"))
> > (define *message* : (Parameterof (Listof String)) (make-parameter '()))
> >
> >
> > (define (parse-cmdline)
> > (command-line
> >#:program "q"
> >#:once-each
> >[("-c" "--channel") #{ch : String} "slack channel to post (default:
> > use .qrc setting or default)" (*channel* ch)]
> >#:args #{msg : String}
> >(*message* msg)))
> > ```
> >
> > On Mon, Mar 6, 2017 at 2:08 AM, kay <> wrote:
> > > For a complex syntax form like `command-line`, I have difficulty
> > > correctly annotate the bindings it defines.
> > >
> > > More specifically, in the below code, for variable `msg`, even the
> > > document[1] says the `#:args` binds as list of **strings**, but the error
> > > indicates that it somehow is declared as `Listof Any`.
> > >
> > > Similarly, for variable `ch` bound in line 11, I believe it should always
> > > be `String`, but it somehow is declared to be `Any`.
> > >
> > > What should I do with this type of error, if I want my varaibles to be
> > > more precisely typed than just `Any`?
> > >
> > >
> > > [1]:
> > > https://docs.racket-lang.org/reference/Command-Line_Parsing.html?q=command-line#%28form._%28%28lib._racket%2Fcmdline..rkt%29._command-line%29%29
> > >
> > > ```
> > > 1 #lang typed/racket
> > > 2
> > > 3 (define *channel* (make-parameter "#general"))
> > > 4 (define *message* : (Parameterof (Listof String)) (make-parameter
> > > '()))
> > > 5
> > > 6
> > > 7 (define (parse-cmdline)
> > > 8 (command-line
> > > 9 #:program "q"
> > > 10 #:once-each
> > > 11 [("-c" "--channel") ch "slack channel to post (default: use
> > > .qrc setting or default)" (*channel* ch)]
> > > 12 #:args msg
> > > 13 (*message* msg)))
> > > 14
> > > 15
> > > 16 #|
> > > 17 tr.rkt:11:91: Type Checker: Wrong argument to parameter -
> > > expected String and got Any in: (*channel* ch)
> > > 18 tr.rkt:13:5: Type Checker: Wrong argument to parameter - expected
> > > (Listof String) and got (Listof Any) in: (*message* msg)
> > > 19 |#
> > > ```
> > >
> > > --
> > > You received this message because you are subscribed to the Google Groups
> > > "Racket Users" group.
> > > To unsubscribe from this group and stop receiving emails from it, send an
> > > email to racket-users+unsubscr...@googlegroups.com.
> > > For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] How to type annotate for bindings in complex syntax forms
Ah I found documentation for `#{ x : ... }` at here[1].
[1]:
https://docs.racket-lang.org/ts-guide/more.html#%28part._.Annotating_.Single_.Variables%29
On Monday, March 6, 2017 at 9:50:39 PM UTC-8, lu wrote:
> Awesome. Thanks! Where can I find the documentation for this TR reader syntax?
>
> Why is TR not able to figure out the type for these variables without human
> help? Does that mean the implementation of `command-line` is in TR and the
> types of those variables are inferred by the type system, or they are
> explicitly typed to be `Any` for simplicity?
>
>
> On Monday, March 6, 2017 at 2:48:15 PM UTC-8, Sam Tobin-Hochstadt wrote:
> > You can use the #{x : T} reader syntax to annotate variables in macros
> > like `command-line`. Here's a working version of your code:
> >
> > ```
> > #lang typed/racket
> >
> > (define *channel* (make-parameter "#general"))
> > (define *message* : (Parameterof (Listof String)) (make-parameter '()))
> >
> >
> > (define (parse-cmdline)
> > (command-line
> >#:program "q"
> >#:once-each
> >[("-c" "--channel") #{ch : String} "slack channel to post (default:
> > use .qrc setting or default)" (*channel* ch)]
> >#:args #{msg : String}
> >(*message* msg)))
> > ```
> >
> > On Mon, Mar 6, 2017 at 2:08 AM, kay <> wrote:
> > > For a complex syntax form like `command-line`, I have difficulty
> > > correctly annotate the bindings it defines.
> > >
> > > More specifically, in the below code, for variable `msg`, even the
> > > document[1] says the `#:args` binds as list of **strings**, but the error
> > > indicates that it somehow is declared as `Listof Any`.
> > >
> > > Similarly, for variable `ch` bound in line 11, I believe it should always
> > > be `String`, but it somehow is declared to be `Any`.
> > >
> > > What should I do with this type of error, if I want my varaibles to be
> > > more precisely typed than just `Any`?
> > >
> > >
> > > [1]:
> > > https://docs.racket-lang.org/reference/Command-Line_Parsing.html?q=command-line#%28form._%28%28lib._racket%2Fcmdline..rkt%29._command-line%29%29
> > >
> > > ```
> > > 1 #lang typed/racket
> > > 2
> > > 3 (define *channel* (make-parameter "#general"))
> > > 4 (define *message* : (Parameterof (Listof String)) (make-parameter
> > > '()))
> > > 5
> > > 6
> > > 7 (define (parse-cmdline)
> > > 8 (command-line
> > > 9 #:program "q"
> > > 10 #:once-each
> > > 11 [("-c" "--channel") ch "slack channel to post (default: use
> > > .qrc setting or default)" (*channel* ch)]
> > > 12 #:args msg
> > > 13 (*message* msg)))
> > > 14
> > > 15
> > > 16 #|
> > > 17 tr.rkt:11:91: Type Checker: Wrong argument to parameter -
> > > expected String and got Any in: (*channel* ch)
> > > 18 tr.rkt:13:5: Type Checker: Wrong argument to parameter - expected
> > > (Listof String) and got (Listof Any) in: (*message* msg)
> > > 19 |#
> > > ```
> > >
> > > --
> > > You received this message because you are subscribed to the Google Groups
> > > "Racket Users" group.
> > > To unsubscribe from this group and stop receiving emails from it, send an
> > > email to racket-users+unsubscr...@googlegroups.com.
> > > For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] How to type annotate for bindings in complex syntax forms
Awesome. Thanks! Where can I find the documentation for this TR reader syntax?
Why is TR not able to figure out the type for these variables without human
help? Does that mean the implementation of `command-line` is in TR and the
types of those variables are inferred by the type system, or they are
explicitly typed to be `Any` for simplicity?
On Monday, March 6, 2017 at 2:48:15 PM UTC-8, Sam Tobin-Hochstadt wrote:
> You can use the #{x : T} reader syntax to annotate variables in macros
> like `command-line`. Here's a working version of your code:
>
> ```
> #lang typed/racket
>
> (define *channel* (make-parameter "#general"))
> (define *message* : (Parameterof (Listof String)) (make-parameter '()))
>
>
> (define (parse-cmdline)
> (command-line
>#:program "q"
>#:once-each
>[("-c" "--channel") #{ch : String} "slack channel to post (default:
> use .qrc setting or default)" (*channel* ch)]
>#:args #{msg : String}
>(*message* msg)))
> ```
>
> On Mon, Mar 6, 2017 at 2:08 AM, kay <> wrote:
> > For a complex syntax form like `command-line`, I have difficulty correctly
> > annotate the bindings it defines.
> >
> > More specifically, in the below code, for variable `msg`, even the
> > document[1] says the `#:args` binds as list of **strings**, but the error
> > indicates that it somehow is declared as `Listof Any`.
> >
> > Similarly, for variable `ch` bound in line 11, I believe it should always
> > be `String`, but it somehow is declared to be `Any`.
> >
> > What should I do with this type of error, if I want my varaibles to be more
> > precisely typed than just `Any`?
> >
> >
> > [1]:
> > https://docs.racket-lang.org/reference/Command-Line_Parsing.html?q=command-line#%28form._%28%28lib._racket%2Fcmdline..rkt%29._command-line%29%29
> >
> > ```
> > 1 #lang typed/racket
> > 2
> > 3 (define *channel* (make-parameter "#general"))
> > 4 (define *message* : (Parameterof (Listof String)) (make-parameter
> > '()))
> > 5
> > 6
> > 7 (define (parse-cmdline)
> > 8 (command-line
> > 9 #:program "q"
> > 10 #:once-each
> > 11 [("-c" "--channel") ch "slack channel to post (default: use
> > .qrc setting or default)" (*channel* ch)]
> > 12 #:args msg
> > 13 (*message* msg)))
> > 14
> > 15
> > 16 #|
> > 17 tr.rkt:11:91: Type Checker: Wrong argument to parameter - expected
> > String and got Any in: (*channel* ch)
> > 18 tr.rkt:13:5: Type Checker: Wrong argument to parameter - expected
> > (Listof String) and got (Listof Any) in: (*message* msg)
> > 19 |#
> > ```
> >
> > --
> > You received this message because you are subscribed to the Google Groups
> > "Racket Users" group.
> > To unsubscribe from this group and stop receiving emails from it, send an
> > email to racket-users+unsubscr...@googlegroups.com.
> > For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] How to type annotate for bindings in complex syntax forms
You can use the #{x : T} reader syntax to annotate variables in macros
like `command-line`. Here's a working version of your code:
```
#lang typed/racket
(define *channel* (make-parameter "#general"))
(define *message* : (Parameterof (Listof String)) (make-parameter '()))
(define (parse-cmdline)
(command-line
#:program "q"
#:once-each
[("-c" "--channel") #{ch : String} "slack channel to post (default:
use .qrc setting or default)" (*channel* ch)]
#:args #{msg : String}
(*message* msg)))
```
On Mon, Mar 6, 2017 at 2:08 AM, kay wrote:
> For a complex syntax form like `command-line`, I have difficulty correctly
> annotate the bindings it defines.
>
> More specifically, in the below code, for variable `msg`, even the
> document[1] says the `#:args` binds as list of **strings**, but the error
> indicates that it somehow is declared as `Listof Any`.
>
> Similarly, for variable `ch` bound in line 11, I believe it should always be
> `String`, but it somehow is declared to be `Any`.
>
> What should I do with this type of error, if I want my varaibles to be more
> precisely typed than just `Any`?
>
>
> [1]:
> https://docs.racket-lang.org/reference/Command-Line_Parsing.html?q=command-line#%28form._%28%28lib._racket%2Fcmdline..rkt%29._command-line%29%29
>
> ```
> 1 #lang typed/racket
> 2
> 3 (define *channel* (make-parameter "#general"))
> 4 (define *message* : (Parameterof (Listof String)) (make-parameter
> '()))
> 5
> 6
> 7 (define (parse-cmdline)
> 8 (command-line
> 9 #:program "q"
> 10 #:once-each
> 11 [("-c" "--channel") ch "slack channel to post (default: use .qrc
> setting or default)" (*channel* ch)]
> 12 #:args msg
> 13 (*message* msg)))
> 14
> 15
> 16 #|
> 17 tr.rkt:11:91: Type Checker: Wrong argument to parameter - expected
> String and got Any in: (*channel* ch)
> 18 tr.rkt:13:5: Type Checker: Wrong argument to parameter - expected
> (Listof String) and got (Listof Any) in: (*message* msg)
> 19 |#
> ```
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Re: [racket-users] How to type annotate for bindings in complex syntax forms
1.5 years ago, I struggled with the command-line, finally I thought
`parse-command-line` is friendlier than its macro form `command-line`, and
got the solution with `cast`:
;;; firstly, define your precise Help-Table.
(define-type Help-Table
(Listof (U (Pairof 'usage-help String)
(Pairof 'once-each (Listof (List (Listof String)
(U (->
String String Void)
(->
String Void))
(Listof
String)))
((cast parse-command-line (-> String (Vectorof String) Help-Table (-> Any
Void) (Listof String) (-> String Void) Void))
(format "~a ~a" (#%module) (path-replace-suffix (cast
(file-name-from-path (#%file)) Path) #""))
(current-command-line-arguments)
`([usage-help . ,(format "~a~n" desc)]
[once-each [("-p") ,(λ [[_ : String] [port : String]] (sakuyamon-port
(cast (string->number port) (Option Index
("Use an alternative ." "port")]
[("-w") ,(λ [[_ : String] [mw : String]]
(sakuyamon-max-waiting (cast (string->number mw) Positive-Index)))
("Maximum number of clients can be waiting for
acceptance." "mw")]
[("-t") ,(λ [[_ : String] [ict : String]]
(sakuyamon-connection-timeout (cast (string->number ict) Positive-Index)))
("Initial connection timeout." "ict")]
[("--SSL") ,(λ [[_ : String]] (sakuyamon-ssl? #true))
("Enable SSL with 443 as default port.")]])
(λ [!] (serve-forever))
null
(lambda [[-h : String]]
(display (string-replace -h #px" -- : .+?-h --'\\s*" ""))
(exit 0)))
at that time, I was a freshman to typed racket, hence so many `cast` in the
solution. The `cast` form is inefficient, but in that situation it's
ignorable.
The other reason was, the annotation of `parse-command-line` lacks the 6th
optional argument which I always need to filter the help message.
Yes, it's ugly, but better than losing the type information of important
parts.
Engineering is the art of tradeoffs.
On Mon, Mar 6, 2017 at 3:08 PM, kay wrote:
> For a complex syntax form like `command-line`, I have difficulty correctly
> annotate the bindings it defines.
>
> More specifically, in the below code, for variable `msg`, even the
> document[1] says the `#:args` binds as list of **strings**, but the error
> indicates that it somehow is declared as `Listof Any`.
>
> Similarly, for variable `ch` bound in line 11, I believe it should always
> be `String`, but it somehow is declared to be `Any`.
>
> What should I do with this type of error, if I want my varaibles to be
> more precisely typed than just `Any`?
>
>
> [1]: https://docs.racket-lang.org/reference/Command-Line_
> Parsing.html?q=command-line#%28form._%28%28lib._racket%
> 2Fcmdline..rkt%29._command-line%29%29
>
> ```
> 1 #lang typed/racket
> 2
> 3 (define *channel* (make-parameter "#general"))
> 4 (define *message* : (Parameterof (Listof String)) (make-parameter
> '()))
> 5
> 6
> 7 (define (parse-cmdline)
> 8 (command-line
> 9 #:program "q"
> 10 #:once-each
> 11 [("-c" "--channel") ch "slack channel to post (default: use
> .qrc setting or default)" (*channel* ch)]
> 12 #:args msg
> 13 (*message* msg)))
> 14
> 15
> 16 #|
> 17 tr.rkt:11:91: Type Checker: Wrong argument to parameter - expected
> String and got Any in: (*channel* ch)
> 18 tr.rkt:13:5: Type Checker: Wrong argument to parameter - expected
> (Listof String) and got (Listof Any) in: (*message* msg)
> 19 |#
> ```
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
[racket-users] How to type annotate for bindings in complex syntax forms
For a complex syntax form like `command-line`, I have difficulty correctly
annotate the bindings it defines.
More specifically, in the below code, for variable `msg`, even the document[1]
says the `#:args` binds as list of **strings**, but the error indicates that it
somehow is declared as `Listof Any`.
Similarly, for variable `ch` bound in line 11, I believe it should always be
`String`, but it somehow is declared to be `Any`.
What should I do with this type of error, if I want my varaibles to be more
precisely typed than just `Any`?
[1]:
https://docs.racket-lang.org/reference/Command-Line_Parsing.html?q=command-line#%28form._%28%28lib._racket%2Fcmdline..rkt%29._command-line%29%29
```
1 #lang typed/racket
2
3 (define *channel* (make-parameter "#general"))
4 (define *message* : (Parameterof (Listof String)) (make-parameter '()))
5
6
7 (define (parse-cmdline)
8 (command-line
9 #:program "q"
10 #:once-each
11 [("-c" "--channel") ch "slack channel to post (default: use .qrc
setting or default)" (*channel* ch)]
12 #:args msg
13 (*message* msg)))
14
15
16 #|
17 tr.rkt:11:91: Type Checker: Wrong argument to parameter - expected
String and got Any in: (*channel* ch)
18 tr.rkt:13:5: Type Checker: Wrong argument to parameter - expected
(Listof String) and got (Listof Any) in: (*message* msg)
19 |#
```
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
