While experimenting with porting an typed program to Typed Racket, I
encountered a few surprises. Some of these seem like they might be bugs,
others missing features, and several probably are misunderstandings on my
part.
*1. struct subtyping doesn't work with #:type-name*
The following program fails to typecheck with the error "Type Checker:
parent type not a valid structure name: animal":
#lang typed/racket
(struct animal ()
#:type-name Animal
#:transparent)
(struct dog animal ()
#:transparent)
Trying to use `Animal` as the parent of `dog` doesn't work either,
producing the expected error from `struct` that `Animal` is not bound to
struct type information.
*2. Problems with define-struct/exec*
There seem to be some subtleties to using applicable structs created with
define-struct/exec that I do not understand. For example, the following
program fails to typecheck:
#lang typed/racket
(define-struct/exec adder ([name : Symbol])
[(λ (this n) (add1 n)) : (-> adder Number Number)])
(define v
(adder 'v))
(apply v '(41))
with the error "Type Checker: Type of argument to apply is not a function
type:
adder".
I thought that I might need to add a type annotation, but I also am
confused about how to write the type of `v` in the above program. If I
change the above program to one that does typecheck:
#lang typed/racket
(define-struct/exec adder ([name : Symbol])
[(λ (this n) (add1 n)) : (-> adder Number Number)])
(define v
(adder 'v))
(v 41)
the REPL prints the type of v as simply `adder`, but, hovering over the use
of `v` in the last line, the tooltip in DrRacket shows the type as `(U (->
adder Number Number) adder)`.
This seems to be wrong. That function type is the type of the value for
`adder`'s prop:procedure, not the type of an `adder` when used as a
function. Annotating `v` with `(: v (U (-> adder Number Number) adder))`
causes the program to fail to typecheck.
But it isn't clear what type should be used to annotate `v`. Writing `(: v
(U (-> Number Number) adder))` also causes typechecking to fail, as does
experimenting with an intersection type or simply writing `(: v (-> Number
Number))`.
*3. parse-command-line doesn't support usage-help, help-labels, help-proc,
or unknown-proc*
The type for `parse-command-line` doesn't support the `'usage-help`
specification (or `#:usage-help` in an equivalent `command-line` form), so
the following program, which works fine in #lang racket, fails to typecheck:
#lang typed/racket
(parse-command-line
"example"
#("-h")
'([usage-help "here is some usage help"])
void
null)
Worse, the type for the `'help-labels`/`#:help-labels` specification is
wrong, so the following program typechecks successfully but raises a
run-time error:
#lang typed/racket
(parse-command-line
"example"
#("-h")
'([help-labels ("this is a help label")])
void
null)
I have tried to write a better contract for `parse-command-line` using
`require/typed`, but the following program, for example, fails to typecheck
with the error "cannot generate contract for variable arity polymorphic
type":
#lang typed/racket/base
(require/typed
racket/cmdline
[parse-command-line
(All (b a ...)
(-> Path-String
(U (Listof String) (Vectorof String))
(Listof
(U (Pairof 'ps (Listof String))
(Pairof
(U 'final 'help-labels 'multi 'once-any 'once-each)
(Listof (Listof Any)))))
(-> Any a ... a b)
(Listof String)
b))])
Note that the type above is exactly the type reported by the #lang
typed/racket REPL for `parse-command-line` by default. Also, this type does
not support the optional "help-proc" or "unknown-proc" arguments.
Thanks to all who have worked on and promoted Typed Racket! Really, it is
remarkable how *few* surprises there are when adding types to an untyped
program.
-Philip
--
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.
