Skip to content

Commit 18b5529

Browse files
dawidl022dawidl022
committed
Construct derivation proof for golang/go#51244 
1 parent b8bfcf3 commit 18b5529

File tree

3 files changed

+212
-8
lines changed

3 files changed

+212
-8
lines changed

‎deliverables/4-cycle-detection-summary/examples/issue-51244.go

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
package main
2+
3+
type A interface{ M(B[T]) T }
4+
type B[a A] struct{}
5+
6+
type T struct{}
7+
8+
func (t T) M(b B[T]) T { return t }
9+
10+
func main() {}

‎deliverables/4-cycle-detection-summary/issue-51244.tex

Lines changed: 161 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,161 @@
1+
\register{A}
2+
\register{M}
3+
\register{B}
4+
\register{T}
5+
6+
\begin{align*}
7+
D_0 & = \type~\A~\interface~\br{ \M(b~\B[\T])~\T } \\
8+
D_1 & = \type~\B[a~\A]~\struct~\br{ } \\
9+
D_2 & = \type~\T~\struct~\br{ } \\
10+
D_3 & = \func~(t~\T)~\M(b~\B[\T])~\T~\br{~\return~t~} \\
11+
\ov{D} & = \{D_0, D_1, D_2, D_3\}
12+
\end{align*}
13+
14+
\begin{mathpar}
15+
\derivrule[T-Interface]{
16+
\axiomrule{
17+
\unique(\M(b~\B[\T])~\T)
18+
}
19+
\\
20+
\emptyset \vdash \M(b~\B[\T])~\T \ok
21+
}{
22+
\emptyset \vdash \interface~\br{ \M(b~\B[\T])~\T } \ok \\
23+
}
24+
25+
\derivrule{
26+
\derivrule{
27+
\eta = (a \by \T)
28+
}{
29+
\eta = ((a~\A) \by \T)
30+
}
31+
\\
32+
\derivrule{
33+
\derivrule[$\imp_I$]{
34+
\derivrule{
35+
\axiomrule{
36+
\{~\M(b~\B[\T])~\T~\} \supseteq \{~\M(b~\B[\T])~\T~\}
37+
}
38+
}{
39+
\methods_\emptyset(\T) \supseteq \methods_\emptyset(\A)
40+
}
41+
}{
42+
\emptyset \vdash T \imp A
43+
}
44+
}{
45+
\emptyset \vdash (a \imp A)\llbracket\eta\rrbracket
46+
}
47+
}{
48+
\eta = ((a~\A) \by_\emptyset \T)
49+
}
50+
51+
\derivrule[T-Named]{
52+
\emptyset \vdash \T \ok
53+
\\
54+
(\type~\B[a~\A]~\struct~\br{ }) \in \ov{D}
55+
\\
56+
\eta = ((a~\A) \by_\emptyset \T)
57+
}{
58+
\emptyset \vdash \B[\T] \ok
59+
}
60+
61+
\derivrule[T-Specification]{
62+
\axiomrule{
63+
\distinct(b)
64+
}
65+
\\
66+
\emptyset \vdash \B[\T] \ok
67+
\\
68+
\emptyset \vdash \T \ok
69+
}{
70+
\emptyset \vdash \M(b~\B[\T])~\T \ok
71+
}
72+
\end{mathpar}
73+
74+
\begin{mathpar}
75+
\derivrule[T-Type]{
76+
\emptyset \vdash \interface~\br{ \M(b~\B[\T])~\T } \ok~~~~~
77+
\axiomrule{
78+
\notcont(\A,~\interface~\br{ \M(b~\B[\T])~\T })
79+
}
80+
}{
81+
D_0 \ok
82+
}
83+
84+
\derivrule[T-Formal]{
85+
\axiomrule{
86+
\distinct(a)
87+
}
88+
\\
89+
\derivrule[T-Named]{
90+
\axiomrule{
91+
(\type~\A~\interface~\br{ \M(b~\B[\T])~\T }) \in \ov{D}
92+
}
93+
}{
94+
(a~\A) \vdash \A \ok
95+
}
96+
}{
97+
(a~\A) \ok
98+
}
99+
100+
\derivrule[T-Type]{
101+
(a~\A) \ok
102+
\\
103+
\axiomrule[T-Struct]{
104+
(a~\A) \vdash \struct~\br{ } \ok
105+
}
106+
\\
107+
\axiomrule{
108+
\notcont(\B,~\struct~\br{ })
109+
}
110+
}{
111+
D_1 \ok
112+
}
113+
114+
\derivrule[T-Type]{
115+
\axiomrule[T-Struct]{
116+
\emptyset \vdash \struct~\br{ } \ok
117+
}
118+
\\
119+
\axiomrule{
120+
\notcont(\T,~\struct~\br{ })
121+
}
122+
}{
123+
D_2 \ok
124+
}
125+
126+
\derivrule{
127+
\axiomrule{
128+
(\type~T~\struct~\br{ }) \in \ov{D}
129+
}
130+
}{
131+
\emptyset = \typeparams(T)
132+
}
133+
134+
\derivrule[T-Var]{
135+
\axiomrule{
136+
(t:\T) \in (t:\T,b:\B[\T])
137+
}
138+
}{
139+
\emptyset;t:\T,b:\B[\T] \vdash t : \T
140+
}
141+
142+
\axiomrule[$\imp_V$]{
143+
\emptyset \vdash T \imp T
144+
}
145+
146+
\derivrule[T-Func]{
147+
\axiomrule{
148+
\distinct(t, b)
149+
}
150+
\\
151+
\emptyset = \typeparams(T)
152+
\\
153+
\emptyset \vdash \M(b~\B[\T])~\T \ok
154+
\\
155+
\emptyset;t:\T,b:\B[\T] \vdash t : \T
156+
\\
157+
\emptyset \vdash T \imp T
158+
}{
159+
D_3 \ok
160+
}
161+
\end{mathpar}

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

