Introduzione alle Generics in Go
2023/04/17
Questo articolo è la versione in forma scritta del talk con lo stesso nome tenuto alla DevFest di Pisa il 2023/04/01
gogenericsdevfestgdgtalklang-it

Introduzione alle Generics in Go

line pen drawing conference blackboard

Questo articolo è tratto da un talk tenuto alla DevFest di Pisa del 1 Aprile 2023 organizzata dal GDG. Le slide originali e tutto il codice derivato da questo talk si trovano in questo repo su GitHub. Per info quasi tutta la prima parte (inclusi i diagrammini) è tratta dall’articolo https://go.dev/blog/intro-generics.

Nella versione 1.18 del Go hanno finalmente introdotto le generics, questo è stato uno dei cambiamenti più grossi al linguaggio dal primo rilascio nel mondo open source.

Il problema

Prima dell’introduzione delle generics in Go se uno voleva scrivere una funzione per calcolare il minimo tra due numeri ad esempio come

func Min(x, y int) int {
    if x < y {
        return x
    }

    return y
}

e voleva utilizzarla anche per altri tipi serviva copia-incollarla cambiando il nome e modificando il tipo in base a quello che uno voleva usare.

func MinInt8(x, y int8) int8 {
    if x < y {
        return x
    }

    return y
}

func MinInt16(x, y int16) int16 {
    if x < y {
        return x
    }

    return y
}

func MinFloat32(x, y float32) float32 {
    if x < y {
        return x
    }

    return y
}

Come possiamo notare in questo caso l’implementazione della funzione è sempre la stessa e non dipende dal tipo specifico che stiamo utilizzando. Quindi seguendo il principio DRY sarebbe meglio non stare a ricopiare ogni volta lo stesso codice.

...
if x < y {
    return x
}

return y
...

Alternativamente un’altra soluzione pre-generics sarebbe quella di far prendere parametri di tipo any e mettere dentro la funzione degli switch sul tipo. In alcuni casi questo potrebbe essere ragionevole ma spesso non è molto pulito come nel caso della funzione minimo, specialmente se vogliamo scrivere codice generico per tipi primitivi.

Inoltre se una funzione prende input di tipo any perdiamo tutta la type-safety a compile-time ed appesantiamo il lavoro da fare a runtime (senza parlare che ora dobbiamo passare in giro dei puntatori).

Un altro modo è di usare go generate con alcuni tool che generano tutte le varianti di una funzione. Questa tecnica è già più ragionevole ma complica il modo di compilare il progetto.

Soluzione: Le Generics

Ormai già da qualche versione possiamo scrivere la seguente funzione

Type Parameters

import "golang.org/x/exp/constraints"

func Min[T constraints.Ordered](x, y T) T {
    if x < y {
        return x
    }
    return y
}

Vedremo meglio più avanti cosa significa di preciso questa notazione, in breve T è il nuovo tipo generico che stiamo introducendo, constraints.Ordered è il vincolo che stiamo imponendo su T.

Possiamo utilizzare la funzione in due modi, o chiamando la funzione e specificando il type parameter esplicitamente come segue

var a, b int = 0, 1
Min[int](a, b)
...
var a, b float32 = 3.14, 2.71
Min[float32](a, b)

oppure in molti casi possiamo sottintenderlo e scrivere direttamente

var a, b int = 0, 1
Min(a, b)
...
var a, b float32 = 3.14, 2.71
Min(a, b)

Type Sets

Più precisamente la notazione per introdurre una generics è della forma [T Vincolo1, R interface{ Method(), ... }, ...], possiamo introdurre tutti i tipi parametrici che vogliamo scrivendo prima il nome del type parameter e poi il vincolo sotto forma di alias o per esteso scrivendo interface{ <vincoli...> }.

In particolare tutti i vincoli sono delle interfacce del Go. In realtà è stata estesa la sintassi delle interfacce del Go per poter ammettere dei cosi detti type sets.

