dual_type and codual_type conditions

[willtebbutt]

A condition that we require on this function is that P <: Q implies dual_type(P) <: dual_type(Q). In particular, this means that we cannot have dual_type(P) == Dual(P, tangent_type(P)) if P is abstract.

This is something that ought to be tested a lot better than it currently is (we have exactly the same requirement for codual_type, but don't properly test it).

Originally posted by @willtebbutt in #389 (comment)

[gdalle]

I confess I don't understand the reasoning that leads from the first sentence to the second. If P <: Q, doesn't that imply tangent_type(P) <: tangent_type(Q)?

[yebai]

The reasoning is vague to me, too. A clearer answer would be helpful.

[willtebbutt]

What about the reasoning is vague? Reading my original comment, it seems quite precise.

[yebai]

It may be obvious to you, but the writing is not clear due to its brevity. I have the same confusion as @gdalle.

[willtebbutt]

It's just a statement about Julia's type system: it's not the case that P <: Q implies T{P} <: T{Q} for some type T (except if T = Tuple). For example, let P = Real and Q = Number, both of which have tangent_type Any. Clearly, P <: Q, but it's not the case that Dual{Real,Any} <: Dual{Number,Any}.

This example lets us conclude that we cannot define dual_type(P) == Dual{P,tangent_type(P)}, because such a definition will not satisfy P <: Q => dual_type(P) <: dual_type(Q).

An implementation of dual_type which works for everything other than subtypes of Type is (roughly)

dual_type(P) = isconcretetype(P) ? Dual(P,tangent_type(P)) : Dual