git.iko.soy/Idris-dev
on de6bb41 help sign in
Idris-dev/tutorial/miscellany.tex
200 lines 5.8 kB history raw
1\section{Miscellany}
3In this section we discuss a variety of additional features: extensible syntax,
4literate programming, interfacing with external libraries through the
5foriegn function interface, and the universe hierarchy.
7\input{syntax}
9\subsection{Literate programming}
11Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an
12extension of \texttt{.lidr} then it is assumed to be a literate file. In literate
13programs, everything is assumed to be a comment unless the line begins with a
14greater than sign \texttt{>}, for example:
16\begin{SaveVerbatim}{litidr}
18> module literate
20This is a comment. The main program is below
22> main : IO ()
23> main = putStrLn "Hello literate world!\n"
25\end{SaveVerbatim}
26\useverb{litidr}
28\noindent
29An additional restriction is that there must be a blank line between a program
30line (beginning with \texttt{>}) and a comment line (beginning with any other
31character).
33\subsection{Foreign function calls}
35For practical programming, it is often necessary to be able to use external libraries,
36particularly for interfacing with the operating system, file system, networking, etc.
37\Idris{} provides a lightweight foreign function interface for achieving this,
38as part of the prelude. For this, we assume a certain amount of knowledge of
39C and the \texttt{gcc} compiler. First, we define a datatype which describes the external
40types we can handle:
42\begin{SaveVerbatim}{foreignty}
44data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit
46\end{SaveVerbatim}
47\useverb{foreignty}
49\noindent
50Each of these corresponds directly to a C type. Respectively: \texttt{int},
51\texttt{float}, \texttt{char}, \texttt{char*}, \texttt{void*} and \texttt{void}.
52There is also a translation to a concrete \Idris{} type, described by the
53following function:
55\begin{SaveVerbatim}{interpfty}
57interpFTy : FTy -> Set
58interpFTy FInt = Int
59interpFTy FFloat = Float
60interpFTy FChar = Char
61interpFTy FString = String
62interpFTy FPtr = Ptr
63interpFTy FUnit = ()
65\end{SaveVerbatim}
66\useverb{interpfty}
68\noindent
69A foreign function is described by a list of input types and a return type, which
70can then be converted to an \Idris{} type:
72\begin{SaveVerbatim}{ffunty}
74ForeignTy : (xs:List FTy) -> (t:FTy) -> Set
76\end{SaveVerbatim}
77\useverb{ffunty}
79\noindent
80A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an
81\texttt{IO} type, for example:
83\begin{SaveVerbatim}{ftyex}
85Idris> ForeignTy [FInt, FString] FString
86Int -> String -> IO String : Set
88Idris> ForeignTy [FInt, FString] FUnit
89Int -> String -> IO () : Set
91\end{SaveVerbatim}
92\useverb{ftyex}
94\noindent
95We build a call to a foreign function by giving the name of the function, a list of
96argument types and the return type. The built in function \texttt{mkForeign}
97converts this description to a function callable by \Idris{}
99\begin{SaveVerbatim}{mkForeign}
101data Foreign : Set -> Set where
102 FFun : String -> (xs:List FTy) -> (t:FTy) ->
103 Foreign (ForeignTy xs t)
105mkForeign : Foreign x -> x
107\end{SaveVerbatim}
108\useverb{mkForeign}
110\noindent
111For example, the \texttt{putStr} function is implemented as follows, as a call to
112an external function \texttt{putStr} defined in the run-time system:
114\begin{SaveVerbatim}{putStrex}
116putStr : String -> IO ()
117putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
118\end{SaveVerbatim}
119\useverb{putStrex}
121\subsubsection*{Include and linker directives}
123Foreign function calls are translated directly to calls to C functions, with appropriate
124conversion between the \Idris{} representation of a value and the C representation.
125Often this will require extra libraries to be linked in, or extra header and object files.
126This is made possible through the following directives:
128\begin{itemize}
129\item \texttt{\%lib "x"} --- include the \texttt{libx} library, equivalent to passing the
130\texttt{-lx} option to \texttt{gcc}.
131\item \texttt{\%include "x.h"} --- use the header file \texttt{x.h}.
132\item \texttt{\%obj "x.o"} --- link with the object file \texttt{x.o}.
133\end{itemize}
135\subsection{Cumulativity}
137Since values can appear in types and \emph{vice versa}, it is natural that types themselves
138have types. For example:
140\begin{SaveVerbatim}{typetypes}
142*universe> :t Nat
143Nat : Set
144*universe> :t Vect
145Vect : Set -> Nat -> Set
147\end{SaveVerbatim}
148\useverb{typetypes}
150\noindent
151But what about the type of \texttt{Set}? If we ask \Idris{} it reports
153\begin{SaveVerbatim}{setset}
155*universe> :t Set
156Set : Set
158\end{SaveVerbatim}
159\useverb{setset}
161\noindent
162It \emph{appears} that \texttt{Set} is its own type. This would lead to an inconsitency
163due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}
164of types (or \emph{universes}):
166\begin{SaveVerbatim}{sethierarchy}
168Set : Set 1 : Set 2 : Set 3 : ...
170\end{SaveVerbatim}
171\useverb{sethierarchy}
173\noindent
174Universes 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}.
176The typechecker generates such universe
177constraints and reports an error if any inconsistencies are found. Ordinarily, a
178programmer does not need to worry about this, but it does prevent (contrived)
179programs such as the following:
181\begin{SaveVerbatim}{idid}
183myid : (a : Set) -> a -> a
184myid _ x = x
186idid : (a : Set) -> a -> a
187idid = myid _ myid
189\end{SaveVerbatim}
190\useverb{idid}
192\noindent
193The application of \texttt{myid} to itself leads to a cycle in the universe hierarchy
194--- \texttt{myid}'s first argument is a \texttt{Set}, which cannot be at a lower level
195than required if it is applied to itself.
197%\subsection{Comparison}
199%How does \Idris{} compare with other dependently typed languages and proof
200%assistants, such as Coq, Agda and Epigram?