@@ -3,7 +3,7 @@
33In this section we discuss a variety of additional features:
44auto implicit and default
55arguments, literate programming, interfacing with external libraries through the
6−foreign function interface, and the universe hierarchy.
6+foreign function interface, type providers, and the universe hierarchy.
77
88\subsection{Auto implicit arguments}
99
@@ -241,11 +241,96 @@ dynamically loaded in the interpreter by using the \texttt{:dynamic} command
241241or the \texttt{\%dynamic} directive. For example:
242242
243243\begin{SaveVerbatim}{xdynamic}
244+
244245Idris> :dynamic libm.so
245246Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
2462470.9995736030415051 : Float
248+
247249\end{SaveVerbatim}
248250\useverb{xdynamic}
251+
252+\subsection{Type Providers}
253+Idris type providers, inspired by F\#'s type providers, are a means of making
254+our types be ``about'' something in the world outside of Idris. For example,
255+given a type that represents a database schema and a query that is checked
256+against it, a type provider could read the schema of a real database during
257+type checking.
258+
259+Idris type providers use the ordinary execution semantics of Idris to run an
260+IO action and extract the result. This result is then saved as a constant in
261+the compiled code. It can be a type, in which case it is used like any other
262+type, or it can be a value, in which case it can be used as any other value,
263+including as an index in types.
264+
265+Type providers are still an experimental extension. To enable the extension,
266+use the \texttt{\%language} directive:
267+\begin{SaveVerbatim}{languageProv}
268+
269+%language TypeProviders
270+
271+\end{SaveVerbatim}
272+
273+\useverb{languageProv}
274+
275+
276+A provider \texttt{p} for some type \texttt{t} is simply an expression of type
277+\texttt{IO (Provider t)}. The \texttt{\%provide} directive causes the type
278+checker to execute the action and bind the result to a name. This is perhaps
279+best illustrated with a simple example. The type provider \texttt{fromFile}
280+reads a text file. If the file consists of the string \texttt{"Int"}, then the
281+type \texttt{Int} will be provided. Otherwise, it will provide the type
282+\texttt{Nat}.
283+
284+\begin{SaveVerbatim}{fromFile}
285+
286+strToType : String -> Type
287+strToType "Int" = Int
288+strToType _ = Nat
289+
290+fromFile : String -> IO (Provider Type)
291+fromFile fname = do str <- readFile fname
292+ return (Provide (strToType (trim str)))
293+
294+\end{SaveVerbatim}
295+\useverb{fromFile}
296+
297+We then use the \texttt{\%provide} directive:
298+
299+\begin{SaveVerbatim}{fromFileUse}
300+
301+%provide (T1 : Type) with fromFile "theType"
302+
303+foo : T1
304+foo = 2
305+
306+\end{SaveVerbatim}
307+\useverb{fromFileUse}
308+
309+\noindent
310+If the file named \texttt{theType} consists of the word \texttt{Int}, then
311+\texttt{foo} will be an \texttt{Int}. Otherwise, it will be a \texttt{Nat}.
312+When Idris encounters the directive, it first checks that the provider
313+expression \texttt{fromFile "theType"} has type \texttt{IO (Provider
314+ Type)}. Next, it executes the provider. If the result is \texttt{Provide t},
315+then \texttt{T1} is defined as \texttt{t}. Otherwise, the result is an error.
316+
317+Our datatype \texttt{Provider t} has the following definition:
318+
319+\begin{SaveVerbatim}{providerdef}
320+
321+data Provider a = Error String
322+ | Provide a
323+
324+\end{SaveVerbatim}
325+\useverb{providerdef}
326+
327+\noindent
328+We have already seen the \texttt{Provide} constructor. The \texttt{Error}
329+constructor allows type providers to return useful error messages. The
330+example in this section was purposefully simple. More complex type provider
331+implementations, including a statically-checked SQLite binding, are available
332+in an external collection.\footnote{\url{https://github.com/david-christiansen/idris-type-providers}}
333+
249334\subsection{Cumulativity}
250335
251336Since values can appear in types and \emph{vice versa}, it is natural that types themselves