git.iko.soy/Idris-dev
on 52d8165 help sign in
Idris-dev/tutorial/content/dsl.tex
82 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\begin{code}
15fact : Expr G (TyFun TyInt TyInt)
16fact = Lam (If (Op (==) (Var stop) (Val 0))
17 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))
18 (Var stop)))
19\end{code}
21\noindent
22Since this is a particularly useful pattern, \Idris{} provides syntax
23overloading~\cite{res-dsl-padl12} to make it easier to program in such
24object languages:
26\begin{code}
27dsl expr
28 lambda = Lam
29 variable = Var
30 index_first = stop
31 index_next = pop
32\end{code}
34\noindent
35A \texttt{dsl} block describes how each syntactic construct is represented in an
36object language. Here, in the \texttt{expr} language, any \Idris{} lambda is
37translated to a \texttt{Lam} constructor; any variable is translated to the
38\texttt{Var} constructor, using \texttt{pop} and \texttt{stop} to construct the
39de Bruijn index (i.e., to count how many bindings since the variable itself was bound).
40It is also possible to overload \texttt{let} in this way. We can now write \texttt{fact}
41as follows:
43\begin{code}
44fact : Expr G (TyFun TyInt TyInt)
45fact = expr (\x => If (Op (==) x (Val 0))
46 (Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))
47\end{code}
49\noindent
50In this new version, \texttt{expr} declares that the next expression will be overloaded.
51We can take this further, using idiom brackets, by declaring:
53\begin{code}
54(<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
55(<$>) = \f, a => App f a
57pure : Expr G a -> Expr G a
58pure = id
59\end{code}
61\noindent
62Note that there is no need for these to be part of an instance of \texttt{Applicative},
63since idiom bracket notation translates directly to the names \texttt{<\$>} and
64\texttt{pure}, and ad-hoc type-directed overloading is allowed. We can now say:
66\begin{code}
67fact : Expr G (TyFun TyInt TyInt)
68fact = expr (\x => If (Op (==) x (Val 0))
69 (Val 1) (Op (*) [| fact (Op (-) x (Val 1)) |] x))
70\end{code}
72\noindent
73With some more ad-hoc overloading and type class instances, and a new
74syntax rule, we can even go as far as:
76\begin{code}
77syntax IF [x] THEN [t] ELSE [e] = If x t e
79fact : Expr G (TyFun TyInt TyInt)
80fact = expr (\x => IF x == 0 THEN 1 ELSE [| fact (x - 1) |] * x)
81\end{code}