git.iko.soy/Idris-dev
on 73ea02b help sign in
Idris-dev/docs/tutorial/syntax.rst
208 lines 8.1 kB history raw
1Syntax Extensions
2=================
4supports the implementation of *Embedded Domain Specific Languages*
5(EDSLs) in several ways [1]_. One way, as we have already seen, is
6through extending ``do`` notation. Another important way is to allow
7extension of the core syntax. In this section we describe two ways of
8extending the syntax: ``syntax`` rules and ``dsl`` notation.
10``syntax`` rules
11----------------
13We have seen ``if...then...else`` expressions, but these are not built
14in. Instead, we can define a function in the prelude as follows (we
15have already seen this function in Section :ref:`sect-lazy`):
17.. code-block:: idris
19 boolCase : (x:Bool) -> Lazy a -> Lazy a -> a;
20 boolCase True t e = t;
21 boolCase False t e = e;
23and then extend the core syntax with a ``syntax`` declaration:
25.. code-block:: idris
27 syntax "if" [test] "then" [t] "else" [e] = boolCase test t e;
29The left hand side of a ``syntax`` declaration describes the syntax
30rule, and the right hand side describes its expansion. The syntax rule
31itself consists of:
33- **Keywords** — here, ``if``, ``then`` and ``else``, which must be
34 valid identifiers
36- **Non-terminals** — included in square brackets, ``[test]``, ``[t]``
37 and ``[e]`` here, which stand for arbitrary expressions. To avoid
38 parsing ambiguities, these expressions cannot use syntax extensions
39 at the top level (though they can be used in parentheses).
41- **Names** — included in braces, which stand for names which may be
42 bound on the right hand side.
44- **Symbols** — included in quotations marks, e.g. ``:=``. This can
45 also be used to include reserved words in syntax rules, such as
46 ``let`` or ``in``.
48The limitations on the form of a syntax rule are that it must include
49at least one symbol or keyword, and there must be no repeated
50variables standing for non-terminals. Any expression can be used, but
51if there are two non-terminals in a row in a rule, only simple
52expressions may be used (that is, variables, constants, or bracketed
53expressions). Rules can use previously defined rules, but may not be
54recursive. The following syntax extensions would therefore be valid:
56.. code-block:: idris
58 syntax [var] ":=" [val] = Assign var val;
59 syntax [test] "?" [t] ":" [e] = if test then t else e;
60 syntax "select" [x] "from" [t] "where" [w] = SelectWhere x t w;
61 syntax "select" [x] "from" [t] = Select x t;
63Syntax macros can be further restricted to apply only in patterns (i.e.,
64only on the left hand side of a pattern match clause) or only in terms
65(i.e. everywhere but the left hand side of a pattern match clause) by
66being marked as ``pattern`` or ``term`` syntax rules. For example, we
67might define an interval as follows, with a static check that the lower
68bound is below the upper bound using ``so``:
70.. code-block:: idris
72 data Interval : Type where
73 MkInterval : (lower : Float) -> (upper : Float) ->
74 so (lower < upper) -> Interval
76We can define a syntax which, in patterns, always matches ``oh`` for
77the proof argument, and in terms requires a proof term to be provided:
79.. code-block:: idris
81 pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
82 term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
84In terms, the syntax ``[x...y]`` will generate a proof obligation
85``bounds_lemma`` (possibly renamed).
87Finally, syntax rules may be used to introduce alternative binding
88forms. For example, a ``for`` loop binds a variable on each iteration:
90.. code-block:: idris
92 syntax "for" {x} "in" [xs] ":" [body] = forLoop xs (\x => body)
94 main : IO ()
95 main = do for x in [1..10]:
96 putStrLn ("Number " ++ show x)
97 putStrLn "Done!"
99Note that we have used the ``{x}`` form to state that ``x`` represents
100a bound variable, substituted on the right hand side. We have also put
101``in`` in quotation marks since it is already a reserved word.
103``dsl`` notation
104----------------
106The well-typed interpreter in Section :ref:`sect-interp` is a simple
107example of a common programming pattern with dependent types. Namely:
108describe an *object language* and its type system with dependent types
109to guarantee that only well-typed programs can be represented, then
110program using that representation. Using this approach we can, for
111example, write programs for serialising binary data [2]_ or running
112concurrent processes safely [3]_.
114Unfortunately, the form of object language programs makes it rather
115hard to program this way in practice. Recall the factorial program in
116``Expr`` for example:
118.. code-block:: idris
120 fact : Expr G (TyFun TyInt TyInt)
121 fact = Lam (If (Op (==) (Var Stop) (Val 0))
122 (Val 1) (Op (*) (app fact (Op (-) (Var Stop) (Val 1)))
123 (Var Stop)))
125Since this is a particularly useful pattern, Idris provides syntax
126overloading [1]_ to make it easier to program in such object
127languages:
129.. code-block:: idris
131 mkLam : TTName -> Expr (t::g) t' -> Expr g (TyFun t t')
132 mkLam _ body = Lam body
134 dsl expr
135 variable = Var
136 index_first = Stop
137 index_next = Pop
138 lambda = mkLam
140A ``dsl`` block describes how each syntactic construct is represented
141in an object language. Here, in the ``expr`` language, any variable is
142translated to the ``Var`` constructor, using ``Pop`` and ``Stop`` to
143construct the de Bruijn index (i.e., to count how many bindings since
144the variable itself was bound); and any lambda is translated to a
145``Lam`` constructor. The ``mkLam`` function simply ignores its first
146argument, which is the name that the user chose for the variable. It
147is also possible to overload ``let`` and dependent function syntax
148(``pi``) in this way. We can now write ``fact`` as follows:
150.. code-block:: idris
152 fact : Expr G (TyFun TyInt TyInt)
153 fact = expr (\x => If (Op (==) x (Val 0))
154 (Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))
156In this new version, ``expr`` declares that the next expression will
157be overloaded. We can take this further, using idiom brackets, by
158declaring:
160.. code-block:: idris
162 (<$>) : (f : Lazy (Expr G (TyFun a t))) -> Expr G a -> Expr G t
163 (<$>) f a = App f a
165 pure : Expr G a -> Expr G a
166 pure = id
168Note that there is no need for these to be part of an instance of
169``Applicative``, since idiom bracket notation translates directly to
170the names ``<*>`` and ``pure``, and ad-hoc type-directed overloading
171is allowed. We can now say:
173.. code-block:: idris
175 fact : Expr G (TyFun TyInt TyInt)
176 fact = expr (\x => If (Op (==) x (Val 0))
177 (Val 1) (Op (*) [| fact (Op (-) x (Val 1)) |] x))
179With some more ad-hoc overloading and type class instances, and a new
180syntax rule, we can even go as far as:
182.. code-block:: idris
184 syntax "IF" [x] "THEN" [t] "ELSE" [e] = If x t e
186 fact : Expr G (TyFun TyInt TyInt)
187 fact = expr (\x => IF x == 0 THEN 1 ELSE [| fact (x - 1) |] * x)
190.. [1] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems
191 programming with embedded domain specific languages. In
192 Proceedings of the 14th international conference on Practical
193 Aspects of Declarative Languages (PADL'12), Claudio Russo and
194 Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,
195 242-257. DOI=10.1007/978-3-642-27694-1_18
196 http://dx.doi.org/10.1007/978-3-642-27694-1_18
198.. [2] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
199 dependent types. In Proceedings of the 5th ACM workshop on
200 Programming languages meets program verification (PLPV
201 '11). ACM, New York, NY, USA,
202 43-54. DOI=10.1145/1929529.1929536
203 http://doi.acm.org/10.1145/1929529.1929536
205.. [3] Edwin Brady and Kevin Hammond. 2010. Correct-by-Construction
206 Concurrency: Using Dependent Types to Verify Implementations of
207 Effectful Resource Usage Protocols. Fundam. Inf. 102, 2 (April
208 2010), 145-176. http://dl.acm.org/citation.cfm?id=1883636