tutorial/content/miscellany.tex · Idris-dev

git.iko.soy/Idris-dev

on 357cd83 help sign in

Idris-dev/tutorial/content/miscellany.tex

458 lines 16 kB history raw

1\section{Miscellany}

3In this section we discuss a variety of additional features:

4auto implicit and default

5arguments, literate programming, interfacing with external libraries through the

6foreign function interface, type providers, code generation and the universe hierarchy.

8\subsection{Auto implicit arguments}

10We have already seen implicit arguments, which allows arguments to be omitted when

11they can be inferred by the type checker, e.g.

13\begin{code}

14index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

15\end{code}

17\noindent

18In other situations, it may be possible to infer arguments not by type checking but

19by searching the context for an appropriate value, or constructing a proof. For example,

20the following definition of \texttt{head} which requires a proof that the list is

21non-empty

23\begin{code}

24isCons : List a -> Bool

25isCons [] = False

26isCons (x :: xs) = True

28head : (xs : List a) -> (isCons xs = True) -> a

29head (x :: xs) _ = x

30\end{code}

32\noindent

33If the list is statically known to be non-empty, either because its value is known or

34because a proof already exists in the context, the proof can be constructed

35automatically. Auto implicit arguments allow this to happen silently. We define

36\texttt{head} as follows:

38\begin{code}

39head : (xs : List a) -> {auto p : isCons xs = True} -> a

40head (x :: xs) = x

41\end{code}

43\noindent

44The \texttt{auto} annotation on the implicit argument means that \Idris{} will

45attempt to fill in the implicit argument using the \texttt{trivial} tactic, which

46searches through the context for a proof, and tries to solve with \texttt{refl}

47if a proof is not found.

48Now when \texttt{head} is applied, the proof can be omitted. In the case that a proof

49is not found, it can be provided explicitly as normal:

51\begin{code}

52head xs {p = ?headProof}

53\end{code}

55\noindent

56More generally, we can fill in implicit arguments with a default value by annotating

57them with \texttt{default}. The definition above is equivalent to:

59\begin{code}

60head : (xs : List a) ->

61 {default proof { trivial; } p : isCons xs = True} -> a

62head (x :: xs) = x

63\end{code}

65\subsection{Implicit conversions}

67\Idris{} supports the creation of \emph{implicit conversions}, which allow

68automatic conversion of values from one type to another when required to make

69a term type correct. This is intended to increase convenience and reduce

70verbosity. A contrived but simple example is the following:

72\begin{code}

73implicit intString : Int -> String

74intString = show

76test : Int -> String

77test x = "Number " ++ x

78\end{code}

80\noindent

81In general, we cannot append an \texttt{Int} to a \texttt{String}, but the

82implicit conversion function \texttt{intString} can convert \texttt{x} to a

83\texttt{String}, so the definition of \texttt{test} is type correct. An

84implicit conversion is implemented just like any other function, but given

85the \texttt{implicit} modifier, and restricted to one explicit argument.

87Only one implicit conversion will be applied at a time. That is, implicit

88conversions cannot be chained.

89Implicit conversions of simple types, as above, are however discouraged! More

90commonly, an implicit conversion would be used to reduce verbosity in an

91embedded domain specific language, or to hide details of a proof. Such examples

92are beyond the scope of this tutorial.

94\subsection{Literate programming}

96Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an

97extension of \texttt{.lidr} then it is assumed to be a literate file. In literate

98programs, everything is assumed to be a comment unless the line begins with a

99greater than sign \texttt{>}, for example:

100

101\begin{lstlisting}

102> module literate

103

104This is a comment. The main program is below

105

106> main : IO ()

107> main = putStrLn "Hello literate world!\n"

108\end{lstlisting}

109

110\noindent

111An additional restriction is that there must be a blank line between a program

112line (beginning with \texttt{>}) and a comment line (beginning with any other

113character).

114

115\subsection{Foreign function calls}

116

117For practical programming, it is often necessary to be able to use external libraries,

118particularly for interfacing with the operating system, file system, networking, etc.

119\Idris{} provides a lightweight foreign function interface for achieving this,

