Guarded Methods in OCaml

Probleemstelling

Wanneer een taal waarin typecontrole plaatsvindt vóór de uitvoering van het programma (zoals Java of OCaml) parametrisch polymorfisme introduceert (zoals generics in Java), is het soms mogelijk om typevariabelen te beperken. Bijvoorbeeld:

class MyClass<T extends S> { ... }

Hier maken we MyClass generiek door ervan uit te gaan dat de typevariabele T een subtype is van S. Het probleem is dat deze beperking geldt voor de gehele klasse. Soms willen we echter dat beperkingen alleen gelden voor bepaalde methoden. Stel dat we een klasse MyList hebben die een lijst beschrijft:

class MyList<A> extends ArrayList<A> {
    public int length() {
        return this.size();
    }
}

Hoe kunnen we een flatten-methode definiëren die voor een lijst zoals [[1, 2, 3], [4, 5]] de lijst [1, 2, 3, 4, 5] zou produceren? Als we de beperking op klasseniveau plaatsen, dwingen we onze lijst om "altijd een lijst van lijsten" te zijn, wat zeer beperkend is. Om zo'n methode te implementeren, zijn er drie theoretische benaderingen mogelijk.

De methode buiten de klasse verplaatsen

De eerste oplossing is de meest voor de hand liggende: simpelweg "valsspelen" door de methode buiten het lichaam van de klasse te plaatsen (bijvoorbeeld in een statische context of een companion object):

class MyList<A> extends ArrayList<A> {
    public static <A> MyList<A> flatten(MyList<MyList<A>> list) {
        // Implementatie van flatten
    }

    public int length() {
        return this.size();
    }
}

Deze aanpak werkt en vereist geen speciale handelingen. Het dwingt de ontwikkelaar echter om bij te houden welke methoden zich in het lichaam van de klasse bevinden en welke in de statische context. Bovendien doorbreekt het de systematische aanpak van het sturen van berichten naar een instantie, wat vaak wordt gepresenteerd als een van de belangrijkste argumenten in het voordeel van objectgeoriënteerd programmeren.

Extension methods

