Waarom worden de niet-afhankelijke typevariabelen in het OCAML-object niet weergegeven wanneer het klassentype wordt gebruikt?

Ik zou graag de reden voor dit gedrag van OCAML-objecten willen begrijpen. Stel dat ik een klasse A heb die methoden van een object van een andere klasse B aanroept. Schematisch roept A # f B # g en B # h op. De normale praktijk in OOP is dat ik zou willen vermijden om B te gebruiken als een vaste betonklasse, maar in plaats daarvan alleen een interface voor B aan te geven. Wat is de beste manier om dit in OCAML te doen? Ik heb verschillende opties uitgeprobeerd en ik begrijp niet helemaal waarom sommige werken terwijl anderen dat niet doen. Hier zijn de codevoorbeelden.

Versie 1:

 # class classA = object
    method f b = b#g + b#h 
   end ;;
 Error: Some type variables are unbound in this type:
     class a : object method f : < g : int; h : int; .. > -> int end
   The method f has type (< g : int; h : int; .. > as 'a) -> int where 'a
   is unbound

This behavior is well-known: OCAML correctly infers that b has the open object type but then complains that my class does not declare any type variables. So it seems that classA is required to have type variables; I then introduced a type variable explicitly.

Versie 2:

 # class ['a] classA2 = object
   method f (b:'a) = b#g + b#h
   end ;;
 class ['a] classA2 :
   object constraint 'a = < g : int; h : int; .. > method f : 'a -> int end

Dit werkt, maar de klasse is nu expliciet polymorf met een typevoorwaarde, zoals OCAML laat zien. Het is ook verwarrend dat het klassetype een typevariabele 'a bevat en toch kan ik nog steeds zeggen laat x = nieuwe classA2 zonder een typewaarde voor ' op te geven a . Waarom is dat mogelijk?

Een ander nadeel van classA2 is dat een expliciete typevoorwaarde (b: 'a) een typevariabele bevat. Ik weet immers dat b moet voldoen aan een vaste interface in plaats van aan een onbekend type 'a . Ik wil dat OCAML verifieert dat deze interface inderdaad correct is.

Dus in versie 3 heb ik eerst een interface classB als een klassetype gedeclareerd en vervolgens verklaard dat b van dit type moet zijn:

 # class type classB = object method g:int method h:int end;;
 class type classB = object method g : int method h : int end
 # class classA3 = object method f (b:classB) = b#g + b#h end;;
 class classA3 : object method f : classB -> int end

Dit werkt ook, maar mijn raadsel blijft: waarom vereist classA3 geen expliciet polymorfisme meer?

Samenvatting van vragen:

  • Waarom is het mogelijk om nieuwe classA2 te gebruiken zonder een type op te geven voor 'a , ook al wordt classA2 aangegeven met een type variabele 'a ?
  • Waarom accepteert classA3 een typevoorwaarde (b: classB) en is er geen variabele met een vast type meer nodig?
  • Is de functionaliteit van classA2 en classA3 anders op een subtiele manier en zo ja, hoe?
7

2 antwoord

Dit gaat een beetje ingewikkeld worden, dus houd het goed. Laat me eerst een classA4 -variant toevoegen, wat toevallig ook is wat je echt nodig hebt.

class classA4 = object
  method f : 'a. (#classB as 'a) -> int = fun b -> b#g + b#h
end

Klassen classA2 , classA3 en classA4 zijn allemaal subtiel anders, en het verschil ligt in hoe OCaml het type polymorfisme en objectpolymorfisme behandelt. Laten we aannemen dat twee klassen, b1 en b2 , het type klasse B implementeren.

In terms of object polymorphism, this means that an expression of type b1 can be coerced to type classB using the coercion syntax (new b1 :> classB). This type coercion discards type information (you no longer know the object is of type b1), so it must be made explicit.

In terms of type polymorphism, this means that type b1 can be used in place of any type variable that has constraint #classB (or < g : int ; h : int ; .. >). This does not discard any type information (as the type variable is replaced by the actual type), so it is performed by the type inference algorithm.

Methode f van classA3 verwacht een parameter van het type classB , wat betekent dat een type dwang verplicht is:

let b = new b1 
let a = new classA3
a # f b (* Type error, expected classB, found b1 *)
a # f (b :> classB) (* Ok ! *)

Dit betekent ook dat (zolang u dwingt) elke klasse die klasse B implementeert, kan worden gebruikt.

Methode f van classA2 verwacht een parameter van een type dat overeenkomt met constraint #classB , maar OCaml bepaalt dat een dergelijk type niet ongebonden mag zijn, dus het is gebonden op het niveau van de klas. Dit betekent dat elke instantie van classA2 parameters accepteert van een single willekeurig type dat classB implementeert (en dat type wordt type-afgeleid).

let b1 = new b1 and b2 = new b2
let a  = new classA2 
a # f b1 (* 'a' is type-inferred to be 'b1 classA2' *)
a # f b2 (* Type error, because b1 != b2  *)

Het is belangrijk op te merken dat classA3 gelijk is aan classB classA2 , daarom is er geen afhankelijke type-variabele vereist, en ook waarom deze strikt minder expressief is dan classA2 .

Methode f van classA4 heeft een expliciet type gekregen met de syntaxis 'a. , die de typevariabele op het methodniveau bindt in plaats van de niveau van de klas. Het is eigenlijk een universele kwantifier, wat betekent dat "deze methode kan worden gebruikt voor elk type " a waarmee #classB wordt geïmplementeerd:

let b1 = new b1 and b2 = new b2
let a  = new classA4
a # f b1 (* 'a is chosen to be b1 for this call *)
a # f b2 (* 'a is chosen to be b2 for this call *)
6
toegevoegd
Geweldig spul, bedankt! Dus klasse A moet altijd polymorfisme hebben, alleen dat wordt soms niet expliciet getoond. Het lijkt er ook op dat OOP expliciete dwang of expliciete universeel gekwantificeerde typevariabelen vereist voor methoden, - beide zijn relatief recente toevoegingen aan OCAML.
toegevoegd de auteur winitzki, de bron

Er is een oplossing die iets eenvoudiger is dan die van Victor: je hoeft class2 niet te parametreren over een type, gebruik gewoon class type classB :

class classA2bis = object
  method f (b: classB) = b#g + b#h
end ;;

Victor's solution (f : 'a . (#classB as 'a) -> int) works for any type that is a supertype of classB. Both are equally expressive: with Victor's solution, as he explain, the class used is instantiated at the call site: a#f b will work for any type of b bigger than classB, by implicit polymorphic instantiation. With this solution, the argument has to be of the exact type classB, so you must coerce it explicitely if b has a bigger type: a#f (b :> classB).

Beide oplossingen brengen dus verschillende complexiteitsproblemen met zich mee: met Victor's oplossing maakt de methode-definitie gebruik van verfijnde polymorfe typen en zijn oproepsites licht van gewicht. Met deze even expressieve oplossing is de definitie eenvoudiger, maar de oproepsites moeten een expliciete dwang gebruiken. Aangezien er slechts één definitielocatie en meerdere oproepsites zijn, heeft het over het algemeen de voorkeur om meer complexiteit te hebben aan de definitiekant, hetgeen wordt gedaan door een zogenaamd deskundige bibliotheekontwerper. In de praktijk zul je beide stijlen in het wild vinden, dus het kan belangrijk zijn om ze allebei te begrijpen.

Een historische opmerking, in reactie op wat je lijkt te zeggen in reacties op Victor's antwoord: subtypen via expliciete dwang en expliciete universeel gekwantificeerde typevariabelen zijn niet recente toevoegingen aan OCaml. Bekijk het bestand Changes van de OCaml-distributie; het objectsysteem dateert van OCaml 1.00 (vanaf ongeveer 1995), ondertitels (met expliciete dwangen) zijn aanwezig sinds rond die tijd, en polymorfe methoden en structuurvelden zijn toegevoegd aan OCaml 3.05, uitgebracht in 2002.

Edit: a remark prompted by comments. You may also write the following, using an object type annotation rather than a class type:

class classA2bis = object
  method f (b: < g : int; h : int >) = b#g + b#h
end ;;

Ik heb alleen klasse B gebruikt zoals deze al in uw voorbeeld was gedefinieerd, dus er was niet veel gebruik van een structurele annotatie. In deze context (het klassentype wordt gebruikt als een type, niet om een ​​ander klassentype te definiëren) zijn de twee equivalent. Ze onthullen niets over de implementatie van het object b genomen als parameter; aangezien het objectsysteem van OCaml structureel typen gebruikt, kan elk object met die twee methoden met de juiste typen claimen dat het past in deze typeannotatie (mogelijk via een expliciete subtyperingsstap); het kan zijn gedefinieerd door iemand anders zonder enige verwijzing naar je eigen klassedefinities.

In het OCAML-objectsysteem zijn er relatief subtiele verschillen tussen objecttypen en klassentypen, waar ik niet veel over weet: ik gebruik geen objectgeoriënteerd programmeren. Als u wilt, kunt u de details in de referentiehandleiding lezen of het U3-boek .

Edit 2: Note that #classB as 'a and classB are not equivalently expressive in general: the first, more complex formulation is useful when you want to express sharing between different occurences of the type. For example, 'a . (#foo as 'a) -> 'a is a very different type from foo -> foo. It is strictly more general, because it preserves strictly more information on the return type. In your case, though, both type are equi-expressive because there is only one occurence of the class type, so no potential sharing.

4
toegevoegd
Goed {f: 'a} is beschikbaar sinds records en parametrische typen bestaan ​​(zelfs vóór Caml Light) en {f:' a. ....} is toegevoegd in OCaml 3.05. Ik denk dat je idee dat het 'recentelijk is toegevoegd' kan komen van het feit dat, in 3.12, zo'n eersteklas polymorfe annotatie 'a. foo waar gegeneraliseerd naar functiedefinities, om polymorfe recursie mogelijk te maken. Er is ook een andere syntaxis laat f (type a) ... die om volledig verschillende redenen ook is toegevoegd in 3.12 (eersteklas modules en, sinds 4.00, GADT).
toegevoegd de auteur gasche, de bron
U denkt dat het gebruik van het klassentype classB "een afhankelijkheid van klasseA op de concrete klasse B" dwingt denk ik misplaatst is. Ik heb mijn antwoord bijgewerkt om dit te vermelden.
toegevoegd de auteur gasche, de bron
"staat niet toe om een ​​andere klasse te gebruiken dan klasse B" betekent niets voor mij, omdat je altijd een object uit een superklasse tot dit type kunt dwingen. Alles met het type kan het type door een dwang. Ik zie niet welk verschil je probeert te maken, behalve misschien syntactisch gemak. Zie mijn tweede bewerking voor een geval waarin is een verschil.
toegevoegd de auteur gasche, de bron
+1 voor uw bewerking2
toegevoegd de auteur Victor Nicollet, de bron
Bedankt voor het historische decor. Was het niet de eerste keer dat je polymorfe records zoals {f: 'a} kon hebben en pas later werden de expliciete universele kwantoren toegevoegd, {f:' a. ('a ->' a -> whatever)} ? Wat betreft uw suggestie, dat wil zeggen met behulp van een concrete klasse en casting, - ja, dit zal natuurlijk werken, maar dit wilde ik in de eerste plaats vermijden, omdat dit een afhankelijkheid van klasse A op het beton i> klasse B, - een afhankelijkheid die klasseA helemaal niet nodig heeft.
toegevoegd de auteur winitzki, de bron
Ik denk dat er een verschil is tussen het gebruik van een typeannotatie , wat een gesloten objecttype is, en , een open objecttype. De tweede dwingt polymorfisme, de eerste laat geen andere klasse toe dan klasse B. Men moet het open objecttype gebruiken om subklassen van klasse B met deze code te kunnen gebruiken. Is dit correct? Ik heb de handleidingen over OOP al gelezen in OCAML, maar naar mijn mening presenteren ze geen duidelijk en eenvoudig beeld.
toegevoegd de auteur winitzki, de bron