Un modo per pensare le interfacce in Go è attraverso il concetto di method set, un tipo soddisfa un’interfaccia se il suo method set contiene il method set definito dall’interfaccia.

go method sets

Un modo alternativo o duale di vedere la cosa è di pensare al type set generato da un’interfaccia, ovvero all’insieme di tutti i tipi (in astratto) che soddisfano quell’interfaccia. A quel punto dato un tipo per vedere se soddisfa o meno l’interfaccia basta vedere se è o meno nel type set dell’interfaccia.

go type sets 1

La nuova sintassi che è stata introdotta per le interfacce è la seguente e ci permette di “forzare” i tipi di base che sono nel type set di un’interfaccia.

go type sets 2

Ad esempio in questo caso l’interfaccia se usata come vincolo per una generics ammetterà solo questi tre tipi.

In particolare è anche stato aggiunto un po’ di zucchero sintattico per quando scriviamo i vincolo

Vediamo un ad esempio come scrivere una funzione generica sui tipi numerici floating point.

func Somma[T float32|float64](x, y T) T {
    return x + y
}

Però in qualche situazione potremmo avere ad esempio un tipo sinonimo di float64 come

type Liter float64

e di base non possiamo usare la funzione di sopra con questo tipo “sinonimo” perché il tipo Liter e float64 sono effettivamente tipi diversi e quindi Liter non è compatibile con float32|float64.

var a, b int = 1, 2
Somma(a, b) // Ok

var a, b Liter = 1, 2
Somma(a, b) // Errore

Se però (come in questo caso) vogliamo rilassare il vincolo possiamo aggiungere una ~ prima del nome del tipo primitivo nel type set

func Somma[T ~float32|~float64](x, y T) T {
    return x + y
}
type Liter float64
var a, b int = 1, 2
Somma(a, b) // Ok

var a, b Liter = 1, 2
Somma(a, b) // Ok

In realtà questo vincolo è già definito nel pacchetto constraints usato prima

package constraints

...

type Float interface {
    ~float32 | ~float64
}

...

ed in realtà anche constraints.Ordered si trova qui ed è definito come segue

package constraints

...

type Ordered interface {
    Integer | Float | ~string
}

type Float interface {
    ~float32 | ~float64
}

type Integer interface {
    Signed | Unsigned
}

type Signed interface {
    ~int | ~int8 | ~int16 | ~int32 | ~int64
}

type Unsigned interface {
    ~uint | ~uint8 | ~uint16 | ~uint32 | ~uint64 | ~uintptr
}

...

(essenzialmente sono andati a vedere secondo la spec del Go quali sono i tipi che supportano < e > e li hanno hardcodati dentro Ordered)

Tipi Generici

Vediamo ora come creare dei tipi generici, ad esempio possiamo definire uno stack come segue

type Stack[T any] []T

Per scrivere i metodi possiamo fare come segue, reintroducendo il tipo generico nel receiver del metodo. In particolare quando definiamo un metodo su un tipo generico dobbiamo reintrodurre il tipo T e questo ci permette di utilizzarlo ovunque nello scope della funzione.

func (s *Stack[T]) Push(value T) {
    *s = append(*s, value)
}

func (s Stack[T]) Peek() T {
    return s[len(s)-1]
}

func (s Stack[T]) Len() int {
    return len(s)
}

Vediamo ora il metodo (Stack[T]).Pop() che è leggermente più interessante.

Decidiamo che vogliamo che ritorni <elemento in cima>, true se lo stack non era vuoto oppure 0, false altrimenti .

func (s *Stack[T]) Pop() (T, bool) {
    items := *s

    if len(items) == 0 {
        var zero T
        return zero, false
    }

    newStack, poppedValue := items[:len(items)-1], items[len(items)-1]
    *s = newStack

    return poppedValue, true
}

