Re: Type equivalency 2

Cagdas Ozgenc wrote:

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 itself.

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'

A language with subtyping would have to treat any contravariant type constructors in a similar way. -- Lennart