Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

93 lines (66 sloc) 2.945 kb
\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 [| efact (x - 1) |] * x)
\end{SaveVerbatim}
\useverb{factd}
Jump to Line
Something went wrong with that request. Please try again.