Compile-time afhankelijke typen

Ik werk aan Syl, een taal die erop gericht is om compile-time berekeningen te coderen in een modaal typesysteem. Syl is primair geïnspireerd door het werk van András Kovács over two-level type theory, evenals de plannen voor OxCaml. De Syl-compiler is te vinden op GitHub.

Modi

In Syl heeft elke waarde, naast een type, een modus (mode). Modi beschrijven eigenschappen van waarden die onafhankelijk zijn van hun typen. Zo gebruikt OxCaml modi om aan te geven of een waarde uniek eigendom is (uniquely owned), beschrijfbaar is, naar een andere thread gestuurd mag worden, enzovoort.

Syl heeft twee modus-assen: staticiteit (staticity) en erasure.

• Staticiteit: Een waarde kan static (statisch) of dynamic (dynamisch) zijn. Een statische waarde is bekend tijdens het compileren; een dynamische waarde is dat mogelijk niet.
• Erasure: Een waarde kan erased (gewist) of unerased (niet gewist) zijn. Een unerased waarde is bekend tijdens runtime; een erased waarde is dat mogelijk niet.

Literalen zijn bijvoorbeeld static unerased, aangezien ze duidelijk bekend zijn tijdens zowel compile-time als runtime. Je kunt dit controleren door een modus-annotatie te schrijven:

let x = 0 @ static unerased;;

Elke modus-as heeft een sub-moding relatie. Als je een statische waarde hebt, is het veilig om te 'vergeten' dat deze bekend is tijdens het compileren en deze dus als dynamisch te behandelen. Op dezelfde manier kan een unerased waarde worden behandeld als erased. Modus-annotaties mogen de modus "verzwakken", maar niet "versterken":

let x = 0 @ dynamic;;
let y = x @ static;;
^^^^^^^^^^
Error: Expected a static expression, but got dynamic.

Zoals verwacht zorgt vertakkingen op basis van een dynamische waarde ervoor dat het resultaat dynamisch is:

let x = 0 @ dynamic;;
let y = (if x == 0 then 1 else 2) @ static;;
^^^^^^^^^^^^^^^^
Error: Expected a static expression, but got dynamic.

Zolang functies geen dynamische waarden vastleggen (capture) of daarop vertakken, behouden ze de staticiteit.

let f = fn (x : int) -> x;;
let x = (f 0) @ static;;
let y = (f (1 @ dynamic)) @ static;;
^^^^^^^^^^^^^^^^^
Error: Expected a static expression, but got dynamic.

Functies die erased waarden retourneren zijn zelf erased en kunnen daarom niet tijdens runtime worden aangeroepen:

let f = fn (x : unit) -> 1 @ erased;;
let g = f @ unerased;;
^
Error: Expected an unerased expression, but got erased.

Toepassing van modus-informatie

Wanneer een waarde bekend is tijdens het compileren, kan de omringende code worden gemonomorfiseerd (monomorphized). Functies met statische parameters maken gebruik van dit feit:

let f = fn (static x : bool) -> print_bool x;;

Wanneer we f x aanroepen, vereist de compiler dat zowel f als x de modus static hebben. Als dat zo is, selecteert de compiler een specifieke implementatie van f die is gespecialiseerd voor de waarde van x. Concreet zou f true een functie aanroepen die print_bool true hardcoded bevat, en hetzelfde geldt voor f false.

In het bovenstaande voorbeeld printen we de waarde van x tijdens runtime, dus moet deze unerased zijn. Dat is vaak onnodig: als x alleen bepaalt hoe het lichaam van f moet worden gecompileerd, kan x erased zijn:

let f = fn (erased x : bool) -> if erased x then print_int 0 else print_int 1;;

Hier impliceert erased ook static, dus zal f worden gespecialiseerd op basis van x. De if erased expressie accepteert een statische erased conditie en is gegarandeerd tijdens compile-time opgelost. Daarom verwijst f true naar een thunk met het lichaam print_int 0, en likewise voor f false.

Afhankelijke typen

Op zichzelf laten de static en erased modi ons expliciet vragen om optimalisaties op basis van specialisatie, maar ze geven ons geen afhankelijke typen. Functies met statische argumenten doen dat wel:

let f = fn (erased x : bool) -> if erased x then 0 else true;;

Hier stelt if erased ons in staat om een integer te retourneren als x waar is, en een boolean in het andere geval. Hierdoor heeft f een afhankelijk functietype (dependent function type), dat codeert hoe het resultaattype afhangt van de waarde van de input:

f : erased bool as x -> if erased x then int else bool

Let op dat ty as name het argument een naam geeft voor gebruik in het resultaat. Applicaties kunnen vervolgens het correcte resultaattype bepalen door het type van f te evalueren:

