7e2765b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Idiom brackets and dsl notation in tutorial

7e2765bEdwin Brady15 years ago

lib/prelude.idr+1−1

compare with master

unifiedsplit

@@ -108,7 +108,7 @@ instance Applicative Maybe where

108 pure = Just

109

110 (Just f) <$> (Just a) = Just (f a)

111− Nothing <$> Nothing = Nothing

111+ _ <$> _ = Nothing

112

113

114---- some mathematical operations

samples/interp.idr+20−3

@@ -44,6 +44,25 @@ using (G : Vect Ty n)

44 pure = id

46 syntax IF [x] THEN [t] ELSE [e] = If x t e

47+

48+ (==) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool

49+ (==) = Op (==)

50+

51+ -- Some dummy instances for Num overloading

52+ instance Eq (Expr G TyInt) where

53+ (==) x y = False

54+

55+ instance Ord (Expr G TyInt) where

56+ compare x y = EQ

57+

58+ instance Num (Expr G TyInt) where

59+ (+) x y = Op (+) x y

60+ (-) x y = Op (-) x y

61+ (*) x y = Op (*) x y

62+

63+ abs x = If (Op (<) x (Val 0)) (Op (-) 0 x) x

64+

65+ fromInteger = Val

48 interp : Env G -> {static} Expr G t -> interpTy t

67 interp : Env G -> {static} Expr G t -> interpTy t

49 interp env (Var i) = lookup i env

68 interp env (Var i) = lookup i env

@@ -67,9 +86,7 @@ using (G : Vect Ty n)

67 eDouble = expr (\x => App (App eAdd x) (Var stop))

86 eDouble = expr (\x => App (App eAdd x) (Var stop))

69 eFac : Expr G (TyFun TyInt TyInt)

88 eFac : Expr G (TyFun TyInt TyInt)

70− eFac = expr (\x => IF Op (==) x (Val 0)

89+ eFac = expr (\x => IF x == 0 THEN 1 ELSE [| eFac (x - 1) |] * x)

71− THEN Val 1

72− ELSE Op (*) [| eFac (Op (-) x (Val 1)) |] x)

74testFac : Int

91testFac : Int

75testFac = interp [] eFac 4

92testFac = interp [] eFac 4

src/Idris/ElabTerm.hs+25−19

@@ -101,7 +101,8 @@ elab ist info pattern tcgen fn tm

101 (elab' ina (PRef fc unitTy))

102 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)

103 elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes

104+ = do let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

104− = resolveTC 2 fn ist

105+ resolveTC 2 fn insts ist

105 elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")

106 elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")

106 instanceArg c

107 instanceArg c

107 elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

108 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

233 ivs' <- get_instances

234 ivs' <- get_instances

234 when (not pattern || (ina && not tcgen)) $

235 when (not pattern || (ina && not tcgen)) $

235 mapM_ (\n -> do focus n

236 mapM_ (\n -> do focus n

237+ let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

236− resolveTC 7 fn ist) (ivs' \\ ivs)

238+ resolveTC 7 fn insts ist) (ivs' \\ ivs)

237 where tcArg (n, PConstraint _ _ Placeholder) = True

239 where tcArg (n, PConstraint _ _ Placeholder) = True

238 tcArg _ = False

240 tcArg _ = False

239

241

@@ -337,10 +339,10 @@ trivial ist = try (do elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf

337 (MN 0 "tac") (PRef (FC "prf" 0) x))

339 (MN 0 "tac") (PRef (FC "prf" 0) x))

338 (tryAll xs)

340 (tryAll xs)

339

341

340−resolveTC :: Int -> Name -> IState -> ElabD ()

342+resolveTC :: Int -> Name -> [Name] -> IState -> ElabD ()

341−resolveTC 0 fn ist = fail $ "Can't resolve type class"

343+resolveTC 0 fn insts ist = fail $ "Can't resolve type class"

342−resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)

344+resolveTC 1 fn insts ist = try (trivial ist) (resolveTC 0 fn insts ist)

343−resolveTC depth fn ist

345+resolveTC depth fn insts ist

