[racket] Typed racket puzzle (ii)

Sam, hello.

On 2011 Aug 16, at 23:08, Sam Tobin-Hochstadt wrote:

> 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.

Ah, right -- thanks.  I'm trying to convert a module to typed/racket, partly out of curiousity, and doing a bit of head-scratching.

> 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.

OoooKay.  I was thinking of subtyping in terms of a naive mixture of the (set) extensions of types (the set of things which are instances of (List String String) is a subset of the things which are instances of (Listof String)), and assignment-compatibility.  That understanding clearly fails in your example, because while (List String String) can be assigned to a (Listof String), the function test is declared to accept -- in the sense of have bound to its arguments -- (Listof String) which in this case isn't true.  Gotcha (I think).

I think I do need to have another go at the Little MLer or Haskell, unless there's a nice compact introduction to the formalities of types someone could point to (and I want to see alphas and betas in there!).

Thanks again.  Best wishes,

Norman


-- 
Norman Gray  :  http://nxg.me.uk
School of Physics and Astronomy, University of Glasgow, UK