Changeset 2408

Timestamp:

Oct 19, 2012, 2:07:29 PM (9 years ago)

Author:

sacerdot

Message:

...

File:

• Papers/polymorphic-variants-2012/polymorphic-variants.tex (modified) (1 diff)

Papers/polymorphic-variants-2012/polymorphic-variants.tex

@@ -40 +40 @@
 \label{sect.introduction}
 
+\section{Polymorphic variants}
+\begin{itemize}
+ \item General introduction, motivations
+ \item Bounded vs not-bounded.
+\end{itemize}
+
+\subsection{Subtyping as instantiation vs subtyping as safe static cast}
+
+\subsection{Syntax \& type checking rules}
+The ones of Guarrigue + casts, but also for the bounded case?
+Casts support both styles of subtyping.
+
+\subsection{Examples}
+The weird function types that only work in subtyping as instantiation
+
+\subsection{Solution to the expression problem}
+Our running example in pseudo-OCaml syntax
+
+\section{Bounded polymorphic variants via dependent types}
+Requirements (i.e. O(1) pattern-matching, natural extracted code, etc.)
+\subsection{Simulation (reduction + type checking)}
+\subsection{Examples}
+The weird function types redone
+\subsection{Subtyping as instantiation vs subtyping as safe static cast}
+Here we show/discuss how our approach supports both styles at once.
+\subsection{Solution to the expression problem, I}
+Using subtyping as cast, the file I have produced
+\subsection{Solution to the expression problem, II}
+Using subtyping as instantiation, comparisons, pros vs cons
+\subsection{Negative encoding (??)}
+The negative encoding and application to the expression problem
+\subsection{Other encodings (??)}
+Hints to other possible encodings
+
+\section{Extensible records (??)}
+
+\section{Comparison to related work and alternatives}
+\begin{itemize}
+ \item Disjoint unions: drawbacks
+ \item Encoding the unbounded case: drawbacks
+\end{itemize}
+
+\section{Appendix: interface of library functions used to implement everything}
+
 \end{document}