Hello.
Yet another question: Consider a type structure like in "Typing Haskell in Haskell" where types are curried, e.g.
data Type = TAp Type Type | TCon Id Kind | TVar Id Kind
This means, "(->) Int" is a valid type. In a subtype calculus you can say, that "a->b" is a subtype of "c->d" if "b" is a subtype of "d" and "c" is a subtype of "a", because "->" is contravariant in its first and covariant in its second argument. So far so good, how can be dealt with subtyping and "partial" types? E.g. is it acceptable to say that "(->) a" is a subtype of "(->) b" if "b" is a subtype of "a"? Any ideas? Or can someone point me to an online-resource which addresses this topic?
Thanks in advance, Steffen
It all depends on the variance, or polarity, of the partial type expression, which must somehow be derivable from the applied type operator (-> in your case). I suggest checking out the work by Martin Steffen on higher-order subtyping; the paper "Polarized Higher-Order Subtyping" should be of particular interest. Martin's papers can be found at http://www.informatik.uni-kiel.de/~ms/Steffen/papers.html -- Johan