let x = (f true) : int;;
let y = (f false) : bool;;

Er is geen aparte type-grammatica: type-formers zoals -> en type-annotaties zijn normale expressies. int en bool zijn simpelweg erased waarden van het type type, en abstractie over deze waarden geeft ons polymorfisme:

let id = fn (erased t : type) -> fn (x : t) -> x;;
let x = id int 0;;
let y = id bool true;;

Zoals eerder gezien, worden functies met statische argumenten gemonomorfiseerd. Tijdens runtime verwijst id int naar een identiteitsfunctie die direct op integers opereert, en hetzelfde geldt voor id bool. Dat wil zeggen dat Syl tijdens compile-time afhankelijk getypeerd is (dependently typed) en tijdens runtime simpel getypeerd (simply typed).

Constructies die de vorm van het runtime-programma bepalen, vereisen statische informatie. Typen zijn altijd erased, dus het runtime-programma kan typen niet inspecteren. Syl implementeert dependent typechecking op een vergelijkbare manier als bestaande talen, dus we zullen dit niet in detail bespreken. De relatie tussen typen en proposities in Syl verschilt echter van talen als Lean, Rocq en Agda.

Bewijzen (Proofs)

In het bijzonder ondersteunt Syl algemene recursie in compile-time berekeningen en staat het type type type toe. Het toestaan van een van deze functies impliceert dat het construeren van een expressie van type t niet bewijst dat de propositie die overeenkomt met t waar is.

Bijvoorbeeld, we kunnen een functie implementeren die ogenschijnlijk een waarde van elk willekeurig type retourneert:

let magic =
fn (erased t : type) ->
fun loop (_ : unit) : t = loop () in
loop ()
;;

Let op dat magic ook geïmplementeerd zou kunnen worden met type : type via de paradox van Girard. Ondanks dat deze functie het type erased type as t -> t heeft, produceert deze nooit daadwerkelijk een waarde—het is een oneindige lus. Het type beschrijft wat magic t zou produceren als het voltooid zou worden, maar garandeert niet dat dit gebeurt.

Hoewel dit typesysteem niet geschikt zou zijn voor een taal voor het bewijzen van stellingen (theorem proving), sluit dit typeveiligheid of zelfs nuttige bewijzen niet uit. Het heeft twee praktische consequenties:

1. Functies die worden gebruikt in type-level berekeningen kunnen divergeren, waardoor typechecking niet beslisbaar (decidable) is.
2. Functies lossen geen universeel gekwantificeerde claims op, dus de compiler moet alle applicaties die bewijzen produceren evalueren voordat hij op hun resultaten kan vertrouwen.

In ruil hiervoor hebben we geen totality checker nodig (alle statische expressies mogen in typen worden gebruikt) of complexe universe machinery (type-level programmeren is intuïtief).

Totaliteit (Totality)

Omdat Syl een programmeertaal is, is het doel van compilatie het produceren van een runtime-artefact dat voldoet aan de invarianten die door het typesysteem worden afgedwongen. Daarom geven we alleen om aanroepen van afhankelijke functies die daadwerkelijk plaatsvinden tijdens de compilatie—het is acceptabel als andere functies divergeren.

Toch is het een slechte gebruikerservaring als de typechecking tijdens het ontwikkelen vastloopt, dus implementeert Syl ook fuel limits (brandstoflimieten):

fun f (erased _ : unit) : erased type = f ();;
^
Error: Recursion limit reached.
let x = 1 : f ();;

Het vermijden van totaliteit betekent ook dat Syl expliciete partiële functies kan ondersteunen tegen geringe extra kosten. Hier is bijvoorbeeld een divisiefunctie die statisch controleert of de divisor niet nul is:

let safe_div =
fn (static d : int) ->
if erased d != 0
then fn (x : int) -> x / d
else unreachable
;;

Het trefwoord unreachable stelt dat een vertakking niet voorkomt in het runtime-programma. Tijdens dependent typechecking wordt de else-tak behandeld als een bottom value, waardoor er geen beperkingen worden opgelegd aan de then-tak. Echter, als de else-tak wordt bereikt tijdens het instantiëren van safe_div, krijgen we een fout:

...
else unreachable
^^^^^^^^^^^
Error: Unreachable reached.
;;
let x = safe_div 0 1;;

Het toestaan van partiële functies opent de deur naar onbegrijpelijke C++-stijl template instantiation fouten. Gelukkig betekent expliciete partialiteit dat we gebruikers kunnen verplichten foutmeldingen te leveren in niet-ondersteunde gevallen. In combinatie met het gebrek aan duck-typing tijdens compile-time, denk ik dat Syl de meeste nadelen kan vermijden.

Voorbeelden

