[racket] Typed racket puzzle (ii)

On Wed, Aug 17, 2011 at 7:01 AM, Norman Gray <norman at astro.gla.ac.uk> wrote:
>
>> 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).

It's ok to think of things as sets, and subtyping as subsets.  The
trick is that functions are a little different than you expect. In
particular, if you have two types, (A -> B) and (C -> D), for the
first to be a subtype of the second, you do need B to be a subtype of
D.  But for the arguments, it goes the other way: C must be a subtype
of A.

Here's how to see why you need that. To say that (A -> B) is a subtype
of (C -> D), you're saying that you can use (A -> B) anywhere you need
(C -> D).  But some program that expects a (C -> D) function might
pass it a C, of course, so your new replacement function must accept
all of the Cs.  Therefore, A needs to accept all of the Cs, which
means that A must be a subtype of C.

The standard term for this is that function types are "contravariant"
(go the other way) in their argument type.

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

Unfortunately, neither ML nor Haskell have subtyping, so this won't be
covered there.
-- 
sam th
samth at ccs.neu.edu