Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Idiom brackets and dsl notation in tutorial

  • Loading branch information...
commit 7e2765b2d1161c0847ecb5155e5c1965d8cabaee 1 parent 392c225
Edwin Brady authored
View
2  lib/prelude.idr
@@ -108,7 +108,7 @@ instance Applicative Maybe where
pure = Just
(Just f) <$> (Just a) = Just (f a)
- Nothing <$> Nothing = Nothing
+ _ <$> _ = Nothing
---- some mathematical operations
View
23 samples/interp.idr
@@ -44,6 +44,25 @@ using (G : Vect Ty n)
pure = id
syntax IF [x] THEN [t] ELSE [e] = If x t e
+
+ (==) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool
+ (==) = Op (==)
+
+ -- Some dummy instances for Num overloading
+ instance Eq (Expr G TyInt) where
+ (==) x y = False
+
+ instance Ord (Expr G TyInt) where
+ compare x y = EQ
+
+ instance Num (Expr G TyInt) where
+ (+) x y = Op (+) x y
+ (-) x y = Op (-) x y
+ (*) x y = Op (*) x y
+
+ abs x = If (Op (<) x (Val 0)) (Op (-) 0 x) x
+
+ fromInteger = Val
interp : Env G -> {static} Expr G t -> interpTy t
interp env (Var i) = lookup i env
@@ -67,9 +86,7 @@ using (G : Vect Ty n)
eDouble = expr (\x => App (App eAdd x) (Var stop))
eFac : Expr G (TyFun TyInt TyInt)
- eFac = expr (\x => IF Op (==) x (Val 0)
- THEN Val 1
- ELSE Op (*) [| eFac (Op (-) x (Val 1)) |] x)
+ eFac = expr (\x => IF x == 0 THEN 1 ELSE [| eFac (x - 1) |] * x)
testFac : Int
testFac = interp [] eFac 4
View
44 src/Idris/ElabTerm.hs
@@ -101,7 +101,8 @@ elab ist info pattern tcgen fn tm
(elab' ina (PRef fc unitTy))
elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes
- = resolveTC 2 fn ist
+ = do let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
+ resolveTC 2 fn insts ist
elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
instanceArg c
elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
@@ -233,7 +234,8 @@ elab ist info pattern tcgen fn tm
ivs' <- get_instances
when (not pattern || (ina && not tcgen)) $
mapM_ (\n -> do focus n
- resolveTC 7 fn ist) (ivs' \\ ivs)
+ let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
+ resolveTC 7 fn insts ist) (ivs' \\ ivs)
where tcArg (n, PConstraint _ _ Placeholder) = True
tcArg _ = False
@@ -337,10 +339,10 @@ trivial ist = try (do elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf
(MN 0 "tac") (PRef (FC "prf" 0) x))
(tryAll xs)
-resolveTC :: Int -> Name -> IState -> ElabD ()
-resolveTC 0 fn ist = fail $ "Can't resolve type class"
-resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)
-resolveTC depth fn ist
+resolveTC :: Int -> Name -> [Name] -> IState -> ElabD ()
+resolveTC 0 fn insts ist = fail $ "Can't resolve type class"
+resolveTC 1 fn insts ist = try (trivial ist) (resolveTC 0 fn insts ist)
+resolveTC depth fn insts ist
= try (trivial ist)
(do t <- goal
let (tc, ttypes) = unApply t
@@ -349,7 +351,7 @@ resolveTC depth fn ist
-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
let depth' = if scopeOnly then 2 else depth
- blunderbuss t depth' (map fst (ctxtAlist (tt_ctxt ist))))
+ blunderbuss t depth' insts)
where
elabTC n | n /= fn && tcname n = (resolve n depth, show n)
| otherwise = (fail "Can't resolve", show n)
@@ -367,25 +369,29 @@ resolveTC depth fn ist
boundVar _ = False
blunderbuss t d [] = lift $ tfail $ CantResolve t
- blunderbuss t d (n:ns) | n /= fn && tcname n = try (resolve n d)
- (blunderbuss t d ns)
- | otherwise = blunderbuss t d ns
+ blunderbuss t d (n:ns)
+ | n /= fn && tcname n = try (resolve n d)
+ (blunderbuss t d ns)
+ | otherwise = blunderbuss t d ns
resolve n depth
| depth == 0 = fail $ "Can't resolve type class"
| otherwise
- = do t <- goal
+ = do t <- goal
+ let (tc, ttypes) = unApply t
+-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
+-- else do
-- if there's a hole in the goal, don't even try
- let imps = case lookupCtxtName Nothing n (idris_implicits ist) of
+ let imps = case lookupCtxtName Nothing n (idris_implicits ist) of
[] -> []
[args] -> map isImp (snd args) -- won't be overloaded!
- args <- apply (Var n) imps
- tm <- get_term
- mapM_ (\ (_,n) -> do focus n
- resolveTC (depth - 1) fn ist)
- (filter (\ (x, y) -> not x) (zip (map fst imps) args))
- -- if there's any arguments left, we've failed to resolve
- solve
+ args <- apply (Var n) imps
+-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
+ mapM_ (\ (_,n) -> do focus n
+ resolveTC (depth - 1) fn insts ist)
+ (filter (\ (x, y) -> not x) (zip (map fst imps) args))
+ -- if there's any arguments left, we've failed to resolve
+ solve
where isImp (PImp p _ _ _) = (True, p)
isImp arg = (False, priority arg)
View
2  tutorial/Makefile
@@ -4,7 +4,7 @@ all: ${PAPER}.pdf
TEXFILES = ${PAPER}.tex intro.tex starting.tex miscellany.tex typesfuns.tex \
classes.tex modules.tex interp.tex views.tex theorems.tex \
- provisional.tex syntax.tex conclusions.tex miscellany.tex
+ provisional.tex syntax.tex conclusions.tex miscellany.tex dsl.tex
DIAGS =
View
75 tutorial/classes.tex
@@ -312,4 +312,79 @@ \subsubsection*{Monad comprehensions}
\end{SaveVerbatim}
\useverb{maddb}
+\subsection{Idiom brackets}
+
+While \texttt{do} notation gives an alternative meaning to sequencing, idioms give an
+alternative meaning to \emph{application}. The notation and larger example in this
+section is inspired by Conor McBride and Ross Paterson's paper "Applicative
+Programming with Effects"~\cite{idioms}.
+
+First, let us revisit \texttt{m\_add} above. All it is really doing is applying
+an operator to two values extracted from Maybe Ints. We could abstract out the
+application:
+
+\begin{SaveVerbatim}{mapp}
+
+m_app : Maybe (a -> b) -> Maybe a -> Maybe b
+m_app (Just f) (Just a) = Just (f a)
+m_app _ _ = Nothing
+
+\end{SaveVerbatim}
+\useverb{mapp}
+
+\noindent
+Using this, we can write an alternative \texttt{m\_add} which uses this alternative
+notion of function application, with explicit calls to \texttt{m\_app}:
+
+\begin{SaveVerbatim}{maddb}
+
+m_add' : Maybe Int -> Maybe Int -> Maybe Int
+m_add' x y = m_app (m_app (Just (+)) x) y
+
+\end{SaveVerbatim}
+\useverb{maddb}
+
+\noindent
+Rather than having to insert \texttt{m\_app} everywhere there is an application, we can
+use \remph{idiom brackets} to do the job for us. To do this, we use the \texttt{Applicative}
+class, which captures the notion of application for a data type:
+
+\begin{SaveVerbatim}{applicative}
+
+infixl 2 <$>
+
+class Applicative (f : Set -> Set) where
+ pure : a -> f a
+ (<$>) : f (a -> b) -> f a -> f b
+
+\end{SaveVerbatim}
+\useverb{applicative}
+
+\noindent
+\texttt{Maybe} is made an instance of \texttt{Applicative} as follows, where \texttt{<\$>}
+is defined in the same way as \texttt{m\_app} above:
+
+\begin{SaveVerbatim}{maybeapp}
+
+instance Applicative Maybe where
+ pure = Just
+
+ (Just f) <$> (Just a) = Just (f a)
+ _ <$> _ = Nothing
+
+\end{SaveVerbatim}
+\useverb{maybeapp}
+
+\noindent
+Using \remph{idiom brackets} we can use this instance as follows, where a function
+application \texttt{[| f a1 ... an |]}
+is translated into \texttt{pure f <\$> a1 <\$> ... <\$> an}:
+
+\begin{SaveVerbatim}{maddc}
+
+m_add' : Maybe Int -> Maybe Int -> Maybe Int
+m_add' x y = [| x + y |]
+
+\end{SaveVerbatim}
+\useverb{maddc}
View
92 tutorial/dsl.tex
@@ -0,0 +1,92 @@
+\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}
+
View
1  tutorial/idris-tutorial.tex
@@ -29,6 +29,7 @@
\input{theorems}
\input{provisional}
\input{miscellany}
+\input{dsl}
\input{conclusions}
\bibliographystyle{abbrv}
View
2  tutorial/interp.tex
@@ -1,5 +1,7 @@
\section{Example: The Well-Typed Interpreter}
+\label{sect:interp}
+
In this section, we'll use the features we've seen so far to write a larger
example, an interpreter for a simple functional programming language, with
variables, function application, binary operators and an \texttt{if...then...else}
View
2  tutorial/typesfuns.tex
@@ -840,7 +840,7 @@ \subsubsection*{Dependent Pairs}
\begin{SaveVerbatim}{vfilternil}
-vfilter p Nil = (_ , [])
+filter p Nil = (_ , [])
\end{SaveVerbatim}
\useverb{vfilternil}
View
8 tutorial/views.tex
@@ -4,14 +4,14 @@ \subsection{Dependent pattern matching}
Since types can depend on values, the form of some arguments can be determined
by the value of others. For example, if we were to write down the implicit
-length arguments to \texttt{app}, we'd see that the form of the length argument was
+length arguments to \texttt{(++)}, we'd see that the form of the length argument was
determined by whether the vector was empty or not:
\begin{SaveVerbatim}{appdep}
-app : Vect a n -> Vect a m -> Vect a (n + m)
-app {n=O} [] [] = []
-app {n=S k} (x :: xs) ys = x :: app xs ys
+(++) : Vect a n -> Vect a m -> Vect a (n + m)
+(++) {n=O} [] [] = []
+(++) {n=S k} (x :: xs) ys = x :: xs ++ ys
\end{SaveVerbatim}
\useverb{appdep}
Please sign in to comment.
Something went wrong with that request. Please try again.