@@ -1,8 +1,8 @@
11\section{Miscellany}
22
33In this section we discuss a variety of additional features: extensible syntax,
4−literate programming, and interfacing with external libraries through the
5−foriegn function interface.
4+literate programming, interfacing with external libraries through the
5+foriegn function interface, and the universe hierarchy.
66
77\input{syntax}
88
@@ -132,6 +132,69 @@ This is made possible through the following directives:
132132\item \texttt{\%obj "x.o"} --- link with the object file \texttt{x.o}.
133133\end{itemize}
134134
135+\subsection{Cumulativity}
136+
137+Since values can appear in types and \emph{vice versa}, it is natural that types themselves
138+have types. For example:
139+
140+\begin{SaveVerbatim}{typetypes}
141+
142+*universe> :t Nat
143+Nat : Set
144+*universe> :t Vect
145+Vect : Set -> Nat -> Set
146+
147+\end{SaveVerbatim}
148+\useverb{typetypes}
149+
150+\noindent
151+But what about the type of \texttt{Set}? If we ask \Idris{} it reports
152+
153+\begin{SaveVerbatim}{setset}
154+
155+*universe> :t Set
156+Set : Set
157+
158+\end{SaveVerbatim}
159+\useverb{setset}
160+
161+\noindent
162+It \emph{appears} that \texttt{Set} is its own type. This would lead to an inconsitency
163+due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}
164+of types (or \emph{universes}):
165+
166+\begin{SaveVerbatim}{sethierarchy}
167+
168+Set : Set 1 : Set 2 : Set 3 : ...
169+
170+\end{SaveVerbatim}
171+\useverb{sethierarchy}
172+
173+\noindent
174+Universes are \emph{cumulative}, that is, if \texttt{x : Set n} we can also have that
175+\texttt{x : Set m}, as long as \texttt{n < m}.
176+The typechecker generates such universe
177+constraints and reports an error if any inconsistencies are found. Ordinarily, a
178+programmer does not need to worry about this, but it does prevent (contrived)
179+programs such as
180+the following:
181+
182+\begin{SaveVerbatim}{idid}
183+
184+myid : (a : Set) -> a -> a
185+myid _ x = x
186+
187+idid : (a : Set) -> a -> a
188+idid = myid _ myid
189+
190+\end{SaveVerbatim}
191+\useverb{idid}
192+
193+\noindent
194+The application of \texttt{myid} to itself leads to a cycle in the universe hierarchy
195+--- \texttt{myid}'s first argument is a \texttt{Set}, which cannot be at a lower level
196+than required if it is applied to itself.
197+
135198%\subsection{Comparison}
136199
137200%How does \Idris{} compare with other dependently typed languages and proof