[plt-scheme] Typed Scheme polymorphic variadic functions

A very helpful explanation...

On Tue, Mar 17, 2009 at 12:49 PM, Stevie Strickland
<sstrickl at ccs.neu.edu> wrote:
...
> Initially, dotted pre-types could only appear as the last part of the domain
> of a function (since they often describe rest arguments).  However, they are
> now allowed to appear in some other useful type constructors such as Values.
>  Unfortunately, we have not yet handled List, and so there's no way for you
> to write an appropriately generic type for the listf function you provided.
>  This work is something we hope to do in the future.
>
> Another source of information is a recently-published paper:
>
>  http://www.ccs.neu.edu/scheme/pubs/#esop09-sthf
>
> Please let me know if this is unclear in any way, or if you have any further
> questions.

(Note: I haven't read the paper yet, but I will do so shortly.)


I am now having problems with the union type constructor:
(U A ... A)
is this also not currently supported?

For my own help in writing the typed list helpers I ginned up a quick
testing infrastructure. This includes a function that runs down a list
of tests, and I struggled a bit with its type signature before
settling on one that is more general than it should be. A test is
generated by a macro that builds each test as a list of a thunked
expression, a value, and a string. This triple of (actual, expected,
message) is not important, but the polymorphism of the checking
function is somewhat interesting. This type is too general, but works
if I apply check-all to an appropriate list as in (check-all
list-of-tests):

(: check-all ((Listof (List (-> Any) Any String)) -> Void))

This type almost works, but not quite if I (apply check-all list-of-tests):
(: check-all (All (A ...) ((List (-> A) A String) ... A -> Void)))

Yet, if I write out (check-all (car lot) (cadr lot)) then it's fine
(lot = list-of-tests). This might make some sense if type checking is
purely syntactic, but since we do know the type of list-of-tests, I
was hoping that the apply function could sort things out. Instead, I
get an error message such as the following:

typecheck: Bad arguments to polymorphic function in apply:
Domain: (List (-> A) A String) ... A
Arguments: (List (List (-> (Listof Integer)) (Listof Integer) String)
(List (-> (Listof Integer)) (Listof Integer) String)) *

Is there a way to convince the type checker that these can be unified?

Anthony