Korsningstyp - Intersection type

I typteori kan en skärningstyp tilldelas värden som kan tilldelas både typ och typ . Detta värde kan ges skärningstypen i ett skärningstypssystem . Generellt, om värdena av två typer överlappar varandra, kan ett värde som hör till skärningspunkten mellan de två områdena tilldelas skärningstypen för dessa två typer. Ett sådant värde kan säkert överföras som argument till funktioner som förväntar sig någon av de två typerna. Till exempel i Java implementerar klassen både och och gränssnitten. Därför kan ett typobjekt säkert överföras till funktioner som förväntar sig ett typargument och till funktioner som förväntar sig ett typargument . ${\ displaystyle \ sigma}$${\ displaystyle \ tau}$${\ displaystyle \ sigma \ cap \ tau}$BooleanSerializableComparableBooleanSerializableComparable

Korsningstyper är sammansatta datatyper . I likhet med produkttyper används de för att tilldela ett objekt flera typer. Produkttyper tilldelas emellertid tupler , så att varje tupelelement tilldelas en viss produkttypskomponent. I jämförelse är underliggande objekt av skärningstyper inte nödvändigtvis sammansatta. En begränsad form av skärningstyper är förädlingstyper .

Korsningstyper är användbara för att beskriva överbelastade funktioner . Om till exempel den typ av funktion som tar ett tal som ett argument och returnerar ett tal, och är den typ av funktion som tar en sträng som ett argument och returnerar en sträng, kan skärningspunkten mellan dessa två typer användas för att beskriva ( överbelastade) funktioner som gör det ena eller det andra, baserat på vilken typ av ingång de ges. number => numberstring => string

Samtida programmeringsspråk, inklusive Ceylon , Flow, Java , Scala , TypeScript och Whiley (se jämförelse av språk med skärningstyper ), använder skärningstyper för att kombinera gränssnittsspecifikationer och för att uttrycka ad hoc polymorfism . Som ett komplement till parametrisk polymorfism kan skärningstyper användas för att undvika klasshierarkiföroreningar från tvärgående problem och minska pannkodskod , som visas i TypeScript-exemplet nedan.

Den typ teoretiska studier av skärningstyper kallas skärningstypen disciplin . Anmärkningsvärt kan programavslutning preciseras med hjälp av skärningstyper.

TypeScript -exempel

TypeScript stöder skärningstyper, förbättrar typsystemets uttrycksfullhet och minskar den potentiella klasshierarkistorleken, enligt följande.

Följande programkod definierar klasserna Chicken, Cowoch RandomNumberGeneratoratt var och en har en metod produceåtervänder ett föremål av endera typen Egg, Milkeller number. Dessutom, de funktioner eatEggoch drinkMilkkräver argument av typ Eggoch Milk, respektive.

class Egg { private kind: "Egg" }
class Milk { private kind: "Milk" }

//produces eggs
class Chicken { produce() { return new Egg(); } }

//produces milk
class Cow { produce() { return new Milk(); } }

//produces a random number
class RandomNumberGenerator { produce() { return Math.random(); } }

//requires an egg
function eatEgg(egg: Egg) {
    return "I ate an egg.";
}

//requires milk
function drinkMilk(milk: Milk) {
    return "I drank some milk.";
}

Följande programkod definierar den ad hoc polymorfa funktion animalToFoodsom åberopar medlemsfunktionen produceför det givna objektet animal. Funktionen animalToFoodhar två typkommentarer, nämligen och , anslutna via konstruktören av skärningstypen . Specifikt, när den appliceras på ett argument av typen returnerar ett objekt av typen typ , och när de appliceras på ett argument av typen returnerar ett objekt av typen typ . Helst bör den inte vara tillämplig på något objekt som (möjligen av en slump) har en metod. ((_: Chicken) => Egg)((_: Cow) => Milk)&animalToFoodChickenEggCowMilkanimalToFoodproduce

//given a chicken, produces an egg; given a cow, produces milk
let animalToFood: ((_: Chicken) => Egg) & ((_: Cow) => Milk) =
    function (animal: any) {
        return animal.produce();
    };

Slutligen visar följande programkod typsäker användning av ovanstående definitioner.

var chicken = new Chicken();
var cow = new Cow();
var randomNumberGenerator = new RandomNumberGenerator();

console.log(chicken.produce()); //Egg { }
console.log(cow.produce()); //Milk { }
console.log(randomNumberGenerator.produce()); //0.2626353555444987

console.log(animalToFood(chicken)); //Egg { }
console.log(animalToFood(cow)); //Milk { }
//console.log(animalToFood(randomNumberGenerator)); //ERROR: Argument of type 'RandomNumberGenerator' is not assignable to parameter of type 'Cow'