Il primo “pattern” interessante che notiamo con le generics è questo di var zero T, in Go quando definiamo una variabile in questo modo verrà automaticamente inizializzata a zero quindi possiamo usare questo trick per ritornare il valore di default per un tipo generico che non possiamo direttamente inizializzare.

Possiamo estrarre questo pattern direttamente in una funzione utility come segue

func Zero[T any]() T {
    var zero T
    return zero
}

Per ora ci tocca definire sempre a mano la variabile var zero T se vogliamo utilizzare il valore di default per un certo tipo però questo problema è già stato riscontrato da altre persone e già si sta pensando a delle soluzioni.

Pattern: Tipi Contenitore

Tipi generici nativi

Fin dal principio il Go ha avuto i seguenti tipi generici baked-in ovvero

Però c’è sempre stato il problema che non era possibile definire funzioni generiche per questi tipi, anzi era idiomatico in Go ripetere sempre l’implementazione imperativa di certe operazioni molto comuni come trovare un elemento in uno slice.

Ora finalmente possiamo definirle in modo generico ed in realtà è già stato creato il pacchetto golang.org/x/exp/slices che contiene una manciata di queste funzioni utili

ed invece golang.org/x/exp/maps per le mappe in Go

Strutture dati generiche

Stanno anche nascendo librerie con già molte strutture dati generiche come ad esempio https://github.com/zyedidia/generic (che ha già circa 1K stelle su su GitHub)

Alcuni Anti-Pattern

Utility HTTP

Diciamo che vogliamo scrivere una funzioni di utility faccia la decodifica di una richiesta HTTP e validi anche il contenuto della richiesta usando l’interfaccia Validator come segue

// library code
type Validator interface {
    Validate() error
}

func DecodeAndValidateJSON[T Validator](r *http.Request) (T, error) {
    var value T
    if err := json.NewDecoder(r.Body).Decode(&value); err != nil {
        var zero T
        return zero, err
    }

    if err := value.Validate(); err != nil {
        var zero T
        return zero, err
    }

    return value, nil
}

Da utilizzare come uno si aspetti (giusto un esempio veloce, non serve concentrarsi troppo su tutto questo codice)

// client code
type FooRequest struct {
    A int    `json:"a"`
    B string `json:"b"`
}

func (foo FooRequest) Validate() error {
    if foo.A < 0 {
        return fmt.Errorf(`parameter "a" cannot be lesser than zero`)
    }
    if !strings.HasPrefix(foo.B, "baz-") {
        return fmt.Errorf(`parameter "b" has wrong prefix`)
    }

    return nil
}
foo, err := DecodeAndValidateJSON[FooRequest](r)
if err != nil {
    http.Error(w, err.Error(), http.StatusInternalServerError)
    return
}

In realtà in questo caso non serve veramente introdurre un type parameter, potevamo scrivere già questa utility senza generics passando una variabile di tipo any

func DecodeAndValidateJSON(r *http.Request, target Validator) error {
    err := json.NewDecoder(r.Body).Decode(target)
    if err != nil {
        return err
    }

    if err := target.Validate(); err != nil {
        return err
    }

    return nil
}
var foo FooRequest
if err := DecodeAndValidateJSON(r, &foo); err != nil {
    http.Error(w, err.Error(), http.StatusInternalServerError)
    return
}

Che si comporta esattamente come prima ed è leggermente più semplice concettualmente.

Intuitivamente quello che fa il compilatore del Go quando c’è una funzione generica è di copia-incollare la funzione con tipi parametrici per ogni tipo nel chiamante. Quindi ci potremmo chiedere se effettivamente sia comunque più performante utilizzare le generics nel caso precedente. Cambiamo esempio per vedere meglio:

Confronto: Generics vs Interfacce

Consideriamo le due seguenti funzioni

func WriteOneByte(w io.Writer, data byte) {
    w.Write([]byte{data})
}

...

d := &bytes.Buffer{}
WriteOneByte(d, 42)
func WriteOneByte[T io.Writer](w T, data byte) {
    w.Write([]byte{data})
}

