git.iko.soy/Idris-dev
on 50878fa help sign in
Idris-dev/docs/reference/syntax-guide.rst
401 lines 7.8 kB history raw
1**************
2Syntax Guide
3**************
5Examples are mostly adapted from the Idris tutorial.
7Source File Structure
8---------------------
10Source files consist of:
121. An optional :ref:`syntax-module-headers`.
132. Zero or more :ref:`syntax-imports`.
143. Zero or more declarations, e.g. :ref:`syntax-variables`,
15 :ref:`syntax-data-types`, etc.
17For example:
19.. code:: idris
21 module MyModule -- module header
23 import Data.Vect -- an import
25 %default total -- a directive
27 foo : Nat -- a declaration
28 foo = 5
30.. _syntax-module-headers:
32Module Header
33~~~~~~~~~~~~~
35A file can start with a module header, introduced by the ``module`` keyword:
37.. code-block:: idris
39 module Semantics
41Module names can be hierarchical, with parts separated by ``.``:
43.. code-block:: idris
45 module Semantics.Transform
47Each file can define only a single module, which includes everything defined in
48that file.
50Like with declarations, a :ref:`docstring <syntax-comments>` can be used to
51provide documentation for a module:
53.. code-block:: idris
55 ||| Implementation of predicate transformer semantics.
56 module Semantics.Transform
58.. _syntax-imports:
60Imports
61~~~~~~~
63An ``import`` makes the names in another module available for use by the current
64module:
66.. code-block:: idris
68 import Data.Vect
70All the declarations in an imported module are available for use in the file.
71In a case where a name is ambiguous --- e.g. because it is imported from
72multiple modules, or appears in multiple visible namespaces --- the ambiguity can be resolved using :ref:`syntax-qualified-names`. (Often, the compiler can
73resolve the ambiguity for you, using the types involved.)
75Imported modules can be given aliases to make qualified names more compact:
77.. code-block:: idris
79 import Data.Vect as V
81Note that names made visible by import are not, by default, re-exported to
82users of the module being written. This can be done using ``import public``:
84.. code-block:: idris
86 import public Data.Vect
88.. _syntax-variables:
90Variables
91---------
93A variable is always defined by defining its type on one line, and its
94value on the next line, using the syntax
96::
98 <id> : <type>
99 <id> = <value>
101Examples
103.. code:: idris
105 x : Int
106 x = 100
107 hello : String
108 hello = "hello"
110Types
111-----
113In Idris, types are first class values. So a type declaration is the
114same as just declaration of a variable whose type is ``Type``. In Idris,
115variables that denote a type must begin with a capital letter. Example:
117.. code:: idris
119 MyIntType : Type
120 MyIntType = Int
122a more interesting example:
124.. code:: idris
126 MyListType : Type
127 MyListType = List Int
129.. _syntax-data-types:
131Data types
132~~~~~~~~~~
134Idris provides two kinds of syntax for defining data types. The first,
135Haskell style syntax, defines a regular algebraic data type. For example
137.. code:: idris
139 data Either a b = Left a | Right b
141or
143.. code:: idris
145 data List a = Nil | (::) a (List a)
147The second, more general kind of data type, is defined using Agda or
148GADT style syntax. This syntax defines a data type that is parameterised
149by some values (in the ``Vect`` example, a value of type ``Nat`` and a
150value of type ``Type``).
152.. code:: idris
154 data Vect : Nat -> Type -> Type where
155 Nil : Vect Z a
156 (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
158Operators
159---------
161Arithmetic
162~~~~~~~~~~
164::
166 x + y
167 x - y
168 x * y
169 x / y
170 (x * y) + (a / b)
172Equality and Relational
173~~~~~~~~~~~~~~~~~~~~~~~
175::
177 x == y
178 x /= y
179 x >= y
180 x > y
181 x <= y
182 x < y
184Conditional
185~~~~~~~~~~~
187::
189 x && y
190 x || y
191 not x
193Conditionals
194------------
196If Then Else
197~~~~~~~~~~~~
199::
201 if <test> then <true> else <false>
203Case Expressions
204~~~~~~~~~~~~~~~~
206::
208 case <test> of
209 <case 1> => <expr>
210 <case 2> => <expr>
211 ...
212 otherwise => <expr>
214Functions
215---------
217Named
218~~~~~
220Named functions are defined in the same way as variables, with the type
221followed by the definition.
223::
225 <id> : <argument type> -> <return type>
226 <id> arg = <expr>
228Example
230.. code:: idris
232 plusOne : Int -> Int
233 plusOne x = x + 1
235Functions can also have multiple inputs, for example
237.. code:: idris
239 makeHello : String -> String -> String
240 makeHello first last = "hello, my name is " ++ first ++ " " ++ last
242Functions can also have named arguments. This is required if you want to
243annotate parameters in a docstring. The following shows the same
244``makeHello`` function as above, but with named parameters which are
245also annotated in the docstring
247.. code:: idris
249 ||| Makes a string introducing a person
250 ||| @first The person's first name
251 ||| @last The person's last name
252 makeHello : (first : String) -> (last : String) -> String
253 makeHello first last = "hello, my name is " ++ first ++ " " ++ last
255Like Haskell, Idris functions can be defined by pattern matching. For
256example
258.. code:: idris
260 sum : List Int -> Int
261 sum [] = 0
262 sum (x :: xs) = x + (sum xs)
264Similarly case analysis looks like
266.. code:: idris
268 answerString : Bool -> String
269 answerString False = "Wrong answer"
270 answerString True = "Correct answer"
272Dependent Functions
273~~~~~~~~~~~~~~~~~~~
275Dependent functions are functions where the type of the return value
276depends on the input value. In order to define a dependent function,
277named parameters must be used, since the parameter will appear in the
278return type. For example, consider
280.. code:: idris
282 zeros : (n : Nat) -> Vect n Int
283 zeros Z = []
284 zeros (S k) = 0 :: (zeros k)
286In this example, the return type is ``Vect n Int`` which is an
287expression which depends on the input parameter ``n``. ### Anonymous
288Arguments in anonymous functions are separated by comma.
290::
292 (\x => <expr>)
293 (\x, y => <expr>)
295Modifiers
296~~~~~~~~~
298Visibility
299^^^^^^^^^^
301::
303 public
304 abstract
305 private
307Totality
308^^^^^^^^
310::
312 total
313 implicit
314 partial
315 covering
317Options
318^^^^^^^
320::
322 %export
323 %hint
324 %no_implicit
325 %error_handler
326 %error_reverse
327 %assert_total
328 %reflection
329 %specialise [<name list>]
331Misc
332----
334.. _syntax-qualified-names:
336Qualified Names
337~~~~~~~~~~~~~~~
339If multiple declarations with the same name are visible, using the name can
340result in an ambiguous situation. The compiler will attempt to resolve the
341ambiguity using the types involved. If it's unable --- for example, because
342the declarations with the same name also have the same type signatures --- the
343situation can be cleared up using a *qualified name*.
345A qualified name has the symbol's namespace prefixed, separated by a ``.``:
347.. code-block:: idris
349 Data.Vect.length
351This would specifically reference a ``length`` declaration from ``Data.Vect``.
353Qualified names can be written using two different shorthands:
3551. Names in modules that are :ref:`imported <syntax-imports>` using an alias
356 can be qualified by the alias.
3582. The name can be qualified by the *shortest unique suffix* of the
359 namespace in question. For example, the ``length`` case above can likely
360 be shortened to ``Vect.length``.
362.. _syntax-comments:
364Comments
365~~~~~~~~
367::
369 -- Single Line
370 {- Multiline -}
371 ||| Docstring (goes before definition)
373Multi line String literals
374~~~~~~~~~~~~~~~~~~~~~~~~~~
376::
378 foo = """
379 this is a
380 string literal"""
382.. _syntax-directives:
384Directives
385----------
387::
389 %lib <path>
390 %link <path>
391 %flag <path>
392 %include <path>
393 %hide <function>
394 %freeze <name>
395 %access <accessibility>
396 %default <totality>
397 %logging <level 0--11>
398 %dynamic <list of libs>
399 %name <list of names>
400 %error_handlers <list of names>
401 %language <extension>