Comment by wittystick

Briefly, algebraic data types add polarity to the types so that we don't have both S <= T and T <= S, which would imply equality. Instead we have S+ <= T- and T+ <= S-. The positive types represent a value source and the negative types are a sink. For example, in a function call, the args are negative and the return type is positive. Inside the function its formal parameters become positive and its return type is negative. Variables exist in an "ambipolar" state which can be both the source or the sink, depending on whether we're using it on the rhs or lhs of an assignment.