diff --git a/005-iface-vs-typeparam.test b/005-iface-vs-typeparam.test deleted file mode 100755 index 75a244a..0000000 Binary files a/005-iface-vs-typeparam.test and /dev/null differ diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..a630b75 --- /dev/null +++ b/Makefile @@ -0,0 +1,32 @@ + +subprojects = $(patsubst examples/%, %, $(wildcard examples/*)) + +.PHONY: usage +usage: + @printf "Found the following subprojects:\n" + @for project in $(subprojects); do printf " - %s\n" $$project; done + @printf "\n" + @printf "Available rules\n" + @printf " - run-: Will run the program\n" + @printf " - compile-: Will compile the program\n" + @printf " - compile-noinline-: Will compile the program without inlining\n" + @printf " - decomp-: Will run lensm on the project\n" + @printf " - decomp-noinline-: Will run lensm on the project without inlining\n" + @printf "\n" + +run-%: FORCE + go run -v ./examples/$* + +compile-%: FORCE + go build -v -o "./bin/$*" ./examples/$* + +compile-noinline-%: FORCE + go build -v -o "./bin/$*@no-inline" -gcflags=-l ./examples/$* + +decomp-%: compile-% FORCE + lensm -text-size 16 -filter main "./bin/$*" + +decomp-noinline-%: compile-noinline-% FORCE + lensm -text-size 16 -filter main "./bin/$*@no-inline" + +FORCE: ; diff --git a/decompile b/decompile deleted file mode 100755 index 6ae2bb4..0000000 Binary files a/decompile and /dev/null differ diff --git a/decompile.test b/decompile.test deleted file mode 100755 index ed2d914..0000000 Binary files a/decompile.test and /dev/null differ diff --git a/examples/decompile/main.go b/examples/decompile/main.go deleted file mode 100644 index 77ac915..0000000 --- a/examples/decompile/main.go +++ /dev/null @@ -1,31 +0,0 @@ -package main - -import ( - "fmt" - - "golang.org/x/exp/constraints" -) - -func Min[T constraints.Ordered](x, y T) T { - if x < y { - return x - } - return y -} - -type Liter int - -func main() { - { - var a, b int = 1, 2 - fmt.Println(Min(a, b)) - } - { - var a, b float64 = 3.14, 2.71 - fmt.Println(Min(a, b)) - } - { - var a, b Liter = 1, 2 - fmt.Println(Min(a, b)) - } -} diff --git a/examples/min/main.go b/examples/min/main.go new file mode 100644 index 0000000..fd0d394 --- /dev/null +++ b/examples/min/main.go @@ -0,0 +1,83 @@ +package main + +import ( + "fmt" + + "golang.org/x/exp/constraints" +) + +// before go generics + +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 MinInt32(x, y int32) int32 { + if x < y { + return x + } + + return y +} + +func MinInt64(x, y int64) int64 { + if x < y { + return x + } + + return y +} + +func MinFloat32(x, y float32) float32 { + if x < y { + return x + } + + return y +} + +func MinFloat64(x, y float64) float64 { + if x < y { + return x + } + + return y +} + +// with go generics + +func Min[T constraints.Ordered](x, y T) T { + if x < y { + return x + } + return y +} + +type Liter int + +func main() { + { + var a, b int = 1, 2 + fmt.Println(Min(a, b)) + } + { + var a, b float64 = 3.14, 2.71 + fmt.Println(Min(a, b)) + } + { + var a, b Liter = 1, 2 + fmt.Println(Min(a, b)) + } +} diff --git a/examples/theorem-proving/main.go b/examples/theorem-proving/main.go new file mode 100644 index 0000000..9dcaae8 --- /dev/null +++ b/examples/theorem-proving/main.go @@ -0,0 +1,87 @@ +package main + +// +// Encoding the semantics +// + +type Bool interface{ isBool() } + +type Term interface{ isTerm() } + +type Term2Term interface{ isTerm2Term() } + +// trick to encode higher-kinded types +type V[H Term2Term, T Term] Term + +// +// Naturals +// + +type Zero Term +type Succ Term2Term + +// Some aliases + +type One = V[Succ, Zero] +type Two = V[Succ, V[Succ, Zero]] +type Three = V[Succ, V[Succ, V[Succ, Zero]]] + +// +// Equality +// + +type Eq[A, B any] Bool + +// Eq_Refl ~> forall x : x = x +func Eq_Reflexive[T any]() Eq[T, T] { panic("axiom") } + +// Eq_Symmetric ~> forall a, b: a = b => b = a +func Eq_Symmetric[A, B any](_ Eq[A, B]) Eq[B, A] { panic("axiom") } + +// Eq_Transitive ~> forall a, b, c: a = b e b = c => a = c +func Eq_Transitive[A, B, C any](_ Eq[A, B], _ Eq[B, C]) Eq[A, C] { panic("axiom") } + +// Function_Eq ~> forall f function, forall a, b terms: a = b => f(a) = f(b) +func Function_Eq[F Term2Term, A, B Term](_ Eq[A, B]) Eq[V[F, A], V[F, B]] { + panic("axiom") +} + +// +// Plus Axioms +// + +type Plus[L, R Term] Term + +// "a + 0 = a" + +// Plus_Zero ~> forall a, b: a + succ(b) = succ(a + b) +func Plus_Zero[N Term]() Eq[Plus[N, Zero], N] { panic("axiom") } + +// "a + (b + 1) = (a + b) + 1" + +// Plus_Sum ~> forall a, b: a + succ(b) = succ(a + b) +func Plus_Sum[N, M Term]() Eq[Plus[N, V[Succ, M]], V[Succ, Plus[N, M]]] { panic("axiom") } + +// +// 1 + 1 = 2 +// + +// Theorem_OnePlusOneEqTwo +func Theorem_OnePlusOneEqTwo() Eq[Plus[One, One], Two] { + var en1 Eq[ + Plus[One, Zero], + One, + ] = Plus_Zero[One]() + + var en2 Eq[ + V[Succ, Plus[One, Zero]], + Two, + ] = Function_Eq[Succ](en1) + + var en3 Eq[ + Plus[One, One], + V[Succ, Plus[One, Zero]], + ] = Plus_Sum[One, Zero]() + + return Eq_Transitive(en3, en2) +} diff --git a/slides.md b/slides.md index aa2b529..34a8879 100644 --- a/slides.md +++ b/slides.md @@ -90,7 +90,7 @@ func MinInt8(x, y int8) int8 { return y } -func MinInt16(x, y int16) int8 { +func MinInt16(x, y int16) int16 { if x < y { return x } @@ -510,6 +510,66 @@ d := &bytes.Buffer{} /* (*bytes.Buffer) */ (*bytes.Buffer).Write(d /* (*bytes.Buffer) */, []byte{ 42 }) ``` + +--- + + + +# Confronto con altri linguaggi +Vediamo come funzionano le generics in Go confrontandole con altri linguaggi + +--- + +## C + +```c +// versione semplificata da linux/minmax.h +#define min(x, y) ({ \ // block expr (GCC extension) + typeof(x) _min1 = (x); \ // eval x once + typeof(y) _min2 = (y); \ // eval y once + (void) (&_min1 == &_min2); \ // check same type + _min1 < _min2 ? _min1 : _min2; \ // do comparison +}) +``` + +--- + +## C++ + +```cpp +template +T min(T const& a, T const& b) +{ + return (a < b) ? a : b; +} +``` + +--- + +## Rust + +```rust +pub fn min(a: T, b: T) -> T { + if a < b { + a + } else { + b + } +} +``` + +--- + +## Go _Gcshape Stenciling_ + +- _A **gcshape** (or gcshape grouping) is a collection of types that can all **share the same instantiation of a generic function/method** in our implementation when specified as one of the type arguments_. + +- _Two concrete types are in the same gcshape grouping if and only if they have the **same underlying type** or they are **both pointer types**._ + +- _In order to avoid creating a different function instantiation for each invocation of a generic function/method with distinct type arguments (which would be pure stenciling), we **pass a dictionary along with every call** to a generic function/method_. + + + --- @@ -613,50 +673,6 @@ var foo Validator = FooRequest{} -# Confronto -Vediamo un attimo come fungono internamente le generics del Go - ---- - -```c -// C? -#define min(x, y) ({ \ - typeof(x) _min1 = (x); \ - typeof(y) _min2 = (y); \ - (void) (&_min1 == &_min2); \ - _min1 < _min2 ? _min1 : _min2; }) -``` - -```cpp -// C++ -template -T min(T const& a, T const& b) -{ - return (a < b) ? a : b; -} -``` - ---- - -```go -// Go -func Min[T constraints.Ordered](x, y T) T { - if x < y { - return x - } - return y -} -``` - -```rust -// Rust -??? -``` - ---- - - - # Pattern (2) Vediamo un analogo di `PhantomData` dal Rust per rendere _type-safe_ l'interfaccia di una libreria @@ -795,13 +811,6 @@ func (p Promise[T]) Await() (T, error) { <-p.done return p.value, p.err } - -type Waiter { Wait() error } - -func (p Promise[T]) Wait() error { - <-p.done - return p.err -} ``` --- @@ -809,11 +818,11 @@ func (p Promise[T]) Wait() error { ```go type PromiseFunc[T any] func(resolve func(T), reject func(error)) -func Start[T any](f PromiseFunc[T]) *Promise[T] { +func Run[T any](f PromiseFunc[T]) *Promise[T] { done := make(chan struct{}) p := Promise{ done: done } - f( + go f( func(value T) { p.value = value; done <- struct{} }, func(err error) { p.err = err; done <- struct{} } ) @@ -825,6 +834,13 @@ func Start[T any](f PromiseFunc[T]) *Promise[T] { --- ```go +type Waiter { Wait() error } + +func (p Promise[T]) Wait() error { + <-p.done + return p.err +} + func AwaitAll(ws ...Waiter) error { var wg sync.WaitGroup wg.Add(len(ws)) @@ -863,6 +879,157 @@ func AwaitAll(ws ...Waiter) error { --- +```go +Validate() +``` + +--- + + + +# 1 + 1 = 2 +_Proof checking_ in Go + +--- + +## Premesse + +```go +type Bool interface{ isBool() } + +type Term interface{ isTerm() } + +type Term2Term interface{ isTerm2Term() } + +// trick to encode higher-kinded types +type V[H Term2Term, T Term] Term +``` + +--- + +## Assiomi dei Naturali + +```go +type Zero Term +type Succ Term2Term + +// 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 + +```go +type Eq[A, B any] Bool + +// Eq_Refl ~> forall x : x = x +func Eq_Reflexive[T any]() Eq[T, T] { + panic("axiom") +} + +// Eq_Symmetric ~> forall a, b: a = b => b = a +func Eq_Symmetric[A, B any](_ Eq[A, B]) Eq[B, A] { + panic("axiom") +} + +// Eq_Transitive ~> forall a, b, c: a = b e b = c => a = c +func Eq_Transitive[A, B, C any](_ Eq[A, B], _ Eq[B, C]) Eq[A, C] { + panic("axiom") +} +``` + +--- + +## "Funzionalità dell'uguale" + +Per ogni funzione `F`, ovvero tipo vincolato all'interfaccia `Term2Term` vorremmo dire che + +``` + F +Eq[ A , B ] ------> Eq[ F[A] , F[B] ] + +``` + +--- + +## "Funzionalità dell'uguale" + +Data una funzione ed una dimostrazione che due cose sono uguali allora possiamo applicare la funzione ed ottenere altre cose uguali + +```go +// Function_Eq ~> forall f function, forall a, b term: +// a = b => f(a) = f(b) +func Function_Eq[F Term2Term, A, B Term](_ Eq[A, B]) Eq[V[F, A], V[F, B]] { + panic("axiom") +} +``` + +--- + +## Assiomi dell'addizione + +```go +type Plus[L, R Term] Term + +// "n + 0 = n" + +// Plus_Zero ~> forall n, m: n + succ(m) = succ(n + m) +func Plus_Zero[N Term]() Eq[Plus[N, Zero], N] { + panic("axiom") +} + +// "n + (m + 1) = (n + m) + 1" + +// Plus_Sum ~> forall a, m: n + succ(m) = succ(n + m) +func Plus_Sum[N, M Term]() Eq[ + Plus[N, V[Succ, M]], + V[Succ, Plus[N, M]], +] { panic("axiom") } +``` + +--- + +## 1 + 1 = 2 + +```go +func Theorem_OnePlusOneEqTwo() Eq[Plus[One, One], Two] { + var en1 Eq[ Plus[One, Zero], One ] = Plus_Zero[One]() + + var en2 Eq[ + V[Succ, Plus[One, Zero]], + Two + ] = Function_Eq[Succ](en1) + + var en3 Eq[ + Plus[One, One], + V[Succ, Plus[One, Zero]], + ] = Plus_Sum[One, Zero]() + + return Eq_Transitive(en3, en2) +} +``` + +--- + +## 1 + 1 = 2 + +```go +func Theorem_OnePlusOneEqTwo() Eq[Plus[One, One], Two] { + return Eq_Transitive( + Plus_Sum[One, Zero](), + Function_Eq[Succ]( + Plus_Zero[One](), + ), + ) +} +``` + +--- + # Conclusione @@ -890,3 +1057,19 @@ Per scrivere _codice generico_ in Go # Fine :C _Domande_ + +--- + + + +## Bibliografia + +- + +- + +-