git.iko.soy/Idris-dev
on 3323d0c help sign in
Idris-dev/docs/reference/syntax-guide.rst
476 lines 9.5 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 need not be capitalised. Example:
117.. code:: idris
119 MyIntType : Type
120 MyIntType = Int
122a more interesting example:
124.. code:: idris
126 MyListType : Type
127 MyListType = List Int
129While capitalising types is not required, the rules for generating implicit
130arguments mean it is often a good idea.
132.. _syntax-data-types:
134Data types
135~~~~~~~~~~
137Idris provides two kinds of syntax for defining data types. The first,
138Haskell style syntax, defines a regular algebraic data type. For example
140.. code:: idris
142 data Either a b = Left a | Right b
144or
146.. code:: idris
148 data List a = Nil | (::) a (List a)
150The second, more general kind of data type, is defined using Agda or
151GADT style syntax. This syntax defines a data type that is parameterised
152by some values (in the ``Vect`` example, a value of type ``Nat`` and a
153value of type ``Type``).
155.. code:: idris
157 data Vect : Nat -> Type -> Type where
158 Nil : Vect Z a
159 (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
161The signature of type constructors may use dependent types
163.. code:: idris
165 data DPair : (a : Type) -> (a -> Type) -> Type where
166 MkDPair : {P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P
168Records
169~~~~~~~
171There is a special syntax for data types with one constructors and
172multiple fields.
174.. code:: idris
176 record A a where
177 constructor MkA
178 foo, bar : a
179 baz : Nat
181This defines a constructor as well as getter and setter function for
182each field.
184.. code:: idris
186 MkA : a -> a -> Nat -> A a
187 foo : A a -> a
188 set_foo : a -> A a -> A a
190The types of record fields may depend on the value of other fields
192.. code:: idris
194 record Collection a where
195 constructor MkCollection
196 size : Nat
197 items : Vect size a
199Setter functions are only provided for fields that do not use dependant
200types. In the example above neither ``set_size`` nor ``set_items`` are
201defined.
204Co-data
205~~~~~~~
207Inifinite data structures can be introduced with the ``codata``
208keyword.
210.. code:: idris
212 codata Stream : Type -> Type where
213 (::) a -> Stream a -> Stream a
215This is syntactic sugar for
217.. code:: idris
219 data Stream : Type -> Type where
220 (::) a -> Delayed Infinite (Stream a) -> Stream a
222Every occurence of the the defined type in a constructor argument will
223be wrapped in the ``Delayed Infinite`` type constructor. This has the
224effect of delaying the evaluation of the second argument when the data
225constructor is applied. The argument is only evaluated when we pattern
226match against the constructor.
229Operators
230---------
232Arithmetic
233~~~~~~~~~~
235::
237 x + y
238 x - y
239 x * y
240 x / y
241 (x * y) + (a / b)
243Equality and Relational
244~~~~~~~~~~~~~~~~~~~~~~~
246::
248 x == y
249 x /= y
250 x >= y
251 x > y
252 x <= y
253 x < y
255Conditional
256~~~~~~~~~~~
258::
260 x && y
261 x || y
262 not x
264Conditionals
265------------
267If Then Else
268~~~~~~~~~~~~
270::
272 if <test> then <true> else <false>
274Case Expressions
275~~~~~~~~~~~~~~~~
277::
279 case <test> of
280 <case 1> => <expr>
281 <case 2> => <expr>
282 ...
283 otherwise => <expr>
285Functions
286---------
288Named
289~~~~~
291Named functions are defined in the same way as variables, with the type
292followed by the definition.
294::
296 <id> : <argument type> -> <return type>
297 <id> arg = <expr>
299Example
301.. code:: idris
303 plusOne : Int -> Int
304 plusOne x = x + 1
306Functions can also have multiple inputs, for example
308.. code:: idris
310 makeHello : String -> String -> String
311 makeHello first last = "hello, my name is " ++ first ++ " " ++ last
313Functions can also have named arguments. This is required if you want to
314annotate parameters in a docstring. The following shows the same
315``makeHello`` function as above, but with named parameters which are
316also annotated in the docstring
318.. code:: idris
320 ||| Makes a string introducing a person
321 ||| @first The person's first name
322 ||| @last The person's last name
323 makeHello : (first : String) -> (last : String) -> String
324 makeHello first last = "hello, my name is " ++ first ++ " " ++ last
326Like Haskell, Idris functions can be defined by pattern matching. For
327example
329.. code:: idris
331 sum : List Int -> Int
332 sum [] = 0
333 sum (x :: xs) = x + (sum xs)
335Similarly case analysis looks like
337.. code:: idris
339 answerString : Bool -> String
340 answerString False = "Wrong answer"
341 answerString True = "Correct answer"
343Dependent Functions
344~~~~~~~~~~~~~~~~~~~
346Dependent functions are functions where the type of the return value
347depends on the input value. In order to define a dependent function,
348named parameters must be used, since the parameter will appear in the
349return type. For example, consider
351.. code:: idris
353 zeros : (n : Nat) -> Vect n Int
354 zeros Z = []
355 zeros (S k) = 0 :: (zeros k)
357In this example, the return type is ``Vect n Int`` which is an
358expression which depends on the input parameter ``n``.
360Anonymous
361~~~~~~~~~
363Arguments in anonymous functions are separated by comma.
365::
367 (\x => <expr>)
368 (\x, y => <expr>)
370Modifiers
371~~~~~~~~~
373Visibility
374^^^^^^^^^^
376::
378 public export
379 export
380 private
382Totality
383^^^^^^^^
385::
387 total
388 implicit
389 partial
390 covering
392Options
393^^^^^^^
395::
397 %export
398 %hint
399 %no_implicit
400 %error_handler
401 %error_reverse
402 %assert_total
403 %reflection
404 %specialise [<name list>]
406Misc
407----
409.. _syntax-qualified-names:
411Qualified Names
412~~~~~~~~~~~~~~~
414If multiple declarations with the same name are visible, using the name can
415result in an ambiguous situation. The compiler will attempt to resolve the
416ambiguity using the types involved. If it's unable --- for example, because
417the declarations with the same name also have the same type signatures --- the
418situation can be cleared up using a *qualified name*.
420A qualified name has the symbol's namespace prefixed, separated by a ``.``:
422.. code-block:: idris
424 Data.Vect.length
426This would specifically reference a ``length`` declaration from ``Data.Vect``.
428Qualified names can be written using two different shorthands:
4301. Names in modules that are :ref:`imported <syntax-imports>` using an alias
431 can be qualified by the alias.
4332. The name can be qualified by the *shortest unique suffix* of the
434 namespace in question. For example, the ``length`` case above can likely
435 be shortened to ``Vect.length``.
437.. _syntax-comments:
439Comments
440~~~~~~~~
442::
444 -- Single Line
445 {- Multiline -}
446 ||| Docstring (goes before definition)
448Multi line String literals
449~~~~~~~~~~~~~~~~~~~~~~~~~~
451::
453 foo = """
454 this is a
455 string literal"""
457.. _syntax-directives:
459Directives
460----------
462::
464 %lib <path>
465 %link <path>
466 %flag <path>
467 %include <path>
468 %hide <function>
469 %freeze <name>
470 %access <accessibility>
471 %default <totality>
472 %logging <level 0--11>
473 %dynamic <list of libs>
474 %name <list of names>
475 %error_handlers <list of names>
476 %language <extension>