console.log(eatEgg(animalToFood(chicken))); //I ate an egg.
//console.log(eatEgg(animalToFood(cow))); //ERROR: Argument of type 'Milk' is not assignable to parameter of type 'Egg'
console.log(drinkMilk(animalToFood(cow))); //I drank some milk.
//console.log(drinkMilk(animalToFood(chicken))); //ERROR: Argument of type 'Egg' is not assignable to parameter of type 'Milk'

Ovanstående programkod har följande egenskaper:

• Linjerna 1–3 skapar objekt chicken, cowoch randomNumberGeneratorav respektive typ.
• Raderna 5–7 skrivs ut för de tidigare skapade objekten respektive resultat (tillhandahålls som kommentarer) vid anrop produce.
• Rad 9 (resp. 10) visar typsäker användning av metoden som animalToFoodtillämpas på chicken(resp. cow).
• Rad 11, om den inte är kommenterad, skulle resultera i ett typfel vid kompileringstidpunkten. Även om genomförandet av animalToFoodkunde åberopa producemetod randomNumberGenerator, den typanteckning av animalToFoodkänns det. Detta är i överensstämmelse med den avsedda innebörden av animalToFood.
• Linje 13 (resp. 15) visar att tillämpning animalToFoodpå chicken(resp. cow) Resulterar i ett objekt av typ Egg(resp. Milk).
• Rad 14 (resp. 16) visar att ansökan animalToFoodtill cow(resp. chicken) Inte resulterar i ett objekt av typ Egg(resp. Milk). Därför skulle rad 14 (resp. 16) leda till ett typfel vid kompileringstidpunkten om den inte kommenterades.

Jämförelse med arv

Ovanstående minimalistiska exempel kan realiseras med arv , till exempel genom att härleda klasserna Chickenoch Cowfrån en basklass Animal. Men i en större miljö kan detta vara ofördelaktigt. Att införa nya klasser i en klasshierarki är inte nödvändigtvis motiverat av tvärgående problem , eller kanske direkt omöjligt, till exempel när man använder ett externt bibliotek. Tänkbart kan ovanstående exempel utökas med följande klasser:

• en klass Horsesom inte har någon producemetod;
• en klass Sheepsom har en producemetod som återvänder Wool;
• en klass Pigsom har en producemetod, som bara kan användas en gång, återvänder Meat.

Detta kan kräva ytterligare klasser (eller gränssnitt) som anger om en produktionsmetod är tillgänglig, om produktmetoden returnerar mat och om produktmetoden kan användas upprepade gånger. Sammantaget kan detta förorena klasshierarkin.

Jämförelse med anttypning

Ovanstående minimalistiska exempel visar redan att ankskrivning är mindre lämpad för att förverkliga det givna scenariot. Medan klassen RandomNumberGeneratorinnehåller en producemetod randomNumberGeneratorbör objektet inte vara ett giltigt argument för animalToFood. Ovanstående exempel kan förverkligas med ankskrivning, till exempel genom att introducera ett nytt fält argumentForAnimalToFoodtill klasserna Chickenoch Cowmarkera att objekt av motsvarande typ är giltiga argument för animalToFood. Detta skulle dock inte bara öka storleken på respektive klasser (särskilt med införandet av fler metoder som liknar animalToFood), utan är också ett icke-lokalt tillvägagångssätt med avseende på animalToFood.

Jämförelse med funktionell överbelastning

Ovanstående exempel kan realiseras med hjälp av funktionsöverbelastning , till exempel genom att implementera två metoder och . I TypeScript är en sådan lösning nästan identisk med exemplet. Andra programmeringsspråk, till exempel Java , kräver distinkta implementeringar av den överbelastade metoden. Detta kan leda till antingen kodduplicering eller pannkodskod . animalToFood(animal: Chicken): EgganimalToFood(animal: Cow): Milk

Jämförelse med besökarmönstret

Ovanstående exempel kan realiseras med hjälp av besökarmönstret . Det skulle kräva att varje djurklass implementerar en acceptmetod som accepterar ett objekt som implementerar gränssnittet AnimalVisitor(lägger till icke-lokal pannkodskod ). Funktionen animalToFoodskulle realiseras som visitmetoden för en implementering av AnimalVisitor. Tyvärr skulle sambandet mellan ingångstyp ( Chickeneller Cow) och resultattyp ( Eggeller Milk) vara svårt att representera.

Begränsningar