Lines changed: 41 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -61,8 +61,6 @@ \section{Typing rules}
6161
{
6262
\ov{\Phi \ok}
6363
\\
64-
\ov{\Phi} = (\ov{\alpha~\gamma})
65-
\\
6664
\ov{\Phi} \vdash~T \ok
6765
\\
6866
\notcont(t,~T)
@@ -180,18 +178,23 @@ \subsection{Type containment rules}
180178
depending on the ordering of type declarations.
181179
\end{itemize}
182180

181+
% TODO mention that non-basic interfaces (e.g. embedded or type set interfaces)
182+
% need to be checked for containment cycles
183+
183184
\subsection{Lifting type parameter reference rules}
184185

185186
\begin{itemize}
186-
\item The Go spec currently states: ``Within a type
187-
parameter list of a generic type T, a type constraint may not
188-
(directly, or indirectly through the type parameter list of another
189-
generic type) refer to T.'' In this section we explore the
190-
consequences of lifting this restriction, i.e. allowing type parameter
187+
\item The Go spec currently states: ``Within a type parameter list of a
188+
generic type T, a type constraint may not (directly, or indirectly
189+
through the type parameter list of another generic type) refer to T.''
190+
We can in fact life this restriction, i.e. allowing type parameter
191191
constraints to refer to the type T being defined.
192192
\end{itemize}
193193

194194
\section{Examples}
195+
196+
\subsection{Containment check in generic type}
197+
195198
\noindent\begin{minipage}[t]{.45\linewidth}
196199
\lstinputlisting[language=Go, tabsize=4, firstline=3]
197200
{./examples/generic-containment-any.go}
@@ -215,12 +218,42 @@ \section{Examples}
215218

216219
\end{minipage}
217220

218-
\subsection{Type checking derivation with contradiction}
221+
\subsubsection{Type checking derivation with contradiction}
219222

220223
Below, we derive a contradiction while type checking the above program on the
221224
left, showing that the $\notcont$ rule is sufficient for detecting structural
222225
cycles in generic types.
223226

224227
\input{generic-containment-any}
225228

229+
\subsection{Issue \#51244}
230+
231+
\href{https://github.com/golang/go/issues/51244}{Issue \#51244} demonstrates
232+
another case where the compiler's cycle detection accepts or rejects the program
233+
depending on the order of type declarations. According to the above defined
234+
rules, the program should be accepted. One of the participants of the issue
235+
(\href{https://github.com/findleyr}{findleyr}) also suggested removing the
236+
restriction of cycles through type parameter constraints.
237+
238+
\subsubsection{Accepting type checking derivation}
239+
240+
\golisting{./examples/issue-51244.go}
241+
242+
\noindent
243+
Below is a derivation of the program in the issue, with minor adjustments to
244+
fit a Featherweight Go-like syntax used in this document.
245+
246+
\input{issue-51244}
247+
248+
% TODO appendix will define remaining rules that have been referenced in rules
249+
% or derivations
250+
251+
\subsection{Self-referential type parameter constraints}
252+
253+
\subsubsection{Positive examples}
254+
255+
% TODO mention Go's structural subtyping
256+
257+
\subsubsection{Negative example}
258+
226259
\end{document}

0 commit comments

Comments
 (0)