344 = try (trivial ist)

346 = try (trivial ist)

345 (do t <- goal

347 (do t <- goal

346 let (tc, ttypes) = unApply t

348 let (tc, ttypes) = unApply t

@@ -349,7 +351,7 @@ resolveTC depth fn ist

349-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $

351-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $

350-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

352-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

351 let depth' = if scopeOnly then 2 else depth

353 let depth' = if scopeOnly then 2 else depth

352− blunderbuss t depth' (map fst (ctxtAlist (tt_ctxt ist))))

354+ blunderbuss t depth' insts)

353 where

355 where

354 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

356 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

355 | otherwise = (fail "Can't resolve", show n)

357 | otherwise = (fail "Can't resolve", show n)

@@ -367,25 +369,29 @@ resolveTC depth fn ist

367 boundVar _ = False

369 boundVar _ = False

368

370

369 blunderbuss t d [] = lift $ tfail $ CantResolve t

371 blunderbuss t d [] = lift $ tfail $ CantResolve t

372+ blunderbuss t d (n:ns)

370− blunderbuss t d (n:ns) | n /= fn && tcname n = try (resolve n d)

373+ | n /= fn && tcname n = try (resolve n d)

371− (blunderbuss t d ns)

374+ (blunderbuss t d ns)

372− | otherwise = blunderbuss t d ns

375+ | otherwise = blunderbuss t d ns

373

376

374 resolve n depth

377 resolve n depth

375 | depth == 0 = fail $ "Can't resolve type class"

378 | depth == 0 = fail $ "Can't resolve type class"

376 | otherwise

379 | otherwise

377− = do t <- goal

380+ = do t <- goal

381+ let (tc, ttypes) = unApply t

382+-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist

383+-- else do

378 -- if there's a hole in the goal, don't even try

384 -- if there's a hole in the goal, don't even try

379− let imps = case lookupCtxtName Nothing n (idris_implicits ist) of

385+ let imps = case lookupCtxtName Nothing n (idris_implicits ist) of

380 [] -> []

386 [] -> []

381 [args] -> map isImp (snd args) -- won't be overloaded!

387 [args] -> map isImp (snd args) -- won't be overloaded!

382− args <- apply (Var n) imps

388+ args <- apply (Var n) imps

383− tm <- get_term

389+-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

384− mapM_ (\ (_,n) -> do focus n

390+ mapM_ (\ (_,n) -> do focus n

385− resolveTC (depth - 1) fn ist)

391+ resolveTC (depth - 1) fn insts ist)

386− (filter (\ (x, y) -> not x) (zip (map fst imps) args))

392+ (filter (\ (x, y) -> not x) (zip (map fst imps) args))

387− -- if there's any arguments left, we've failed to resolve

393+ -- if there's any arguments left, we've failed to resolve

388− solve

394+ solve

389 where isImp (PImp p _ _ _) = (True, p)

395 where isImp (PImp p _ _ _) = (True, p)

390 isImp arg = (False, priority arg)

396 isImp arg = (False, priority arg)

391

397

tutorial/Makefile+1−1

@@ -4,7 +4,7 @@ all: ${PAPER}.pdf

5TEXFILES = ${PAPER}.tex intro.tex starting.tex miscellany.tex typesfuns.tex \

6 classes.tex modules.tex interp.tex views.tex theorems.tex \

7− provisional.tex syntax.tex conclusions.tex miscellany.tex

7+ provisional.tex syntax.tex conclusions.tex miscellany.tex dsl.tex

9DIAGS =

tutorial/classes.tex+75

@@ -312,4 +312,79 @@ m_add x y = [ x' + y' | x' <- x, y' <- y ]

312\end{SaveVerbatim}

313\useverb{maddb}

314

315+\subsection{Idiom brackets}

316+

317+While \texttt{do} notation gives an alternative meaning to sequencing, idioms give an

318+alternative meaning to \emph{application}. The notation and larger example in this

319+section is inspired by Conor McBride and Ross Paterson's paper "Applicative

320+Programming with Effects"~\cite{idioms}.

321+

322+First, let us revisit \texttt{m\_add} above. All it is really doing is applying

323+an operator to two values extracted from Maybe Ints. We could abstract out the

324+application:

325+

326+\begin{SaveVerbatim}{mapp}

327+

328+m_app : Maybe (a -> b) -> Maybe a -> Maybe b

329+m_app (Just f) (Just a) = Just (f a)

330+m_app _ _ = Nothing

331+

332+\end{SaveVerbatim}

333+\useverb{mapp}

334+

335+\noindent

336+Using this, we can write an alternative \texttt{m\_add} which uses this alternative

337+notion of function application, with explicit calls to \texttt{m\_app}:

338+

339+\begin{SaveVerbatim}{maddb}

340+

341+m_add' : Maybe Int -> Maybe Int -> Maybe Int

342+m_add' x y = m_app (m_app (Just (+)) x) y

343+

344+\end{SaveVerbatim}

345+\useverb{maddb}

346+

347+\noindent

348+Rather than having to insert \texttt{m\_app} everywhere there is an application, we can

349+use \remph{idiom brackets} to do the job for us. To do this, we use the \texttt{Applicative}

350+class, which captures the notion of application for a data type:

351+

352+\begin{SaveVerbatim}{applicative}

353+

354+infixl 2 <$>

355+

356+class Applicative (f : Set -> Set) where

357+ pure : a -> f a

358+ (<$>) : f (a -> b) -> f a -> f b

359+

360+\end{SaveVerbatim}

361+\useverb{applicative}

362+

363+\noindent

364+\texttt{Maybe} is made an instance of \texttt{Applicative} as follows, where \texttt{<\$>}

365+is defined in the same way as \texttt{m\_app} above:

366+

367+\begin{SaveVerbatim}{maybeapp}

368+

369+instance Applicative Maybe where

370+ pure = Just

371+

372+ (Just f) <$> (Just a) = Just (f a)

373+ _ <$> _ = Nothing

374+

375+\end{SaveVerbatim}

376+\useverb{maybeapp}

377+

378+\noindent

379+Using \remph{idiom brackets} we can use this instance as follows, where a function

380+application \texttt{[| f a1 ... an |]}

381+is translated into \texttt{pure f <\$> a1 <\$> ... <\$> an}:

382+

383+\begin{SaveVerbatim}{maddc}

384+

385+m_add' : Maybe Int -> Maybe Int -> Maybe Int

386+m_add' x y = [| x + y |]

387+

388+\end{SaveVerbatim}

389+\useverb{maddc}

315

390

tutorial/dsl.texnew file+92

@@ -0,0 +1,92 @@

1+\section{More on overloading: \texttt{dsl} notation}

3+The well-typed interpreter in Section \ref{sect:interp} is a simple example of

4+a common programming pattern with dependent types, namely: describe an

5+\emph{object language}

6+and its type system with dependent types to guarantee that only well-typed programs

7+can be represented, then program using that representation. Using this approach

8+we can, for example, write programs for serialising binary data~\cite{plpv11} or

9+running concurrent processes safely~\cite{cbconc-fi}.

10+

11+Unfortunately, the form of object language programs makes it rather hard to program

12+this way in practice. Recall the factorial program in \texttt{Expr} for example:

13+

14+\useverb{facttest}

15+

16+\noindent

17+Since this is a particularly useful pattern, \Idris{} provides syntax

18+overloading~\cite{res-dsl-padl12} to make it easier to program in such

19+object languages:

20+

21+\begin{SaveVerbatim}{exprdsl}

22+

23+dsl expr

24+ lambda = Lam

25+ variable = Var

26+ index_first = stop

27+ index_next = pop

28+

29+\end{SaveVerbatim}

30+\useverb{exprdsl}

31+

32+\noindent

33+A \texttt{dsl} block describes how each syntactic construct is represented in an

34+object language. Here, in the \texttt{expr} language, any \Idris{} lambda is

35+translated to a \texttt{Lam} constructor; any variable is translated to the

36+\texttt{Var} constructor, using \texttt{pop} and \texttt{stop} to construct the

37+de Bruijn index (i.e., to count how many bindings since the variable itself was bound).

38+It is also possible to overload \texttt{let} in this way. We can now write \texttt{fact}

39+as follows:

40+

41+\begin{SaveVerbatim}{factb}

42+

43+fact : Expr G (TyFun TyInt TyInt)

44+fact = expr (\x => If (Op (==) x (Val 0))

45+ (Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))

46+

47+\end{SaveVerbatim}

48+\useverb{factb}

49+

50+\noindent

51+In this new version, \texttt{expr} declares that the next expression will be overloaded.

52+We can take this further, using idiom brackets, by declaring:

53+

54+\begin{SaveVerbatim}{idiomexpr}

55+

56+(<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

57+(<$>) = \f, a => App f a

58+

59+pure : Expr G a -> Expr G a

60+pure = id

61+

62+\end{SaveVerbatim}

63+\useverb{idiomexpr}

64+

65+\noindent

66+Note that there is no need for these to be part of an instance of \texttt{Applicative},

67+since idiom bracket notation translates directly to the names \texttt{<\$>} and

68+\texttt{pure}, and ad-hoc type-directed overloading is allowed. We can now say:

69+

70+\begin{SaveVerbatim}{factc}

71+

72+fact : Expr G (TyFun TyInt TyInt)

73+fact = expr (\x => If (Op (==) x (Val 0))

74+ (Val 1) (Op (*) [| fact (Op (-) x (Val 1)) |] x))

75+

76+\end{SaveVerbatim}

77+\useverb{factc}

78+

79+\noindent

80+With some more ad-hoc overloading and type class instances, and a new

81+syntax rule, we can even go as far as:

82+

83+\begin{SaveVerbatim}{factd}

84+

85+syntax IF [x] THEN [t] ELSE [e] = If x t e

86+

87+fact : Expr G (TyFun TyInt TyInt)

88+fact = expr (\x => IF x == 0 THEN 1 ELSE [| efact (x - 1) |] * x)

89+

90+\end{SaveVerbatim}

91+\useverb{factd}

92+

tutorial/idris-tutorial.tex+1

@@ -29,6 +29,7 @@

29\input{theorems}

30\input{provisional}

31\input{miscellany}

32+\input{dsl}

32\input{conclusions}

33\input{conclusions}

34\bibliographystyle{abbrv}

35\bibliographystyle{abbrv}

tutorial/interp.tex+2

@@ -1,5 +1,7 @@

1\section{Example: The Well-Typed Interpreter}

3+\label{sect:interp}

3In this section, we'll use the features we've seen so far to write a larger

5In this section, we'll use the features we've seen so far to write a larger

4example, an interpreter for a simple functional programming language, with

6example, an interpreter for a simple functional programming language, with

5variables, function application, binary operators and an \texttt{if...then...else}

7variables, function application, binary operators and an \texttt{if...then...else}

tutorial/typesfuns.tex+1−1

@@ -840,7 +840,7 @@ If the \texttt{Vect} is empty, the result is easy:

840

841\begin{SaveVerbatim}{vfilternil}

842

843−vfilter p Nil = (_ , [])

843+filter p Nil = (_ , [])

844

845\end{SaveVerbatim}

846\useverb{vfilternil}

tutorial/views.tex+4−4

@@ -4,14 +4,14 @@

5Since types can depend on values, the form of some arguments can be determined

6by the value of others. For example, if we were to write down the implicit

7−length arguments to \texttt{app}, we'd see that the form of the length argument was

7+length arguments to \texttt{(++)}, we'd see that the form of the length argument was

8determined by whether the vector was empty or not:

10\begin{SaveVerbatim}{appdep}

12−app : Vect a n -> Vect a m -> Vect a (n + m)

12+(++) : Vect a n -> Vect a m -> Vect a (n + m)

13−app {n=O} [] [] = []

13+(++) {n=O} [] [] = []

14−app {n=S k} (x :: xs) ys = x :: app xs ys

14+(++) {n=S k} (x :: xs) ys = x :: xs ++ ys

16\end{SaveVerbatim}

17\useverb{appdep}