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