Type equivalency 2

Cagdas Ozgenc co19@cornell.edu
Thu, 6 Jun 2002 13:38:36 +0300

> The type constructor F and the type constructor (->) are quite different.
> They have the same kind, but just as the type only tell you part of what a
> value
> is, thekind only tells you part of what a type is.
> Very informally a value of type "F a b" means "I have an a and a b",
> as type "a -> b" means "if you give me an a I'll give you a b".  So the
> function
> arrow "consumes" its first argument rather than produces it.

Then either -> is not a type constructor, or the concept of type
constructors has to be divided into two : consuming type constructors, and
producing type constructors. If so then language has to support a way to
define consuming type constructors as well, in order to be consistent within

I think -> is defined to be a type constructor to make functions first class
values. In the meantime, type systems that support subtyping seem to treat
the arrow in a special fashion. For example

if  A <: B and C <: D then (B -> C) <: (A -> D)   where a <: b indicates 'a'
being a subtype of 'b'

Now do you get the impression that the subtype relation is defined over a
type-constructor here? What about other type constructors then?