[racket] Typed racket puzzle (ii)

On Tue, Aug 16, 2011 at 5:57 PM, Norman Gray <norman at astro.gla.ac.uk> wrote:
>
> Greetings, all.
>
> I'm terribly puzzled by a typed-racket error message I'm getting (I seem to be rather abusing this list today -- apologies -- but I'm busy reminding myself why it's useful not to do two interesting develoments with a project at one time).
>
> If I run the following in DrRacket:
>
> #lang typed/racket
>
> (: my-func (String String -> String))
> (define (my-func s1 s2)
>  (string-append s1 ":" s2))
>
> (my-func "Hello" "World")
>
> (: call-func ((List String String) -> String))
> (define (call-func string-list)
>  ((inst apply String String) my-func string-list)
>  ;(apply my-func string-list)
>  )
>
> (call-func '("Hello" "There"))
>
> ...I get an error message
>
>> Type Checker: Cannot instantiate non-polymorphic type ((String * -> String) (Listof String) -> String) in: apply
>
> Dr Racket also tells me that:
>
>    > apply
>    - : (All (a b) ((a * -> b) (Listof a) -> b))
>
> Which makes sense, in that it corresponds to the message I'm seeing.
>
> Now, I don't _really_ follow the logic of Typed Racket in a fully formal way (I know, I should have another go at The Little MLer), but the only way I can really make sense of this message is if the type (String String -> String) is not a subtype of (String * -> String), or if (List String String) is not a subtype of (Listof String).  Both of these would be a little unexpected.
>
> Is that the right interpretation (in which case, where could I find the hierarchy of types?); or is APPLY being more particular about its types than is appropriate?

There are several problems here:

1. The error message you're getting about `apply' is wrong -- it
should instantiate just fine.  I'll fix that.
2. `apply' should work, without instantiation, in this case.  Right
now, it doesn't handle fixed-arity functions applied to fixed length
lists, but I'll fix that, too.

But third, you're right that (String String -> String) is not a
subtype of (String * -> String), so if your instantiation had worked,
the program wouldn't typecheck.  The way to see why this is is as
follows:

(: test : (String * -> String) -> Any)
(define (test f)
  (f "a" "b" "b"))

(test (lambda: ([x : String] [y : String]) x))

Now, if this program type checked, which is what that subtyping would
allow, we'd get an error when we applied our function to the wrong
number of arguments.  So we can't allow that subtyping.
-- 
sam th
samth at ccs.neu.edu