120as part of the prelude. For this, we assume a certain amount of knowledge of

121C and the \texttt{gcc} compiler. First, we define a datatype which describes the external

122types we can handle:

123

124\begin{code}

126\end{code}

127

128\noindent

129Each of these corresponds directly to a C type. Respectively: \texttt{int},

130\texttt{double}, \texttt{char}, \texttt{char*}, \texttt{void*} and \texttt{void}.

131There is also a translation to a concrete \Idris{} type, described by the

132following function:

133

134\begin{code}

135interpFTy : FTy -> Type

136interpFTy FInt = Int

137interpFTy FFloat = Float

138interpFTy FChar = Char

139interpFTy FString = String

140interpFTy FPtr = Ptr

141interpFTy FUnit = ()

142\end{code}

143

144\noindent

145A foreign function is described by a list of input types and a return type, which

146can then be converted to an \Idris{} type:

147

148\begin{code}

149ForeignTy : (xs:List FTy) -> (t:FTy) -> Type

150\end{code}

151

152\noindent

153A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an

154\texttt{IO} type, for example:

155

156\begin{lstlisting}

157Idris> ForeignTy [FInt, FString] FString

158Int -> String -> IO String : Type

159

160Idris> ForeignTy [FInt, FString] FUnit

161Int -> String -> IO () : Type

162\end{lstlisting}

163

164\noindent

165We build a call to a foreign function by giving the name of the function, a list of

166argument types and the return type. The built in function \texttt{mkForeign}

167converts this description to a function callable by \Idris{}

168

169\begin{code}

170data Foreign : Type -> Type where

171 FFun : String -> (xs:List FTy) -> (t:FTy) ->

172 Foreign (ForeignTy xs t)

173

174mkForeign : Foreign x -> x

175\end{code}

176

177\noindent

178For example, the \texttt{putStr} function is implemented as follows, as a call to

179an external function \texttt{putStr} defined in the run-time system:

180

181\begin{code}

182putStr : String -> IO ()

183putStr x = mkForeign (FFun "putStr" [FString] FUnit) x

184\end{code}

185

186\subsubsection*{Include and linker directives}

187

188Foreign function calls are translated directly to calls to C functions, with appropriate

189conversion between the \Idris{} representation of a value and the C representation.

190Often this will require extra libraries to be linked in, or extra header and object files.

191This is made possible through the following directives:

192

193\begin{itemize}

194\item \texttt{\%lib \emph{target} "x"} --- include the \texttt{libx} library. If the target is \texttt{C} this is equivalent to passing the

195\texttt{-lx} option to \texttt{gcc}. If the target is Java the library will be interpreted as a

196"groupId:artifactId:packaging:version" dependency coordinate for maven.

197\item \texttt{\%include \emph{target} "x"} --- use the header file or import \texttt{x} for the given back end target.

198\item \texttt{\%link \emph{target} "x.o"} --- link with the object file \texttt{x.o} when using the given back end target.

199\item \texttt{\%dynamic "x.so"} --- dynamically link the interpreter with the shared object \texttt{x.so}.

200\end{itemize}

201

202\subsubsection*{Testing foreign function calls}

203Normally, the Idris interpreter (used for typechecking and at the REPL) will

204not perform IO actions. Additionally, as it neither generates C code nor

205compiles to machine code, the \texttt{\%lib}, \texttt{\%include} and

206\texttt{\%link} directives have no effect. IO actions and FFI calls can be

207tested using the special REPL command \texttt{:x EXPR}, and C libraries can be

208dynamically loaded in the interpreter by using the \texttt{:dynamic} command

209or the \texttt{\%dynamic} directive. For example:

210

211\begin{lstlisting}

212Idris> :dynamic libm.so

213Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)

2140.9995736030415051 : Float

215\end{lstlisting}

216

217\subsection{Type Providers}

218Idris type providers, inspired by F\#'s type providers, are a means of making

219our types be ``about'' something in the world outside of Idris. For example,

220given a type that represents a database schema and a query that is checked

221against it, a type provider could read the schema of a real database during

222type checking.

223

