[racket] Typed racket puzzle (ii)

From: Sam Tobin-Hochstadt (samth at ccs.neu.edu)
Date: Wed Aug 17 08:12:27 EDT 2011

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

Posted on the users mailing list.