Å ena sidan, skärningstyper kan användas för att lokalt Antecknings olika typer till en funktion utan att införa nya klasser (eller gränssnitt) till klasshierarkin. Å andra sidan kräver detta tillvägagångssätt att alla möjliga argumenttyper och resultattyper anges specifikt. Om en funktions beteende kan specificeras exakt av antingen ett enhetligt gränssnitt, parametrisk polymorfism eller anttryckning , är korsningstypernas generösa natur ogynnsam. Därför bör skärningstyper anses komplettera befintliga specifikationsmetoder.

Beroende skärningstyp

En beroende skärningstyp , betecknad , är en beroende typ där typen kan bero på termvariabeln . I synnerhet, om en term har den beroende skärningstypen , då termen har både typen och typen , där är den typ, som resulterar från att ersätta alla förekomster av termen variabeln i med termen . ${\ displaystyle (x: \ sigma) \ cap \ tau}$${\ displaystyle \ tau}$${\ displaystyle x}$${\ displaystyle M}$${\ displaystyle (x: \ sigma) \ cap \ tau}$${\ displaystyle M}$${\ displaystyle \ sigma}$${\ displaystyle \ tau [x: = M]}$${\ displaystyle \ tau [x: = M]}$${\ displaystyle x}$${\ displaystyle \ tau}$${\ displaystyle M}$

Scala exempel

Scala stöder typdeklarationer som objektmedlemmar. Detta gör att en typ av en objektmedlem kan bero på värdet av en annan medlem, som kallas en vägberoende typ . Till exempel definierar följande programtext en Scala -egenskap Witness, som kan användas för att implementera singletonmönstret .

trait Witness {
  type T
  val value: T {}
}

Ovanstående egenskap Witnessdeklarerar medlemmen T, som kan tilldelas en typ som dess värde, och medlemmen value, som kan tilldelas ett värde av typ T. Följande programtext definierar ett objekt booleanWitnesssom förekomst av ovanstående drag Witness. Objektet booleanWitnessdefinierar typen Tsom Booleanoch värdet valuesom true. Till exempel utföra utskrifter på konsolen. System.out.println(booleanWitness.value)true

object booleanWitness extends Witness {
  type T = Boolean
  val value = true
}

Låt vara typen (specifikt en posttyp ) av objekt som har elementets typ . I exemplet ovan kan objektet tilldelas den beroende skärningstypen . Motiveringen är följande. Objektet har den medlem som tilldelats typen som dess värde. Eftersom är en typ har objektet typen . Dessutom har objektet den medlem som tilldelas värdet för typ . Eftersom värdet på är har objektet typen . Totalt sett har objektet skärningstypen . Därför, som presenterar självreferens som beroende, har objektet den beroende skärningstypen . ${\ displaystyle \ langle {\ textf {x}}: \ sigma \ rangle}$${\ displaystyle {\ textf {x}}}$${\ displaystyle \ sigma}$booleanWitness${\ displaystyle (x: \ langle {\ textf {T}}: {\ text {Type}} \ rangle) \ cap \ langle {\ textf {värde}}: x. {\ textf {T}} \ rangle}$booleanWitnessTBooleanBooleanbooleanWitness${\ displaystyle \ langle {\ textf {T}}: {\ text {Type}} \ rangle}$booleanWitnessvaluetrueBooleanbooleanWitness.TBooleanbooleanWitness${\ displaystyle \ langle {\ texter {värde}}: {\ texter {booleanWitness.T}} \ rangle}$booleanWitness${\ displaystyle \ langle {\ textf {T}}: {\ text {Type}} \ rangle \ cap \ langle {\ textf {värde}}: {\ textf {booleanWitness.T}} \ rangle}$booleanWitness${\ displaystyle (x: \ langle {\ textf {T}}: {\ text {Type}} \ rangle) \ cap \ langle {\ textf {värde}}: x. {\ textf {T}} \ rangle}$

Alternativt kan ovanstående minimalistiska exempel beskrivas med hjälp av beroende posttyper . I jämförelse med beroende korsningstyper utgör beroende posttyper ett strikt mer specialiserat typteoretiskt koncept.

Korsning av en typfamilj

En skärningspunkt mellan en typfamilj , betecknad , är en beroende typ där typen kan bero på termvariabeln . I synnerhet, om en term har den typ , sedan för varje term av typ uttrycket har typen . Denna uppfattning kallas också för implicit Pi -typ , och observerar att argumentet inte hålls på terminsnivå. ${\ displaystyle \ bigcap _ {x: \ sigma} \ tau}$${\ displaystyle \ tau}$${\ displaystyle x}$${\ displaystyle M}$${\ displaystyle \ bigcap _ {x: \ sigma} \ tau}$${\ displaystyle N}$${\ displaystyle \ sigma}$${\ displaystyle M}$${\ displaystyle \ tau [x: = N]}$${\ displaystyle N}$

Jämförelse av språk med skärningstyper

Referenser