...

d := &bytes.Buffer{}
WriteOneByte[*bytes.Buffer](d, 42)

A primo impatto potremmo pensare che la prima sia più lenta perché stiamo passando una variabile di tipo *bytes.Buffer ad una funzione che prende un’interfaccia io.Writer quindi già in qualche modo ci dovrebbe essere un primo passaggio di conversione. Inoltre quando dentro la funzione chiamiamo .Write(...) in qualche modo il Go dovrà passare dalla vtable per capire che funzione chiamare.

In realtà se facciamo un piccolo benchmark vediamo che

BenchmarkInterface
BenchmarkInterface-4            135735110            9.017 ns/op

BenchmarkGeneric
BenchmarkGeneric-4              50947912            22.26 ns/op

la prima funzione in realtà è quella più veloce tra le due, anzi è veloce praticamente il doppio.

Se proviamo ad aggiungere l’annotazione //go:noinline alla prima funzione possiamo iniziare ad intuire cosa sta succedendo

//go:noinline
func WriteOneByte(w io.Writer, data byte) {
    w.Write([]byte{data})
}

perché ora rifacendo il benchmark i risultati della funzione generica e di quella senza inline sono circa uguali.

BenchmarkInterface
BenchmarkInterface-4            135735110            9.017 ns/op

BenchmarkInterfaceNoInline
BenchmarkInterfaceNoInline-4    46183813            23.64 ns/op

BenchmarkGeneric
BenchmarkGeneric-4              50947912            22.26 ns/op

Cioè che sta succedendo dipende dal fatto che il compilatore del Go in realtà è molto bravo a trattare le interfacce ed in questo caso semplicemente utilizzando la strategia dell’inlining riesce a ottimizzare parecchio la funzione e saltare molti passaggi inutili.

d := &bytes.Buffer{} /* (*bytes.Buffer) */
WriteOneByte(d /* (io.Writer) */, 42)
↓
d := &bytes.Buffer{} /* (*bytes.Buffer) */
(io.Writer).Write(d /* (io.Writer) */, []byte{ 42 })
↓
d := &bytes.Buffer{} /* (*bytes.Buffer) */
(*bytes.Buffer).Write(d /* (*bytes.Buffer) */, []byte{ 42 })

Quello che sta succedendo qui è che inizialmente il Go fa l’inlining della funzione WriteOneByte sostituendone il contenuto in place nel chiamante. Poi si accorge che non serve più fare il wrapping e l’unwrapping dell’interfaccia io.Writer quindi inserisce direttamente la chiamata al metodo statico (*bytes.Buffer).Write(d, ...).

Quindi essenzialmente spesso possiamo fidarci di usare le interfacce in Go senza preoccuparci troppo in problemi di performance.

Implementazione delle Generics con Dictionaries e GCShape Stenciling

Vediamo meglio come funziona l’implementazione delle generics nel Go.

Pattern: Type-safe Database API

Vediamo un modo interessante per rendere type-safe l’interfaccia di una libreria utilizzando le generics.

In molti linguaggi con le generics ci sono casi in cui può essere utile definire un tipo generico senza però usare la generics all’interno della definizione (ad esempio in Rust non usare una generics dà proprio errore però in certi casi è utile fare questa cosa quindi è stato introdotto il tipo PhantomData<T>).

Spesso ad esempio quando lavoriamo con un database ci tocca passare in giro nella nostra applicazione ID di righe nel database per varie entità (utenti, prodotti, …). E se non stiamo attenti può succedere di sbagliarsi e passare l’ID di un utente come ID di un prodotto e viceversa.

L’idea

Proviamo ad usare la tecnica citata sopra per rendere type-safe l’interfaccia con *sql.DB. Introduciamo alcuni tipi

type DatabaseRef[T any] string

questo tipo DatabaseRef[T] rappresenterà un ID tipato da passare in giro nella nostra applicazione

