[racket] Typed racket puzzle (ii)

On Wed, Aug 17, 2011 at 9:42 AM, Norman Gray <norman at astro.gla.ac.uk> wrote:
>
> Sam, hello.
>
> On 2011 Aug 17, at 13:12, Sam Tobin-Hochstadt wrote:
>
>>> 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.
>
> Thanks for the explanation.  Curses!  I must have been reasonably close to working that out for myself, with the thought about what the function is intended to accept.
>
>> 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.
>
> Don't you mean "C must be a subtype of A", here?

Yes, definitely.  It's hard to get math right in prose.  :)

>> The standard term for this is that function types are "contravariant"
>> (go the other way) in their argument type.
>
> Thanks for 'contravariant' in this context.  It's led me to the relevant application of category theory, which I think is the underlying structure I was looking for.  I suppose it's effectively a combination of 'define' and ':' which is in practice the functor in TR terms, with subtyping being the morphism in the type category.  Or something like that.

I don't think `define' and `:' are functors in any sensible category
of Typed Racket types.  But I've been surprised before.  In
particular, `define' is solely about computation, not about types.
-- 
sam th
samth at ccs.neu.edu