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