Getypeerde Interpreter

Het volgende programma vereist niet de volledige kracht van afhankelijke typen—het wordt vaak gebruikt als motiverend voorbeeld voor GADTs in OCaml of Haskell—maar ik denk dat de vergelijking illustratief is.

We beginnen met het definiëren van een variant om als index te gebruiken:

let sort = variant { int, bool };;

Notitie: Zowel sort als de constructoren sort.int/sort.bool zijn normale waarden. Variants zijn unboxed.

Dan een functie om een sort om te zetten naar het overeenkomstige type:

fun value (erased s : sort) : erased type =
match erased s {
.int -> int,
.bool -> bool,
}
;;

Notitie: Net als if erased, staat match erased een erased scrutinee toe en wordt dit tijdens compile-time opgelost.

Vervolgens een geïndexeerd expressietype. Het type is letterlijk een recursieve functie met een sort-argument:

fun expr (erased s : sort) : erased type =
match erased s {
.int ->
variant {
lit : int,
add : &(expr sort.int ^ expr sort.int),
if_ : &(expr sort.bool ^ expr sort.int ^ expr sort.int),
},
.bool ->
variant {
lit : bool,
eq : &(expr sort.int ^ expr sort.int),
},
}
;;

Notitie: & representeert een indirectie. ^ is de tuple-type former.

Tot slot de interpreter:

fun eval (erased s : sort) : expr s -> value s =
fn (e : expr s) ->
match erased s {
.int ->
match e {
.lit n -> n,
.add &(left, right) -> eval sort.int left + eval sort.int right,
.if_ &(condition, yes, no) ->
if eval sort.bool condition then eval sort.int yes else eval sort.int no,
},
.bool ->
match e {
.lit b -> b,
.eq &(left, right) -> eval sort.int left == eval sort.int right,
},
}
;;

Functies met statische argumenten worden gemonomorfiseerd en erased vertakkingen worden geëlimineerd, waardoor de interpreter compileert naar dezelfde structuur als je zou verwachten van template specialization in C++.

Vector met lengte-index

Waarschuwing: de syntax hier moet nog sterk worden verbeterd.

Correcte afhankelijke typen stellen ons in staat om de lengte van lijsten in het typesysteem te coderen. Laten we een append-functie schrijven waarvan het type aantoont dat de outputlengte de som is van de inputlengtes. Aangezien Syl geen tools heeft voor redeneren over signed, fixed-width integers, definiëren we ons eigen Peano nat type:

let nat =
fun nat (erased _ : unit) : erased type =
variant { zero, succ : &(nat ()) }
in
nat ()
;;

Notitie: er is geen let rec, dus we definiëren nat via een recursieve functie.

Dan een optelfunctie voor nats:

fun add (static nm : nat ^ nat) : nat =
match static nm {
(.zero, m) -> m,
(.succ &n, m) -> nat.succ box (add (n, m)),
}
;;

Notitie: match static is als match erased, maar wist de inhoud van de scrutinee niet. We zouden overal erased moeten gebruiken, maar variant-constructoren zijn nog niet modus-polymorf. Als alle nats erased waren, zou de box indirectie ook niet nodig zijn.

Nu de unboxed, lengte-geïndexeerde lijst:

fun vec (erased t : type) : erased (erased nat -> erased type) =
fn (erased n : nat) ->
match erased n {
.zero -> variant { nil },
.succ &n -> variant { cons : t ^ vec t n },
}
;;

En tot slot de append-functie. Cruciaal is dat de compiler in staat is om af te leiden dat de .cons case het juiste return-type heeft door add en vec uit te vouwen:

fun append
(erased t : type) : (static nat as n
-> static nat as m
-> vec t n
-> vec t m
-> vec t (add (n, m))) =
fn (static n : nat) ->
fn (static m : nat) ->
fn (v1 : vec t n) ->
fn (v2 : vec t m) ->
match static n {
.zero -> v2,
.succ &n_minus_1 ->
match v1 {
.cons (x, xs) -> (vec t (add (n, m))).cons (x, append t n_minus_1 m xs v2),
},
}
;;

Notitie: dit is vrij omslachtig omdat we geen n-aire functiesyntax hebben. We moeten ook het vec type volledig kwalificeren waar .cons vandaan komt, omdat dit nog niet wordt afgeleid.

Zoals hierboven vermeld, zijn alle lengtes bekend tijdens compile-time, dus heeft het runtime-programma semantiek die vergelijkbaar is met een constexpr lengteberekening in C++.

Uitbreidingen

Veel nuttige taalfuncties kunnen worden gedefinieerd in gebruikerscode met behulp van compile-time afhankelijke typen. Hier zijn enkele veelbelovende (gedeeltelijk geïmplementeerde) voorbeelden.

