git.iko.soy/Idris-dev
on master help sign in
Note on cumulativity in tutorial
0b9cab2Edwin Brady
src/Idris/ElabTerm.hs+1−1
compare with master
unifiedsplit
@@ -86,7 +86,7 @@ elab ist info pattern tcgen fn tm
86 local f = do e <- get_env
86 local f = do e <- get_env
87 return (f `elem` map fst e)
87 return (f `elem` map fst e)
88
88
89− elab' ina PSet = do fill RSet; solve
89+ elab' ina PSet = do apply RSet []; solve
90 elab' ina (PConstant c) = do apply (RConstant c) []; solve
90 elab' ina (PConstant c) = do apply (RConstant c) []; solve
91 elab' ina (PQuote r) = do fill r; solve
91 elab' ina (PQuote r) = do fill r; solve
92 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))
92 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))
tutorial/examples/universe.idrnew file+7
@@ -0,0 +1,7 @@
1+myid : (a : Set) -> a -> a
2+myid _ x = x
3+
4+idid : (a : Set) -> a -> a
5+idid = myid _ myid
6+
7+
tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/miscellany.tex+65−2
@@ -1,8 +1,8 @@
1\section{Miscellany}
1\section{Miscellany}
2
2
3In this section we discuss a variety of additional features: extensible syntax,
3In this section we discuss a variety of additional features: extensible syntax,
4−literate programming, and interfacing with external libraries through the
4+literate programming, interfacing with external libraries through the
5−foriegn function interface.
5+foriegn function interface, and the universe hierarchy.
6
6
7\input{syntax}
7\input{syntax}
8
8
@@ -132,6 +132,69 @@ This is made possible through the following directives:
132\item \texttt{\%obj "x.o"} --- link with the object file \texttt{x.o}.
132\item \texttt{\%obj "x.o"} --- link with the object file \texttt{x.o}.
133\end{itemize}
133\end{itemize}
134
134
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+
135%\subsection{Comparison}
198%\subsection{Comparison}
136
199
137%How does \Idris{} compare with other dependently typed languages and proof
200%How does \Idris{} compare with other dependently typed languages and proof