Subtyping

[Johan Nordlander]

> 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