Higher-Kinded Types

Higher-kinded types zijn simpelweg erased functies op typen. Je kunt erover abstraheren zoals over alles:

singleton :
erased (erased type -> erased type) as container ->
erased type as element ->
element ->
container element

Dit voorbeeld werkt al, maar zoals geschreven kun je met container alleen maar applicaties uitvoeren. We hebben ook de mogelijkheid nodig om interfaces te specificeren die typen en waarden verbinden.

Modules en Functoren

Zodra Syl OxCaml-stijl modaliteiten heeft, kun je erased/dynamic waarden nesten in unerased/static waarden. Dan kunnen afhankelijke records de plaats innemen van ML-stijl modules:

let container = record {
ty : erased type -> erased type @@ erased,
create : erased type as element -> element -> ty element,
};;

@@ erased impliceert dat alle gebruikt van container.ty een erased waarde zien, ongeacht de erasure van de container. Nu kunnen we singleton een implementeerbaar type geven:

singleton :
static container as container ->
erased type as element ->
element ->
container.ty element

Op dezelfde manier kunnen ML-stijl functors worden geïmplementeerd als afhankelijke functies:

fun pair (static c : container) : container = {
ty = (fn (erased element : type) ->
c.ty element ^ c.ty element),
create = (fn (erased element : type) ->
fn (e : element) ->
c.create element e, c.create element e),
};;

Met afgeleide argumenten zouden records de meeste voordelen van typeclasses of traits kunnen bieden.

Imports

We kunnen zelfs statische berekeningen gebruiken om te beschrijven hoe programma's met meerdere bestanden worden opgebouwd. De compiler hoeft alleen de volgende functies te leveren:

importsig : erased string -> erased type import : erased string as path -> importsig path

Als we definities op bestandsniveau behandelen als record-velden, kan import_sig een record-type voor een bestand afleiden en kan import een waarde van dat type produceren. Sterker nog, deze functies zouden net zo gemakkelijk code-strings kunnen accepteren, waardoor we code tijdens compile-time kunnen genereren.

Reflectie

Syl heeft al rudimentaire reflectie via de ingebouwde repr-functie, die metadata voor een type retourneert:

fun print_ty (erased t : type) : unit =
match erased repr t {
.unit -> print "unit",
.bool -> print "bool",
.int -> print "int",
_ -> unreachable,
}
;;

Deze faciliteit zou eenvoudig kunnen worden uitgebreid om de structuur van typen te inspecteren, wat vervolgens kan worden gebruikt om getypeerde Rust- of OCaml-stijl derivers te implementeren.

Gebruikersgedefinieerde Layouts

Hoewel dit speculatief is, denk ik dat we de runtime-layouts van typen tijdens compile-time moeten kunnen definiëren en manipuleren. Met zo'n functie zouden gebruikers veilig interoperabele niche optimizations kunnen beschrijven. Dit zou ook een notie van "niet-adresseerbare" velden vereisen, waarbij geen pointers naar deze velden kunnen worden gemaakt.

Overig

Het ontwerp van Syl is nog lang niet voltooid. In het bijzonder zijn er nog oplossingen nodig voor modus-polymorfisme, lifetimes, lineariteit, impliciete parameters en bewijzen. De compiler heeft incrementele compilatie, nuttige foutrapportages en een LLVM-backend nodig.

***

Voetnoten

1. In de literatuur worden modale typesystemen gepresenteerd in termen van modaliteiten. We beschrijven modi zoals ze verschijnen in OxCaml, maar je kunt dit vertalen door alle waarden te beschouwen als static unerased totdat ze worden vastgelegd onder een dynamic of erased modaliteit.
2. Momenteel heeft staticiteit het modale axioma K, wat statische functies toestaat om te opereren op dynamische argumenten. Ik ben van plan de impliciete applicatieregel te vervangen door modus-polymorfisme, wat ook erasure kan behandelen.
3. Dit is het kernidee van Staged Compilation with Two-Level Type Theory, hoewel het niet als een modaal typesysteem wordt gepresenteerd.
4. Dit idee wordt formeel verkend in Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems.
5. Syl heeft nog geen gelijkheidstypen (equality types), maar zodra dit er zijn, zal erasure een natuurlijk mechanisme bieden om bewijs-producerende berekeningen af te dwingen wanneer hun resultaten nodig zijn. Bijvoorbeeld: assert erased b zou b = true in de bewijscontext kunnen vaststellen door te controleren of het reduceert tot true.
6. Dit is geen eerlijke vergelijking, maar het is beter! C++ / Syl.
7. Er bestaan ideeën over hoe dergelijke modaliteiten afleidbaar te maken, maar ik begrijp ze nog niet.