Ko- och kontravarians

Johan Kullbom []

I denna artikel försöker jag förstå och i bästa fall även förmedla viss förståelse för något som kallas kovarians respektive kontravarians (covariance and contravariance) inom typteori men främst i förhållande till programmeringsspråken Scala, C# och Java.

Innehåll

Motivation

Destruktivitet?

Arrayer är felaktigt kovarianta

Substituerbarhet

Delegates har korrekt varians

Funktionstyper och subtyper

Motivation

Jag har den senaste tiden ägnat mig mycket åt att försöka förstå mig på det som kallas generics i C# (och Java) och i viss mån typteori i allmänhet. För ett tag sedan blev jag varse att (motsvarande) List<Monkey> inte var en subklass till List<Animal>.

public class Animal {}
public class Mammal : Animal {}
public class Giraffe : Mammal {}
public class Monkey : Mammal {}

Utifrån denna klasshieraki tyckte jag att jag borde kunna skriva:

List<Monkey> monkeys = new List<Monkey>();
List<Animal> animals = monkeys; 

Till att börja med tyckte jag att detta måste vara ett misstag i språket (C#) och började gräva i vad som kunde motivera detta missförhållande. Ganska snart hittade jag en övertygande förklaring. Om min kod skulle vara tillåten skulle jag också kunna utvidga den till:

List<Monkey> monkeys = new List<Monkey>();
List<Animal> animals = monkeys; 

animals.Add(new Giraffe());

Att jag inte får lägga till en giraff till en lista av apor förstod jag. Men tänk om min List-klass skulle ha varit immutable och inte hade några metoder i stil med Add?

Det visade sig att teorin kring under vilka omständigheter dylik substituering kan tillåtas är både omfattande och särdeles intressant.

Destruktivitet?

Utifrån exemplet med listor och Add-metoden ligger det nära till hands att hänföra problemet till destruktivitet i allmänhet. I C# skulle det t.ex. inte finnas några hinder för att låta IEnumerable<Animal> vara substituerbart med IEnumerable<Monkey>.

IEnumerable<Monkey> monkeys = new List<Monkey>();
IEnumerable<Animal> animals = monkeys;

För att övertyga oss om att detta faktiskt inte har att göra med destruktivitet tänker vi oss att vår IEnumerable har en RemoveAll-metod.

IEnumerable<Monkey> monkeys = new List<Monkey>();
IEnumerable<Animal> animals = monkeys;

animals.RemoveAll();

Det är fortfarande helt typsäkert att låta IEnumerable<A> vara substituerbart med IEnumerable<B> om B är en subklass (eller mer generellt: substituerbar) med A.

Om vi istället tänker oss att IEnumerable<T> har en (icke destruktiv) bool Contains(T element)-method så är det plötsligt inte typsäkert längre.

IEnumerable<Monkey> monkeys = new List<Monkey>();
IEnumerable<Animal> animals = monkeys;

animals.Contains(new Giraffe());

Arrayer är felaktigt kovarianta

En annan intressant iaktagelse är att i både C# och Java så passerar kod motsvarande mitt urspungliga exempel typkontroll om vi istället använder vanliga arrayer:

Monkey[] monkeys = new Monkey[] { new Monkey(), new Monkey(), new Monkey() };
Animal[] animals = monkeys;

animals[2] = new Giraffe(); // Ger exception runtime!

Arrayer vars elementtyp är av s.k. referenstyp (reference type) är i C# och Java kovariant mot sin elementtyp. Arrayer är (felaktigt) definierade som substituerbara med arrayer vars elementtyp är substituerbar med sin elementtyp.

Detta är förstås vansinne och kan inte annat än betraktas som ett misstag (det hela blir ju inte bättre av att foreach också har en minst sagt märklig definition i C#).

Notera här att varken C# eller Java anser att Animal[] är en superklass till Monkey[]. Animal[] är däremot (egentligen inte) subtituerbart med Monkey[] och i den meningen en supertyp till denna.

Substituerbarhet

Barbara Liskov har en välkänd formulering om krav på en subtyp (Liskov Substitution Principle - LSP):

Let φ(x) be a property provable about objects x of type T. Then φ(y) should be true for objects y of type S where S is a subtype of T.

En array av typen Animal[] kan sägas äga egenskapen av att kunna innehålla alla objekt av typen Animal. Om en annan typ skall kunna betraktas som en subtyp till Animal[] måste denna egenskap gälla även för den typen. Monkey[] har inte den egenskapen då den bara kan innehålla element av typen Monkey.

Liskovs formulering bygger på en definition av subtyp utifrån substituerbarhet gällande beteende:

Definition of the subtype relation, ⪯: σ = ⟨O_σ, S, M⟩ is a subtype of τ = ⟨O_τ, T, N⟩ if there exists an abstraction function, A : S → T, and a renaming map, R : M → N such that:

1. Subtype methods preserve the supertype methods' behavoir. If m_τ of τ is the corresponding renamed method m_σ of σ the following rules must hold:

   • Signature rule.

     • Contravariance of arguments. m_τ and m_σ have the same number of arguments. If the list of argument types of m_τ is α_i and that of m_σ is β_i then ∀i . α_i ⪯ β_i.

     • Covariance of result. Either both m_τ and m_σ have a result or neither has. If there is a result, let m_τ's result type be α and m_σ's be β. Then β ⪯ α.

     • Exception rule. The exceptions signaled by m_σ are contained in the set of exceptions signaled by m_τ.

   • Methods rule. For all x : σ:

     • Pre-condition rule. m_τ.pre[A(x_pre)/x_pre] ⇒ m_σ.pre.

     • Post-condition rule. m_σ.post ⇒ m_τ.post[A(x_pre)/x_pre, A(x_post)/x_post]

2. Subtypes preserve supertype properties. For all computations, c, and all states ρ and ψ in c such that ρ precedes ψ, for all x : σ:

   • Invariant Rule. Subtype invariants ensure supertype invariants.

     I_σ ⇒ I_τ[A(x_ρ)/x_ρ]

   • Constraint Rule. Subtype constraints ensure supertype constraints.

     C_σ ⇒ C_τ[A(x_ρ)/x_ρ, A(x_ψ)/x_ψ]

En typ beskrivs av en trippel, ⟨O, S, M⟩, där O är en mängd objekt, V är en mängd värden och M är en mängd metoder. I det här sammanhanget intresserar vi oss inte vidare för detta utan tittar på de två första punkterna under “signature rule”.

För en subtyps (σ) metoder gäller att varje argumenttyp (β_i) måste vara en supertyp (∀i . α_i ⪯ β_i - eller med vanligare symbol för subtyp ∀i . α_i <: β_i ) till motsvarande argumenttyp (α_i) i supertypens metod. Argumenttyperna till en subtyps metoder måste vara kontravarianta till supertypen.

För returtyper gäller det motsatta. Returntypen (β) för en subtyps metoder måste vara en subtyp (β ⪯ α) till returtypen (α) av supertypens metod. Returtyperna av en subtyps metoder måste vara kovarianta till supertypen.

För funktionstyper gäller samma regler. Vi kan utifrån Liskovs definition betrakta en funktionstyp som en klass eller ett interface bestående av enbart en metod.

Delegates har korrekt varians

I C# är varians för funktionstyper (delegates) korrekt implementerat. En funktiontyp som returnerar Animal kan utan problem substitueras av en annan som returnerar Giraffe.

Func<Mammal> fn = () => new Giraffe();

Att försöka substituera fn med en funktion med kontravariant returtyp däremot går inte.

Func<Mammal> fn = () => new Animal(); // Ger error CS1662

För argumenttyper gäller istället kontravarians så att en funktionstyp kan substitueras med en annan vars argumenttyper är supertyper till de ursprungliga argumenttyperna:

Action<Mammal> action = (Animal a) => {};

Argumenttyper som är subtyper går inte:

Action<Mammal> action = (Giraffe a) => {}; // Get error CS1661

Tyvärr har man, i C#, bara implementerat varians för lambda-uttryck (och “method groups”) och alla försök att substituera en faktisk typ med en annan godkänns inte.

Func<Giraffe> fn1 = () => new Giraffe();
Func<Mammal> fn2 = fn1; // Ger error

Då funktionstyper är vanliga klasser skulle man för att klara detta behöva generell varians för klasser. I Scala som har generell varians är funktiontyper (med ett argument) generiskt definierat som:

trait Function1[-T1, +R] extends AnyRef { self =>
  def apply(v1:T1): R
  // ...
}

Returtypen (R) är definierad som kovariant (+) och argumenttypen (T1) som kontravariant (-).

För högre ordningens funktionstyper blir det lite värre. En funktion som returnerar en annan funktion kan kan inte vara kovariant i förhållande till argumenttyperna i den returnerade funktionstypen.

delegate Func<T, R> MetaFunc<T, R>();

I MetaFunc kan inte T vara kovariant definierad då förväntningarna på den returnerade funktionen (Func<T, R>) är att kontravarians gäller i förhållande till T. R däremot står i kovariant position både i MetaFunc och i dess returtyp och skulle därör kunna vara kovariant definierad. Ett typargument står i ko- eller kontravariant position till den innersta (polymorpha) typen argumentet ingår i. I MetaFunc står T i kontravariant position medans R står i kovariant position i förhållande till Func och skulle (om C# tillät det) kunna definieras som:

delegate Func<T, R> MetaFunc<-T, +R>();

Referenser/bibliografi: