Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

A bit of paper structure

  • Loading branch information...
commit 1d803f138904ca79e95cdc26ca46786d7ec74e9c 1 parent df28b80
Edwin Brady authored
View
1  Papers/Epic/epic.tex
@@ -31,6 +31,7 @@
\newcommand{\Idris}{\textsc{Idris}}
\newcommand{\Funl}{\textsc{Funl}}
\newcommand{\Agda}{\textsc{Agda}}
+\newcommand{\LamPi}{$\lambda_\Pi$}
\newcommand{\perule}[1]{\vspace*{0.1cm}\noindent
\begin{center}
View
122 Papers/Epic/example.tex
@@ -1,7 +1,121 @@
\section{Example High Level Languages}
-% Two different examples. Perhaps:
-% * a LOGO like language (foreign functions, graphics, dynamic types?)
-% * dependent types with natelim (e.g. adder)
+\subsection{Untyped $\lambda$-calculus}
+
+HOAS representation
+
+\begin{SaveVerbatim}{llang}
+
+data Lang = Lam (Lang -> Lang)
+ | Ref Name
+ | App Lang Lang
+ | Const Const
+ | Op Infix Lang Lang
+
+\end{SaveVerbatim}
+\useverb{llang}
+
+\begin{SaveVerbatim}{lconsts}
+
+data Const = CInt Int
+ | CStr String
+
+\end{SaveVerbatim}
+\useverb{lconsts}
+
+\begin{SaveVerbatim}{lops}
+
+data Infix = IPlus | IMinus | ITimes | IDivide | IAppend
+ | IEQ | ILT | IGT
+
+\end{SaveVerbatim}
+\useverb{lops}
+
+\begin{SaveVerbatim}{lprogs}
+
+data Def = LangDef Lang
+ | PrimDef EpicDecl
+
+type Defs = [(Name, Def)]
+
+\end{SaveVerbatim}
+\useverb{lprogs}
+
+\begin{SaveVerbatim}{lcompile}
+
+build :: Lang -> Term
+build (Lam f) = term (\x -> build (f (EpicRef x)))
+build (EpicRef x) = term x
+build (Ref n) = ref n
+build (App f a) = build f @@ build a
+build (Const (CInt x)) = int x
+build (Const (CStr x)) = str x
+build (Op IAppend l r) = fn "append" @@ build l @@ build r
+build (Op op l r) = op_ (eOp op) (build l) (build r)
+ where eOp IPlus = Plus
+ eOp IMinus = Minus
+ eOp ITimes = Times
+ eOp IDivide = Divide
+ eOp IEQ = OpEQ
+ eOp ILT = OpLT
+ eOp IGT = OpGT
+
+\end{SaveVerbatim}
+\codefig{lcompile}{Compiling Untyped $\lambda$-calculus}
+
+Conversion of terms to Epic expressions is given in Figure
+\ref{lcompile}. Some things to note. To compile a lambda, we need
+something to apply the lambda to. Easiest way to do this is extend the
+\texttt{Lang} datatype with an Epic reference:
+
+\begin{SaveVerbatim}{lextend}
+
+data Lang = ...
+ | EpicRef Expr
+
+build (Lam f) = term (\x -> build (f (EpicRef x)))
+
+\end{SaveVerbatim}
+\useverb{lextend}
+
+Might be better to have an environment or not use HOAS, but this is
+cheap and much less error prone than the alternatives.
+Compiling string append uses a built in function provided by the Epic
+interface in \texttt{basic\_defs}:
+
+\begin{SaveVerbatim}{lappend}
+
+build (Op IAppend l r) = fn "append" @@ build l @@ build r
+
+\end{SaveVerbatim}
+\useverb{lappend}
+
+Otherwise it's just a straightforward traversal of the term. Now we
+translate a list of HOAS definitions into an Epic program, add the
+Epic basic definitions, and run it. This runs the function called
+\texttt{"main"}. Epic will report an error if this doesn't exist.
+
+\begin{SaveVerbatim}{lmain}
+
+mkProgram :: Defs -> Program
+mkProgram ds = basic_defs ++
+ map (\ (n, d) -> (n, mkEpic d)) ds
+
+mkEpic :: Def -> EpicDecl
+mkEpic (PrimDef p) = p
+mkEpic (LangDef l) = EpicFn (build l)
+
+execute :: Defs -> IO ()
+execute p = run (mkProgram p)
+
+\end{SaveVerbatim}
+\useverb{lmain}
+
+\subsection{Dependently Typed $\lambda$-calculus}
+
+\LamPi{}~\cite{simply-easy}.
+
+\subsection{A Dynamically Typed Turtle Graphics Language}
+
+
-[Give high level translation, rather than concrete Haskell]
View
3  Papers/Epic/language.tex
@@ -90,4 +90,5 @@ \subsection{Implementation}
\subsection{Haskell API}
-(Give HOAS translation as an example)
+Function names. Distinction between Haskell application and Epic
+application (\texttt{@@}).
View
30 Papers/Epic/literature.bib
@@ -1,3 +1,33 @@
+@article{cbconc,
+ author = {Edwin Brady and
+ Kevin Hammond},
+ title = {Correct-by-Construction Concurrency: Using Dependent Types
+ to Verify Implementations of Effectful Resource Usage Protocols},
+ journal = {Fundam. Inform.},
+ volume = {102},
+ number = {2},
+ year = {2010},
+ pages = {145-176},
+ ee = {http://dx.doi.org/10.3233/FI-2010-303},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@article{simply-easy,
+ author = {Andres L{\"o}h and
+ Conor McBride and
+ Wouter Swierstra},
+ title = {A Tutorial Implementation of a Dependently Typed Lambda
+ Calculus},
+ journal = {Fundam. Inform.},
+ volume = {102},
+ number = {2},
+ year = {2010},
+ pages = {177-207},
+ ee = {http://dx.doi.org/10.3233/FI-2010-304},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+
@inproceedings{mitchell-super,
author = {Mitchell, Neil},
title = {Rethinking supercompilation},
Please sign in to comment.
Something went wrong with that request. Please try again.