@@ -3,7 +3,7 @@
3In this section we discuss a variety of additional features:
3In this section we discuss a variety of additional features:
4auto implicit and default
4auto implicit and default
5arguments, literate programming, interfacing with external libraries through the
5arguments, literate programming, interfacing with external libraries through the
6−foriegn function interface, and the universe hierarchy.
6+foreign function interface, type providers, and the universe hierarchy.
8\subsection{Auto implicit arguments}
8\subsection{Auto implicit arguments}
@@ -241,11 +241,96 @@ dynamically loaded in the interpreter by using the \texttt{:dynamic} command
241or the \texttt{\%dynamic} directive. For example:
241or the \texttt{\%dynamic} directive. For example:
243\begin{SaveVerbatim}{xdynamic}
243\begin{SaveVerbatim}{xdynamic}
244Idris> :dynamic libm.so
245Idris> :dynamic libm.so
245Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
246Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
2460.9995736030415051 : Float
2470.9995736030415051 : Float
247\end{SaveVerbatim}
249\end{SaveVerbatim}
248\useverb{xdynamic}
250\useverb{xdynamic}
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
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.
265+Type providers are still an experimental extension. To enable the extension,
266+use the \texttt{\%language} directive:
267+\begin{SaveVerbatim}{languageProv}
269+%language TypeProviders
273+\useverb{languageProv}
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
284+\begin{SaveVerbatim}{fromFile}
286+strToType : String -> Type
287+strToType "Int" = Int
290+fromFile : String -> IO (Provider Type)
291+fromFile fname = do str <- readFile fname
292+ return (Provide (strToType (trim str)))
297+We then use the \texttt{\%provide} directive:
299+\begin{SaveVerbatim}{fromFileUse}
301+%provide (T1 : Type) with fromFile "theType"
307+\useverb{fromFileUse}
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.
317+Our datatype \texttt{Provider t} has the following definition:
319+\begin{SaveVerbatim}{providerdef}
321+data Provider a = Error String
325+\useverb{providerdef}
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}}
249\subsection{Cumulativity}
334\subsection{Cumulativity}
251Since values can appear in types and \emph{vice versa}, it is natural that types themselves
336Since values can appear in types and \emph{vice versa}, it is natural that types themselves