Permalink
Browse files

First complete tutorial draft

  • Loading branch information...
1 parent ebbcf8d commit 310ca03a73c238d54c69c4aec030e7eda4bb82bd Edwin Brady committed Jan 1, 2012
View
@@ -35,20 +35,10 @@ ForeignTy xs t = mkForeign' (rev xs) (IO (interpFTy t)) where {
mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty);
}
-namespace foreign {
- infixr 7 :: ;
-
- data FEnv : List FTy -> Set where
- Nil : FEnv Nil
- | (::) : {xs:List FTy} ->
- interpFTy x -> FEnv xs -> FEnv (x ::xs);
-
- data Foreign : Set -> Set where
- FFun : String -> (xs:List FTy) -> (t:FTy) ->
- Foreign (ForeignTy xs t);
-
-}
+data Foreign : Set -> Set where
+ FFun : String -> (xs:List FTy) -> (t:FTy) ->
+ Foreign (ForeignTy xs t);
mkForeign : Foreign x -> x;
-- mkForeign compiled as primitive
View
@@ -1,2 +1,13 @@
\section{Further Reading}
+Further information about \Idris{} programming, and programming with dependent
+types in general, can be obtained from various sources:
+
+\begin{itemize}
+\item The \Idris{} web site (\url{http://idris-lang.org/}) and by asking questions
+on the mailing list.
+\item Examining the prelude and exploring the \texttt{samples} in the distribution.
+\item Various papers (e.g. \cite{plpv11, scrap-engine,res-dsl-padl12}). These mostly describe
+older versions of \Idris{}.
+\end{itemize}
+
@@ -37,7 +37,7 @@ using (G : Vect Ty n) {
interp env (App f s) = (interp env f) (interp env s);
interp env (Op op x y) = op (interp env x) (interp env y);
interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);
-
+
eId : Expr G (TyFun TyInt TyInt);
eId = Lam (Var stop);
View
Binary file not shown.
@@ -28,7 +28,6 @@
\input{views}
\input{theorems}
\input{provisional}
-\input{syntax}
\input{miscellany}
\input{conclusions}
View
@@ -1,3 +1,13 @@
+@inproceedings{res-dsl-padl12,
+ title = {Resource-safe Systems Programming with Embedded Domain Specific Languages},
+ year = {2012},
+ booktitle = {Practical Applications of Declarative Languages 2012},
+ author = {Edwin Brady and Kevin Hammond},
+ series = {LNCS},
+ publisher = {Springer},
+ note = {To appear}
+}
+
@article{lambdapi,
author = {Andres L\"{o}h and Conor McBride and Wouter Swierstra},
title = {A tutorial implementation of a dependently typed lambda calculus},
View
@@ -1,13 +1,139 @@
\section{Miscellany}
-Small things which don't quite fit elsewhere:
+In this section we discuss a variety of additional features: extensible syntax,
+literate programming, and interfacing with external libraries through the
+foriegn function interface.
+
+\input{syntax}
+
+\subsection{Literate programming}
+
+Like Haskell, \Idris{} supports \emph{literate} programming. If a file has an
+extension of \texttt{.lidr} then it is assumed to be a literate file. In literate
+programs, everything is assumed to be a comment unless the line begins with a
+greater than sign \texttt{>}, for example:
+
+\begin{SaveVerbatim}{litidr}
+
+> module literate;
+
+This is a comment. The main program is below
+
+> main : IO ();
+> main = putStrLn "Hello literate world!\n";
+
+\end{SaveVerbatim}
+\useverb{litidr}
+
+\noindent
+An additional restriction is that there must be a blank line between a program
+line (beginning with \texttt{>}) and a comment line (beginning with any other
+character).
+
+\subsection{Foreign function calls}
+
+For practical programming, it is often necessary to be able to use external libraries,
+particularly for interfacing with the operating system, file system, networking, etc.
+\Idris{} provides a lightweight foreign function interface for achieving this,
+as part of the prelude. For this, we assume a certain amount of knowledge of
+C and the \texttt{gcc} compiler. First, we define a datatype which describes the external
+types we can handle:
+
+\begin{SaveVerbatim}{foreignty}
+
+data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit;
+
+\end{SaveVerbatim}
+\useverb{foreignty}
+
+\noindent
+Each of these corresponds directly to a C type. Respectively: \texttt{int},
+\texttt{float}, \texttt{char}, \texttt{char*}, \texttt{void*} and \texttt{void}.
+There is also a translation to a concrete \Idris{} type, described by the
+following function:
+
+\begin{SaveVerbatim}{interpfty}
+
+interpFTy : FTy -> Set;
+interpFTy FInt = Int;
+interpFTy FFloat = Float;
+interpFTy FChar = Char;
+interpFTy FString = String;
+interpFTy FPtr = Ptr;
+interpFTy FUnit = ();
+
+\end{SaveVerbatim}
+\useverb{interpfty}
+
+\noindent
+A foreign function is described by a list of input types and a return type, which
+can then be converted to an \Idris{} type:
+
+\begin{SaveVerbatim}{ffunty}
+
+ForeignTy : (xs:List FTy) -> (t:FTy) -> Set;
+
+\end{SaveVerbatim}
+\useverb{ffunty}
+
+\noindent
+A foreign function is assumed to be impure, so \texttt{ForeignTy} builds an
+\texttt{IO} type, for example:
+
+\begin{SaveVerbatim}{ftyex}
+
+Idris> ForeignTy [FInt, FString] FString
+Int -> String -> IO String : Set
+
+Idris> ForeignTy [FInt, FString] FUnit
+Int -> String -> IO () : Set
+
+\end{SaveVerbatim}
+\useverb{ftyex}
+
+\noindent
+We build a call to a foreign function by giving the name of the function, a list of
+argument types and the return type. The built in function \texttt{mkForeign}
+converts this description to a function callable by \Idris{}
+
+\begin{SaveVerbatim}{mkForeign}
+
+data Foreign : Set -> Set where
+ FFun : String -> (xs:List FTy) -> (t:FTy) ->
+ Foreign (ForeignTy xs t);
+
+mkForeign : Foreign x -> x;
+
+\end{SaveVerbatim}
+\useverb{mkForeign}
+
+\noindent
+For example, the \texttt{putStr} function is implemented as follows, as a call to
+an external function \texttt{putStr} defined in the run-time system:
+
+\begin{SaveVerbatim}{putStrex}
+
+putStr : String -> IO ();
+putStr x = mkForeign (FFun "putStr" [FString] FUnit) x;
+
+\end{SaveVerbatim}
+\useverb{putStrex}
+
+\subsubsection*{Include and linker directives}
+
+Foreign function calls are translated directly to calls to C functions, with appropriate
+conversion between the \Idris{} representation of a value and the C representation.
+Often this will require extra libraries to be linked in, or extra header and object files.
+This is made possible through the following directives:
\begin{itemize}
-\item Literate programming
-\item Foreign functions
+\item \texttt{\%lib "x"} --- include the \texttt{libx} library, equivalent to passing the
+\texttt{-lx} option to \texttt{gcc}.
+\item \texttt{\%include "x.h"} --- use the header file \texttt{x.h}.
+\item \texttt{\%obj "x.o"} --- link with the object file \texttt{x.o}.
\end{itemize}
-\subsection{Comparison}
+%\subsection{Comparison}
-How does \Idris{} compare with other dependently typed languages and proof
-assistants, such as Coq, Agda and Epigram?
+%How does \Idris{} compare with other dependently typed languages and proof
+%assistants, such as Coq, Agda and Epigram?
View
@@ -1 +1,53 @@
-\section{Syntax Extensions}
+\subsection{Syntax Extensions}
+
+\Idris{} supports the implementation of Embedded Domain Specific Languages (EDSLs) in
+several ways~\cite{res-dsl-padl12}. One way, as we have already seen, is through
+extending \texttt{do} notation. Another important way is to allow extension of the core
+syntax. For example, we have seen \texttt{if...then...else} expressions, but these
+are not built in --- instead, we define a function in the prelude\ldots
+
+\begin{SaveVerbatim}{boolelim}
+
+boolElim : (x:Bool) -> |(t : a) -> |(f : a) -> a;
+boolElim True t e = t;
+boolElim False t e = e;
+
+\end{SaveVerbatim}
+\useverb{boolelim}
+
+\noindent
+\ldots and extend the core syntax with a \texttt{syntax} declaration:
+
+\begin{SaveVerbatim}{syntaxif}
+
+syntax if [test] then [t] else [e] = boolElim test t e;
+
+\end{SaveVerbatim}
+\useverb{syntaxif}
+
+\noindent
+The left hand side of a \texttt{syntax} declaration describes the syntax rule, and the right
+hand side describes its expansion. The syntax rule itself consists of:
+
+\begin{itemize}
+\item \textbf{Keywords} --- here, \texttt{if}, \texttt{then} and \texttt{else}, which must
+be valid identifiers
+\item \textbf{Non-terminals} --- included in square brackets, \texttt{[test]}, \texttt{[t]}
+and \texttt{[e]} here, which stand for arbitrary expressions
+\item \textbf{Symbols} --- included in quotations marks, e.g. \texttt{":="}
+\end{itemize}
+
+\noindent
+The only limitations on the form of a syntax rule are that it must include at least one
+symbol or keyword, and there must be no repeated variables standing for non-terminals.
+The following syntax extensions would therefore be valid:
+
+\begin{SaveVerbatim}{syntaxex}
+
+syntax [var] ":=" [val] = Assign var val
+syntax select [x] from [t] = Select x t;
+syntax select [x] from [t] where [w] = SelectWhere x t w;
+
+\end{SaveVerbatim}
+\useverb{syntaxex}
+

0 comments on commit 310ca03

Please sign in to comment.