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