Kotlin (en andere talen zoals C#) bieden extension methods. Deze maken het niet alleen mogelijk om een bestaande klasse uit te breiden (wat zeer nuttig is voor het toevoegen van gedrag aan de String-klasse, die in Java final is), maar bieden ook meer flexibiliteit bij het definiëren van de ontvanger. We zouden flatten als volgt kunnen schrijven (in Kotlin):

class MyList<A> : ArrayList<A> { ... }

fun <A> MyList<MyList<A>>.flatten() = ...

Hoewel deze oplossing bijna perfect lijkt, moet de methode nog steeds buiten de klasse worden gedefinieerd. Dit kan betekenen dat bepaalde leden van de klasse publiek moeten worden gemaakt om toegankelijk te zijn vanuit een extensie (wat kan leiden tot leaky abstractions). Desalniettemin blijft de systematische aanpak van berichten verzenden behouden, terwijl er een fijnmazigere kwalificatie van de ontvanger mogelijk is.

Guarded methods

De laatste benadering is waarschijnlijk de meest ideologische, omdat de definitie van de methode binnen de klasse blijft. Er worden geen abstracties doorbroken. Dit is het idee achter guarded methods: de mogelijkheid om beperkingen op de generieke parameter toe te voegen op het niveau van de methode-definitie. In een imaginaire syntaxis (deze code compileert omdat hij niet syntactisch ongeldig is, maar produceert niet het beoogde effect):

class MyList<A> : ArrayList<A>() {
    fun length() = size
    fun <B> MyList<MyList<B>>.flatten() =
        // Implementatie van flatten
}

Hoewel dit niet significant anders lijkt dan klassieke extension methods, lost het alle eerder genoemde problemen op:

• We kunnen de ontvanger preciezer karakteriseren dan in een normale methode.
• We doorbreken het reguliere berichtenverkeer niet.
• We profiteren nog steeds van beschikbare leden (waardoor we representaties niet blootstellen).

Hoewel guarded methods noodzakelijk lijken, zijn er naar mijn weten geen mainstream talen die hun definitie toestaan. Gelukkig is het in OCaml mogelijk om ze te encoderen.

OOP/FP-symmetrie: theorie en praktijk

Omdat guarded methods zeldzaam zijn in populaire programmeertalen, ontdekte ik hun bestaan onlangs tijdens het lezen van de slides van de presentatie "The Object-Oriented/Functional-Programming symmetry: theory and practice" door Gabriel Scherer.

Ik raad deze presentatie aan; deze toont een symmetrie tussen de instrumenten van statisch getypeerde functionele programmering en objectgeoriënteerd programmeren. De presentatie is uitgebreid, toegankelijk en relatief onbevooroordeeld over de voor- en nadelen van beide benaderingen. Hoewel het niet tijdens de presentatie zelf aan bod kwam (tijd is vaak de vijand van een spreker), bevatten de slides een hele sectie over guarded methods.

Het oorspronkelijke voorbeeld biedt een symmetrische observatie tussen de implementatie van de flatten-functie in een klassieke functionele stijl:

type 'a list = ...
let rec length : 'a list -> int = ...
let rec concat : 'a list -> 'a list -> 'a list = ...
let rec flatten : 'a list list -> 'a list = function
| [] -> []
| x::xs -> x @ flatten xs

En de implementatie van een flatten-methode in een objectgeoriënteerde wereld. De vraag is: welk type moet flatten hebben?

class type ['a] olist = object
  method length : int
  method concat : 'a olist -> 'a olist
  method flatten : ???
end

Scherer stelt daarom deze syntaxis voor, die een guard op de flatten-methode impliceert:

method flatten : 'b olist with 'a = 'b olist

Deze syntaxis maakt het mogelijk om een guarded method te beschrijven en zou gegeneraliseerd kunnen worden als: method methodenaam : returntype with generictype = othertype. Net als bij substituties in modules zouden we beperkingen op meerdere generics kunnen specificeren met and. Bijvoorbeeld: method foo : string with 'a = string and b = int voor een klasse geparametriseerd door twee types: class ['a, 'b] t.

Daarnaast zou deze syntaxis het mogelijk maken om specifieke behaviors elegant te definiëren. Voor ons olist-type zouden we bijvoorbeeld een sum-methode kunnen aanbieden als de elementen van de lijst integers zijn:

class type ['a] olist = object
  method length : int
  method concat : 'a olist -> 'a olist
  method flatten : 'b olist with 'a = 'b olist
  method sum : int with 'a = int
end

Dit klinkt fantastisch, maar helaas is deze syntaxis niet beschikbaar in OCaml. Gelukkig kunnen we dit encoderen met een paar kleine hulpmiddelen.

Guarded Methods in OCaml

Om guarded methods te encoderen, heb ik contact opgenomen met Florian Angeletti (ook bekend als Octachron). Ons doel is om toe te staan dat er aan bepaalde methoden een beperking wordt toegevoegd, zodat ze alleen toegankelijk zijn als het type van de ontvanger daaraan voldoet. Zonder de syntaxis van de taal aan te passen, kan het modelleren van een beperking bestaan uit het leveren van een extra parameter die deze afdwingt. Met andere woorden: we willen bewijs leveren.

Een type equality witness leveren

Sinds de introductie van generalized algebraic data types (GADTs) in de taal, is er een vrij eenvoudige manier om een type equality witness te definiëren:

type (_, _) eq =
| Refl : ('a, 'a) eq

Het eq-type heeft slechts één constructor: Refl. Hiermee kunnen type-gelijkheden worden gerepresenteerd die niet door de type-checker bekend zijn. Omdat we alleen Refl-waarden kunnen construeren die twee gelijke types associëren, garandeert het instantiëren van Refl binnen een scope dat die types equivalent zijn. Bijvoorbeeld:

type other_int = int
let _ : (int, other_int) eq = Refl
(* Nu hebben we een bewijs van [int = other_int]. *)

Dit voorbeeld is enigszins kunstmatig omdat de compiler hier perfect weet dat int = other_int. Er zijn echter gevallen waarin de compiler dit niet kan weten, bijvoorbeeld wanneer data tijdens runtime wordt geleverd of wanneer de representatie van het type verborgen is door abstractie. Het belangrijkste is: als we een Refl-waarde kunnen construeren, hebben we de garantie dat twee syntactisch verschillende types in feite gelijk zijn.

Beperken met eq

Terug naar het voorbeeld van een object-API voor een lijst. Hier is de interface:

class type ['a] obj_list =
object ('self)
  method length : int
  method append : 'a list -> 'a obj_list
  method uncons : ('a * 'self) option
  method flatten : ???
end

Om een type te geven aan flatten, willen we opleggen dat 'a (de typeparameter van de obj_list-klasse) een lijst is. We willen dus een bewijs dat 'a van het type 'b list is; een garantie dat 'a en 'b list gelijk zijn. De oplossing is simpel: vereis dat er een waarde van het type ('a, 'b list) eq wordt meegegeven:

method flatten : ('a, 'b list) eq -> 'b list

De interface obj_list implementeren

De eerste methoden (length, append en uncons) zijn eenvoudig te implementeren:

let my_list (list : 'a list) =
object (self : 'a obj_list)
  val l = list
  method length = List.length l
  method append x = {<l = List.append l x>}
  method uncons = match l with [] -> None | x :: xs -> Some (x, {<l = xs>})
  method flatten = ???
end

Nu richten we ons op flatten. We doorlopen de lijst recursief en voegen elk element samen met het vorige. De truc zit hem in het instantiëren van Refl om te bewijzen dat 'a = 'b list.

method flatten : 'b. ('a, 'b list) eq -> 'b list =
  let rec aux : type a b. a #obj_list -> (a, b list) eq -> b list =
    fun list witness -> match list#uncons with
    | None -> []
    | Some (head_list, xs) ->
        let flatten_list : b list =
          let Refl = witness in head_list
        in flatten_list @ aux xs witness
  in aux self

Een guarded method sum toevoegen

Laten we nu een sum-methode toevoegen die de som van een lijst integers produceert. Eerst voegen we sum toe aan onze interface met de beperking dat het typeparameter int moet zijn:

class type ['a] obj_list =
object ('self)
  method length : int
  method append : 'a list -> 'a obj_list
  method uncons : ('a * 'self) option
  method flatten : ('a, 'b list) eq -> 'b list
  method sum : ('a, int) eq -> int
end

Vervolgens implementeren we de sum-methode met behulp van de fold_left-functie:

method sum : ('a, int) eq -> int =
  let aux : type a. a list -> (a, int) eq -> int =
    fun list Refl -> List.fold_left (fun acc x -> acc + x) 0 list
  in aux l

De implementatie van sum is logisch eenvoudiger dan die van flatten omdat het geen extra typevariabelen introduceert. We kunnen de methoden nu testen: we roepen flatten aan op een object van type 'a list objlist en sum op een object van type int objlist.

let a = my_list [ [ 1 ]; [ 2 ]; [ 3 ] ]
let _ = assert ([ 1; 2; 3 ] = a#flatten Refl)

let b = my_list [ 1; 2; 3; 4 ]
let _ = assert (10 = b#sum Refl)

Als we een guarded method proberen aan te roepen met het verkeerde type — bijvoorbeeld sum uitvoeren op lijst a (die van het type 'a list obj_list is) — zal het programma niet compileren:

1 | let _ = a#sum Refl
^^^^
Error: This expression has type (int list, int list) eq
but an expression was expected of type (int list, int) eq
Type int list is not compatible with type int

Dit is exact het gewenste gedrag. We kunnen nu methoden definiëren die het type van de ontvanger beperken middels een type equality witness.

Conclusie

Het is verrassend dat guarded methods niet aanwezig zijn in alle statisch getypeerde OOP-talen, aangezien ze meer methoden mogelijk maken terwijl de berichten-semantiek behouden blijft. Ik ben mij niet bewust van talen die hiervoor native syntactische ondersteuning bieden, hoewel ik via Nicolas Rinaudo vernam dat Scala een vergelijkbare encoding gebruikt, maar waarbij de type equality witness impliciet wordt geleverd. Dit maakt de aanroep lichter omdat de gebruiker niet handmatig Refl hoeft te verzenden.

Hoewel de encoding in OCaml enigszins zwaar is, stelt het expliciet manipuleren van een type equality witness ons in staat om guarded methods te implementeren. Is het nuttig? Aangezien OOP zelden wordt aangemoedigd in OCaml, waarschijnlijk niet, maar het was een leuke manier om een concreet en praktisch gebruiksvoorbeeld voor equality witnesses te presenteren.