Ko- och kontravarians

Johan Kullbom [HiddenEMail]
2008 (senast uppdaterad 2008-07-05)

Valid XHTML 1.0 Transitional
Valid CSS!

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.

Uttrycket (monkeys is Animal[]) returnerar true i C# så det betraktas faktiskt som en subtyp.

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 : ST, and a renaming map, R : MN 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(xpre)/xpre] ⇒ mσ.pre.

      • Post-condition rule. mσ.postmτ.post[A(xpre)/xpre, A(xpost)/xpost]

  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.

Både C# och Scala expanderar funktionstyper till en klass/interface med en metod. I förslaget för att införa funktionstyper i Java 6 tänker man sig också en sådan lösning.

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

Error CS1662: “Cannot convert lambda expression to delegate type 'System.Func<Mammal>' because some of the return types in the block are not implicitly convertible to the delegate return type”

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

Error CS1661: “Cannot convert lambda expression to delegate type 'System.Action<Mammal>' because the parameter types do not match the delegate parameter types”

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:

Eric Lippert; “Covariance and Contravariance in C#”; Blog: Fabulous Adventures In Coding; 2007 - 2008;
[Part One]
[Part Two: Array Covariance]
[Part Three: Method Group Conversion Variance]
[Part Four: Real Delegate Variance]
[Part Five: Higher Order Functions Hurt My Brain]
[Part Six: Interface Variance]
[Part Seven: Why Do We Need A Syntax At All?]
[Part Eight: Syntax Options]
[Part Nine: Breaking Changes]
[art Ten: Dealing With Ambiguity]
[Part Eleven: To infinity, but not beyond]
Martin Odersky; “Scala By Example” - “8.2 Variance Annotations”; 2008; [Online]
Barbara H. Liskov och Jeannette M. Wing; “A New Definition of the Subtype Relation”; 1993; [Online]
Barbara H. Liskov och Jeannette M. Wing; “Behavioral Subtyping Using Invariants and Constraints”; 1999; CMU-CS-99-156; [Online]
Emir, Kennedy, Russo, Yu; “Variance and Generalized Constraints for C Generics”; [Online]
Andrew J. Kennedy och Benjamin C. Pierce; “On Decidability of Nominal Subtyping with Variance”; [Online]
Moors, Piessens, Odersky; “Generics of a Higher Kind”; [Online]