On Wed, Aug 17, 2011 at 9:42 AM, Norman Gray <nor...@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 sa...@ccs.neu.edu _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/users
