Add code to writeup of examples

Author: dawidl022

deliverables/4-cycle-detection-summary/examples/generic-containment-any.go

@@ -1,20 +1,5 @@
 package main
 
-import "fmt"
-
-// Let's remember Bar in the type parameter constraint is syntactic sugar for
-// an anonymous type set interface: interface { Bar }. The only type
-// this constraint can be instantiated with is Bar (struct type).
-//
-// This code compiles in this declaration order, but fails to compile if
-// we reverse the order of struct declarations.
-//
-// The code also (rightfully so) fails to compile if we add a field of type b,
-// as this would violate the notContains constraint. However e.g. a field of type
-// pointer to b is fine.
-//
-// I.e. by introducing type set interfaces, we need to extend notContains
-// checks to type parameters in generic types.
 type Foo[T any] struct {
 	x T
 }
@@ -24,8 +9,4 @@ type Bar struct {
 }
 
 func main() {
-	x := Foo[Bar]{}
-	y := Bar{x: x}
-	fmt.Println(x)
-	fmt.Println(y)
 }

deliverables/4-cycle-detection-summary/examples/generic-containment-clean.go

@@ -0,0 +1,18 @@
+package main
+
+import "fmt"
+
+type Foo[T Bar] struct {
+	x *T
+}
+
+type Bar struct {
+	x Foo[Bar]
+}
+
+func main() {
+	x := Foo[Bar]{}
+	y := Bar{x: x}
+	fmt.Println(x)
+	fmt.Println(y)
+}

deliverables/4-cycle-detection-summary/summary.tex

@@ -7,6 +7,7 @@
 \usepackage{stmaryrd}
 \usepackage{xcolor}
 \usepackage{hyperref}
+\usepackage{listings}
 
 \input{../../projects/go-generic-array-sizes/theory/macros}
 
@@ -191,6 +192,34 @@ \subsection{Lifting type parameter reference rules}
 \end{itemize}
 
 \section{Examples}
+\noindent\begin{minipage}[t]{.45\linewidth}
+    \lstinputlisting[language=Go, tabsize=4, firstline=3]
+    {./examples/generic-containment-any.go}
+
+    The definition of \texttt{Bar} should be rejected, since it creates a type
+    containment cycle via \texttt{Foo}. The compiler correctly reports \texttt{Bar}
+    as an invalid recursive type.
+\end{minipage}
+\hfill
+\noindent\begin{minipage}[t]{.45\linewidth}
+    \lstinputlisting[language=Go, tabsize=4, firstline=3, lastline=35]
+    {./examples/generic-containment-clean.go}
+
+    Using e.g. a pointer to \texttt{T} in the
+    definition of \texttt{Foo} would make the program valid. We can even
+    change the type constraint of \texttt{T} from \texttt{any} to \texttt{Bar}, and
+    the type checker should behave the same. However, as of Go 1.23, such a program
+    is either rejected or accepted by the type checker depending on the order of the
+    struct declarations (similar to \href{https://github.com/golang/go/issues/65714}{Issue
+        \#65714}).
+
+\end{minipage}
+
+\subsection{Type checking derivation with contradiction}
+
+Below, we derive a contradiction while type checking the above program on the
+left, showing that the $\notcont$ rule is sufficient for detecting structural
+cycles in generic types.
 
 \input{generic-containment-any}