224Idris type providers use the ordinary execution semantics of Idris to run an

225IO action and extract the result. This result is then saved as a constant in

226the compiled code. It can be a type, in which case it is used like any other

227type, or it can be a value, in which case it can be used as any other value,

228including as an index in types.

229

230Type providers are still an experimental extension. To enable the extension,

231use the \texttt{\%language} directive:

232

233\begin{code}

234%language TypeProviders

235\end{code}

236

237A provider \texttt{p} for some type \texttt{t} is simply an expression of type

238\texttt{IO (Provider t)}. The \texttt{\%provide} directive causes the type

239checker to execute the action and bind the result to a name. This is perhaps

240best illustrated with a simple example. The type provider \texttt{fromFile}

241reads a text file. If the file consists of the string \texttt{"Int"}, then the

242type \texttt{Int} will be provided. Otherwise, it will provide the type

243\texttt{Nat}.

244

245\begin{code}

246strToType : String -> Type

247strToType "Int" = Int

248strToType _ = Nat

249

250fromFile : String -> IO (Provider Type)

251fromFile fname = do str <- readFile fname

252 return (Provide (strToType (trim str)))

253\end{code}

254

255We then use the \texttt{\%provide} directive:

256

257\begin{code}

258%provide (T1 : Type) with fromFile "theType"

259

260foo : T1

261foo = 2

262\end{code}

263

264\noindent

265If the file named \texttt{theType} consists of the word \texttt{Int}, then

266\texttt{foo} will be an \texttt{Int}. Otherwise, it will be a \texttt{Nat}.

267When Idris encounters the directive, it first checks that the provider

268expression \texttt{fromFile "theType"} has type \texttt{IO (Provider

269 Type)}. Next, it executes the provider. If the result is \texttt{Provide t},

270then \texttt{T1} is defined as \texttt{t}. Otherwise, the result is an error.

271

272Our datatype \texttt{Provider t} has the following definition:

273

274\begin{code}

275data Provider a = Error String

276 | Provide a

277\end{code}

278

279\noindent

280We have already seen the \texttt{Provide} constructor. The \texttt{Error}

281constructor allows type providers to return useful error messages. The

282example in this section was purposefully simple. More complex type provider

283implementations, including a statically-checked SQLite binding, are available

