Permalink
Browse files

Document named instances

  • Loading branch information...
Edwin Brady
Edwin Brady committed May 4, 2012
1 parent ec631d7 commit 4bbbf1dc969119ee7113f631a5f8e0d73d2b8ff3
Showing with 47 additions and 1 deletion.
  1. +46 −0 tutorial/classes.tex
  2. +1 −1 tutorial/miscellany.tex
View
@@ -482,3 +482,49 @@ \subsubsection{An error-handling interpreter}
\end{SaveVerbatim}
\useverb{evalexpr}
+\subsection{Named Instances}
+
+It can be desirable to have multiple instances of a type class, for example to provide
+alternative methods for sorting or printing values. To achieve this, instances can
+be \remph{named} as follows:
+
+\begin{SaveVerbatim}{myord}
+
+instance [myord] Ord Nat where
+ compare O (S n) = GT
+ compare (S n) O = LT
+ compare O O = EQ
+ compare (S x) (S y) = compare @{myord} x y
+
+\end{SaveVerbatim}
+\useverb{myord}
+
+\noindent
+This declares an instance as normal, but with an explicit name, \texttt{myord}.
+The syntax \texttt{compare @\{myord\}} gives an explicit instance to
+\texttt{compare}, otherwise it would use the default instance for \texttt{Nat}.
+We can use this, for example, to sort a list of \texttt{Nat}s in reverse.
+Given the following list:
+
+\begin{SaveVerbatim}{myordlist}
+
+testList : List Nat
+testList = [3,4,1]
+
+\end{SaveVerbatim}
+\useverb{myordlist}
+
+\noindent
+\ldots we can sort it using the default \texttt{Ord} instance, then the named
+instance \texttt{myord} as follows, at the \Idris{} prompt:
+
+\begin{SaveVerbatim}{myordlistrun}
+
+*named_instance> show (sort testList)
+"[sO, sssO, ssssO]" : String
+*named_instance> show (sort @{myord} testList)
+"[ssssO, sssO, sO]" : String
+
+\end{SaveVerbatim}
+\useverb{myordlist}
+
View
@@ -114,7 +114,7 @@ \subsection{Foreign function calls}
\noindent
Each of these corresponds directly to a C type. Respectively: \texttt{int},
-\texttt{float}, \texttt{char}, \texttt{char*}, \texttt{void*} and \texttt{void}.
+\texttt{double}, \texttt{char}, \texttt{char*}, \texttt{void*} and \texttt{void}.
There is also a translation to a concrete \Idris{} type, described by the
following function:

0 comments on commit 4bbbf1d

Please sign in to comment.