git.iko.soy/Idris-dev
on ef93607 help sign in
Idris-dev/tutorial/dsl.tex
92 lines 2.9 kB history raw
1\subsection{\texttt{dsl} notation}
3The well-typed interpreter in Section \ref{sect:interp} is a simple example of
4a common programming pattern with dependent types, namely: describe an
5\emph{object language}
6and its type system with dependent types to guarantee that only well-typed programs
7can be represented, then program using that representation. Using this approach
8we can, for example, write programs for serialising binary data~\cite{plpv11} or
9running concurrent processes safely~\cite{cbconc-fi}.
11Unfortunately, the form of object language programs makes it rather hard to program
12this way in practice. Recall the factorial program in \texttt{Expr} for example:
14\useverb{facttest}
16\noindent
17Since this is a particularly useful pattern, \Idris{} provides syntax
18overloading~\cite{res-dsl-padl12} to make it easier to program in such
19object languages:
21\begin{SaveVerbatim}{exprdsl}
23dsl expr
24 lambda = Lam
25 variable = Var
26 index_first = stop
27 index_next = pop
29\end{SaveVerbatim}
30\useverb{exprdsl}
32\noindent
33A \texttt{dsl} block describes how each syntactic construct is represented in an
34object language. Here, in the \texttt{expr} language, any \Idris{} lambda is
35translated to a \texttt{Lam} constructor; any variable is translated to the
36\texttt{Var} constructor, using \texttt{pop} and \texttt{stop} to construct the
37de Bruijn index (i.e., to count how many bindings since the variable itself was bound).
38It is also possible to overload \texttt{let} in this way. We can now write \texttt{fact}
39as follows:
41\begin{SaveVerbatim}{factb}
43fact : Expr G (TyFun TyInt TyInt)
44fact = expr (\x => If (Op (==) x (Val 0))
45 (Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))
47\end{SaveVerbatim}
48\useverb{factb}
50\noindent
51In this new version, \texttt{expr} declares that the next expression will be overloaded.
52We can take this further, using idiom brackets, by declaring:
54\begin{SaveVerbatim}{idiomexpr}
56(<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
57(<$>) = \f, a => App f a
59pure : Expr G a -> Expr G a
60pure = id
62\end{SaveVerbatim}
63\useverb{idiomexpr}
65\noindent
66Note that there is no need for these to be part of an instance of \texttt{Applicative},
67since idiom bracket notation translates directly to the names \texttt{<\$>} and
68\texttt{pure}, and ad-hoc type-directed overloading is allowed. We can now say:
70\begin{SaveVerbatim}{factc}
72fact : Expr G (TyFun TyInt TyInt)
73fact = expr (\x => If (Op (==) x (Val 0))
74 (Val 1) (Op (*) [| fact (Op (-) x (Val 1)) |] x))
76\end{SaveVerbatim}
77\useverb{factc}
79\noindent
80With some more ad-hoc overloading and type class instances, and a new
81syntax rule, we can even go as far as:
83\begin{SaveVerbatim}{factd}
85syntax IF [x] THEN [t] ELSE [e] = If x t e
87fact : Expr G (TyFun TyInt TyInt)
88fact = expr (\x => IF x == 0 THEN 1 ELSE [| fact (x - 1) |] * x)
90\end{SaveVerbatim}
91\useverb{factd}