284in an external collection.\footnote{\url{https://github.com/david-christiansen/idris-type-providers}}

285

286\subsection{JavaScript Target}

287

288\Idris{} is capable of producing \emph{JavaScript} code that can be run in a browser

289as well as in the \emph{NodeJS} environment or alike. One can use the FFI to

290communicate with the \emph{JavaScript} ecosystem.

291

292\subsubsection*{Code Generation}

293

294\noindent

295Code generation is split into two separate targets. To generate code that is

296tailored for running in the browser issue the following command:

297

298\begin{lstlisting}[language=bash]

299$ idris --codegen javascript hello.idr -o hello.js

300\end{lstlisting}

301

302\noindent

303The resulting file can be embedded into your HTML just like any other

304\emph{JavaScript} code.

305

306\noindent

307Generating code for \emph{NodeJS} is slightly different. \Idris{} outputs

308a \emph{JavaScript} file that can be directly executed via \texttt{node}.

309

310\begin{lstlisting}[language=bash]

311$ idris --codegen node hello.idr -o hello

312$ ./hello

313Hello world

314\end{lstlisting}

315

316\noindent

317Take into consideration that the \emph{JavaScript} code generator is using

318\texttt{console.log} to write text to \texttt{stdout}, this means that it will

319automatically add a newline to the end of each string. This behavior

320does not show up in the \emph{NodeJS} code generator.

321

322\subsubsection*{Using the FFI}

323

324\noindent

325To write a useful application we need to communicate with the outside

326world. Maybe we want to manipulate the DOM or send an Ajax request. For this

327task we can use the FFI. Since most \emph{JavaScript} APIs demand callbacks

328we need to extend the FFI so we can pass functions as arguments.

329

330\noindent

331The \emph{JavaScript} FFI works a little bit differently than the regular FFI.

332It uses positional arguments to directly insert our arguments into a piece

333of \emph{JavaScript} code.

334

335\noindent

336One could use the primitive addition of \emph{JavaScript} like so:

337

338\begin{code}

339module Main

340

341primPlus : Int -> Int -> IO Int

342primPlus a b = mkForeign (FFun "%0 + %1" [FInt, FInt] FInt) a b

343

344main : IO ()

345main = do

346 a <- primPlus 1 1

347 b <- primPlus 1 2

348 print (a, b)

349\end{code}

350

351\noindent

352Notice that the \texttt{\%n} notation qualifies the position of the

353\texttt{n}-th argument given to our foreign function starting from 0. When

354you need a percent sign rather than a position simply use \texttt{\%\%}

355instead.

356

357\noindent

358Passing functions to a foreign function is very similar. Let's assume that

359we want to call the following function from the \emph{JavaScript} world:

360

361\begin{code}[language=c]

362function twice(f, x) {

363 return f(f(x));

364}

365\end{code}

366

367\noindent

368We obviously need to pass a function \texttt{f} here (we can infer it from

369the way we use \texttt{f} in \texttt{twice}, it would be more obvious if

370\emph{JavaScript} had types).

371

372\noindent

373The \emph{JavaScript} FFI is able to understand functions as arguments when

374you give it something of type \texttt{FFunction}. The following example code

375calls \texttt{twice} in \emph{JavaScript} and returns the result to our

376\Idris{} program:

377

378\begin{code}

379module Main

380

381twice : (Int -> Int) -> Int -> IO Int

382twice f x = mkForeign (

383 FFun "twice(%0,%1)" [FFunction FInt FInt, FInt] FInt

384) f x

385

386main : IO ()

387main = do

388 a <- twice (+1) 1

389 print a

390\end{code}

391

392\noindent

393The program outputs \texttt{3}, just like we expected.

394

395\subsubsection*{Shrinking down generated \emph{JavaScript}}

396

397\Idris{} can produce very big chunks of \emph{JavaScript} code. However, the

398generated code can be minified using the \texttt{closure-compiler} from

399Google. Any other minifier is also suitable but \texttt{closure-compiler}

400offers advanced compilation that does some aggressive inlining and code

401elimination. \Idris{} can take full advantage of this compilation mode and

402it's highly recommended to use it when shipping a \emph{JavaScript}

403application written in \Idris{}.

404

405\subsection{Cumulativity}

406

407Since values can appear in types and \emph{vice versa}, it is natural that types themselves

408have types. For example:

409

410\begin{lstlisting}

411*universe> :t Nat

412Nat : Type

413*universe> :t Vect

414Vect : Nat -> Type -> Type

415\end{lstlisting}

416

417\noindent

418But what about the type of \texttt{Type}? If we ask \Idris{} it reports

419

420\begin{lstlisting}

421*universe> :t Type

422Type : Type 1

423\end{lstlisting}

424

425\noindent

426If \texttt{Type} were its own type, it would lead to an inconsitency

427due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}

428of types (or \emph{universes}):

429

430\begin{code}

431Type : Type 1 : Type 2 : Type 3 : ...

432\end{code}

433

434\noindent

435Universes are \emph{cumulative}, that is, if \texttt{x : Type n} we can also have that

436\texttt{x : Type m}, as long as \texttt{n < m}.

437The typechecker generates such universe

438constraints and reports an error if any inconsistencies are found. Ordinarily, a

439programmer does not need to worry about this, but it does prevent (contrived)

440programs such as the following:

441

442\begin{code}

443myid : (a : Type) -> a -> a

444myid _ x = x

445

446idid : (a : Type) -> a -> a

447idid = myid _ myid

448\end{code}

449

450\noindent

451The application of \texttt{myid} to itself leads to a cycle in the universe hierarchy

452--- \texttt{myid}'s first argument is a \texttt{Type}, which cannot be at a lower level

453than required if it is applied to itself.

454

455%\subsection{Comparison}

456

457%How does \Idris{} compare with other dependently typed languages and proof

458%assistants, such as Coq, Agda and Epigram?