package tables

// tables metadata
var Users = database.Table[User]{ ... }
var Products = database.Table[Product]{ ... }

Poi ad esempio possiamo introdurre una lista di tabelle tipate come qui sopra in modo da poter anche verificare che anche le operazioni facciamo sul nostro database siano sulle entità giuste.

E poi l’idea è che potremo interagire con il nostro database utilizzando alcune funzioni Create, Read, Update, Delete che controllano che il tipo della tabella che stiamo usando sia lo stesso della referenza che gli stiamo passando.

// userRef1 :: Ref[User]
userRef1 := DatabaseRef[User]("j.smith@example.org")
// Ok
user1, err := database.Read(dbConn, tables.Users, userRef1)

// Errore: "Ref[Product] != Ref[User]"
user2, err := database.Read(dbConn, tables.Products, userRef1)

Implementazione

Definiamo i seguenti tipi in un modulo chiamato database

package database

type WithPK interface {
    PrimaryKey() *string
}

type Ref[T WithPK] string

type Table[T WithPK] struct {
    Name     string
    PkColumn string
    Columns  func(*T) []any
}

A questo punto definiamo le funzione per eseguire le nostre operazioni CRUD come segue

package database

...

func Create[T WithPK](d DB, t Table[T], row T) (Ref[T], error)

func Insert[T WithPK](d DB, t Table[T], row T) (Ref[T], error)

func Read[T WithPK](d DB, t Table[T], ref Ref[T]) (*T, error)

func Update[T WithPK](d DB, t Table[T], row T) error

func Delete[T WithPK](d DB, t Table[T], id Ref[T]) error

come possiamo vedere stiamo introducendo il type parameter T e poi lo stiamo utilizzando per forzare che quando passiamo Table[T] e un valore abbiamo lo stesso tipo.

Giusto per dare un’idea vediamo come si potrebbe implementare la funzione Read

func Read[T WithPK](d DB, t Table[T], ref Ref[T]) (*T, error) {
    result := d.QueryRow(
        fmt.Sprintf(
            `SELECT * FROM %s WHERE %s = ?`,
            t.Name, t.PkColumn,
        ),
        string(ref),
    )

    var value T
    if err := result.Scan(t.Columns(&value)...); err != nil {
        return nil, err
    }

    return &value, nil
}

L’unica cosa da osservare è che stiamo facendo interpolazione per costruire la query giusta ma non comporta veramente problemi di sql injection perché l’idea sarebbe che tutti i metadati sulle tabelle siano noti a compile time.

Vediamo un breve esempio di come utilizzare questa “libreria”, possiamo definire così un tipo che rappresenti un nostro utente

package model

type User struct {
    Username  string
    FullName  string
    Age       int
}

func (u *User) PrimaryKey() *string {
    return &u.Username
}

Ed invece come segue i metadati per la tabella Users, in particolare la funzione Columns qui l’ho scritta a mano ma penso si dovrebbe poter generare all’avvio del programma con un po’ di reflection

package tables

var Users = Table[User]{
    Name: "users",
    PkColumn: "username",
    Columns: func(u *User) []any {
        return []any{ &u.Username, &u.FullName, &u.Age }
    }
}

In conclusione possiamo anche utilizzare le generics per rendere type-safe l’interfaccia di qualcosa che inizialmente non lo era.

Pattern: Channels

Vediamo qualche utility per lavorare meglio con i channel. Intanto definiamo la seguente utility che ci permette di inviare un valore ad un channel se in quel momento era libero di accettare valori.

func trySend[T any](c chan<- T, v T) bool {
    select {
    case c <- v:
        return true
    default:
        return false
    }
}

E possiamo utilizzarla per definire ad esempio questa funzione per fare una “gara” tra vari channel e vedere chi ritorna per primo un risultato.

func raceSame[T any](cs ...<-chan T) T {
    done := make(chan T)
    defer close(done)

    for _, c := range cs {
        go func(c <-chan T) {
            trySend(done, <-c)
        }(c)
    }

    return <-done
}

