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