E se volessimo una funzione race per channel tutti di tipi diversi? Possiamo risolvere questo problema ad esempio introducendo un’interfaccia Awaiter ed un tipo awaiterChan che ci permette di metterci in attesa su channel per tipi qualsiasi

type Awaiter interface {
    Await()
}

type awaiterChan[T any] <-chan T

func (ac awaiterChan[T]) Await() { <-ac }

Spesso però ci interessa anche il risultato ricevuto dal channel quindi introduciamo anche il seguente tipo che salva il risultato dentro un puntatore fornito dall’esterno

type targetChan[T any] struct {
    c      <-chan T
    target *T
}

func (tc targetChan[T]) Await() { *tc.target = <-tc.c }

a questo punto possiamo definire la funzione race “generica” per interfacce in quest’altro modo

func race(rs ...Awaiter) {
    done := make(chan struct{})
    defer close(done)

    for _, r := range rs {
        go func(r Awaiter) {
            r.Await()
            trySend(done, struct{}{})
        }(r)
    }

    <-done
}

da utilizzare ad esempio così

var result2 int
var result3 float64

raceAny(
    awaiterChan[string](c1),
    targetChan[int]{c2, &result2},
    targetChan[float64]{c3, &result3},
)

fmt.Println(result2, result3)

ed in realtà facendo un po’ di pulizia ed introducendo un paio di funzioni potremmo ottenere un’API molto simpatica come

var result2 int
var result3 float64

channels.Race(
    channels.Awaiter(c1),
    channels.Awaiter(c2, channels.WithTarget(&result2)),
    channels.Awaiter(c3, channels.WithTarget(&result3)),
)

fmt.Println(result2, result3)

1 + 1 = 2

Ora per concludere vediamo un esempio spastico giusto per vedere la potenza che possono raggiungere le generics in Go.

In questi esempi ci interesserà giusto che il programma compili quindi spesso per evitare di definire il corpo di alcune funzioni useremo dei panic.

Premesse

Definiamo i possibili “tipi” delle nostre espressioni, le definiamo come interfacce con metodi privati giusto per forzare il compilatore a rigettare ad esempio var b Bool; var n Nat = b che sarà utile nel nostro caso in cui avremo molti tipi abbastanza complessi

type Bool interface{ isBool() }

type Nat interface{ isNat() }

type Nat2Nat interface{ isNat2Nat() }

Inoltre introduciamo il seguente tipo V di “valutazione”

type V[ H Nat2Nat, T Nat ] Nat

questo essenzialmente è un trucco per poter codificare gli higher-kinded types in Go (di base in Go non possiamo scrivere funzioni con vincoli come

MapContainerItems[F Functor[_], T, S any](items F[T], f func(T) S) F[S]

in cui un vincolo è a sua volta generico in un parametro). Moralmente V[H, T] indica la valutazione di una funzione H per un valore T. In ogni caso sarà più chiaro il senso di questo tipo più avanti quando definiremo gli assiomi dell’uguaglianza.

Assiomi dei Naturali

A questo punto possiamo definire i numeri naturali come tipi in questo modo (da ricordare che type <newtype> <expr> definisce un nuovo tipo mentre la sintassi type <name> = <expr> introduce solo un alias)

type Zero Nat
type Succ Nat2Nat

// Alcuni alias utili
type One = V[Succ, Zero]
type Two = V[Succ, V[Succ, Zero]]
type Three = V[Succ, V[Succ, V[Succ, Zero]]]

Uguaglianza

Ora definiamo un tipo per rappresentare l’uguaglianza tra due termini.

type Eq[A, B any] Bool

con rispettivi assiomi di riflessività, simmetria e transitività per l’uguaglianza

func Eq_Reflexive[T any]() Eq[T, T] {
    panic("axiom: comptime only")
}

func Eq_Symmetric[A, B any](_ Eq[A, B]) Eq[B, A] {
    panic("axiom: comptime only")
}

func Eq_Transitive[A, B, C any](_ Eq[A, B], _ Eq[B, C]) Eq[A, C] {
    panic("axiom: comptime only")
}

ad esempio l’assioma di riflessività Eq_Reflexive ci dice che per ogni tipo $\mathtt T$ possiamo dire che $\mathtt T = \mathtt T$.

Il secondo di simmetria invece ci dice che se sappiamo che $\mathtt A = \mathtt B$ allora possiamo anche dire $\mathtt B = \mathtt A$.

L’ultimo invece ci dice che data una dimostrazione di $\mathtt A = \mathtt B$ e $\mathtt B = \mathtt C$ possiamo ottenere una dimostrazione $\mathtt A = \mathtt C$.

Uguaglianza e Sostituzione

Un altro assioma dell’uguaglianza su cui spesso si sorvola è quello della sostituzione, ovvero se abbiamo due cose uguali ed una mappa allora anche gli elementi mappati sono uguali.

Più precisamente per ogni funzione F, ovvero tipo vincolato all’interfaccia Nat2Nat vorremmo dire che

$$ \texttt{Eq[A, B]} \; \xrightarrow{\texttt{F[}\,\cdot\,\texttt{]}} \; \texttt{Eq[F[A], F[B]]} $$

e possiamo codificare questa cosa in Go come segue: data una funzione ed una dimostrazione che due cose sono uguali allora possiamo applicare la funzione ed ottenere altre cose uguali

func Function_Eq[F Nat2Nat, A, B Nat](_ Eq[A, B]) Eq[V[F, A], V[F, B]] {
    panic("axiom: comptime only")
}

qui il tipo V ci permette di codificare la valutazione di una funzione al livello dei tipi. L’altra cosa da notare è che la nostra funzione sarà Succ che abbiamo definito come di tipo Nat2Nat (se avessimo avuto gli higher-kinded types avremmo potuto definire direttamente Succ come type Succ[N Nat] Nat invece ora ci tocca rappresentarla come tipo non generico)

Assiomi dell’addizione

Questi sono gli assiomi dell’addizione (giusto quelli che ci servono) secondo Peano, il primo ci dice giusto che $n + 0 = n$ mentre il secondo è l’assioma di ricorsione della somma $n + (m + 1) = (n + m) + 1$.

type Plus[L, R Nat] Nat

func Plus_Zero[N Nat]() Eq[Plus[N, Zero], N] {
    panic("axiom: comptime only")
}

func Plus_Sum[N, M Nat]() Eq[
    Plus[N, V[Succ, M]],
    V[Succ, Plus[N, M]],
] { panic("axiom: comptime only") }

La dimostrazione finale

Ed ora possiamo concludere con la nostra dimostrazione di 1 + 1 = 2 al livello dei tipi

func Theorem_OnePlusOneEqTwo() Eq[Plus[One, One], Two] {
    // enunciamo che "1 + 0 = 1"
    // en1 :: Eq[ Plus[One, Zero], One ]
    en1 := Plus_Zero[One]()

    // ora invece che "(1 + 0) + 1 = 2"
    // en2 :: Eq[ V[Succ, Plus[One, Zero]], Two ]
    en2 := Function_Eq[Succ](en1)

    // infine che "1 + 1 = (1 + 0) + 1"
    // en3 :: Eq[ Plus[One, One], V[Succ, Plus[One, Zero]] ]
    en3 := Plus_Sum[One, Zero]()

    // ed ora uniamo gli ultimi due fatti
    return Eq_Transitive(en3, en2)
}

e questo conclude la nostra dimostrazione.

Conclusione

Regole generali

Per scrivere codice generico in Go

Domande dal pubblico

Alla fine alcune persone hanno fatto delle domande

Bibliografia

Tutta la prima parte del talk deriva essenzialmente da questi articoli.