git.iko.soy/Idris-dev
on 88005d8 help sign in
Idris-dev/docs/reference/syntax-guide.rst
284 lines 4.8 kB history raw
1**************
2Syntax Guide
3**************
5Examples are mostly adapted from the Idris tutorial.
7Variables
8---------
10A variable is always defined by defining its type on one line, and its
11value on the next line, using the syntax
13::
15 <id> : <type>
16 <id> = <value>
18Examples
20.. code:: idris
22 x : Int
23 x = 100
24 hello : String
25 hello = "hello"
27Types
28-----
30In Idris, types are first class values. So a type declaration is the
31same as just declaration of a variable whose type is ``Type``. In Idris,
32variables that denote a type must begin with a capital letter. Example:
34.. code:: idris
36 MyIntType : Type
37 MyIntType = Int
39a more interesting example:
41.. code:: idris
43 MyListType : Type
44 MyListType = List Int
46Data types
47~~~~~~~~~~
49Idris provides two kinds of syntax for defining data types. The first,
50Haskell style syntax, defines a regular algebraic data type. For example
52.. code:: idris
54 data Either a b = Left a | Right b
56or
58.. code:: idris
60 data List a = Nil | (::) a (List a)
62The second, more general kind of data type, is defined using Agda or
63GADT style syntax. This syntax defines a data type that is parameterised
64by some values (in the ``Vect`` example, a value of type ``Nat`` and a
65value of type ``Type``).
67.. code:: idris
69 data Vect : Nat -> Type -> Type where
70 Nil : Vect Z a
71 (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
73Operators
74---------
76Arithmetic
77~~~~~~~~~~
79::
81 x + y
82 x - y
83 x * y
84 x / y
85 (x * y) + (a / b)
87Equality and Relational
88~~~~~~~~~~~~~~~~~~~~~~~
90::
92 x == y
93 x /= y
94 x >= y
95 x > y
96 x <= y
97 x < y
99Conditional
100~~~~~~~~~~~
102::
104 x && y
105 x || y
106 not x
108Conditionals
109------------
111If Then Else
112~~~~~~~~~~~~
114::
116 if <test> then <true> else <false>
118Case Expressions
119~~~~~~~~~~~~~~~~
121::
123 case <test> of
124 <case 1> => <expr>
125 <case 2> => <expr>
126 ...
127 otherwise => <expr>
129Functions
130---------
132Named
133~~~~~
135Named functions are defined in the same way as variables, with the type
136followed by the definition.
138::
140 <id> : <argument type> -> <return type>
141 <id> arg = <expr>
143Example
145.. code:: idris
147 plusOne : Int -> Int
148 plusOne x = x + 1
150Functions can also have multiple inputs, for example
152.. code:: idris
154 makeHello : String -> String -> String
155 makeHello first last = "hello, my name is " ++ first ++ " " ++ last
157Functions can also have named arguments. This is required if you want to
158annotate parameters in a docstring. The following shows the same
159``makeHello`` function as above, but with named parameters which are
160also annotated in the docstring
162.. code:: idris
164 ||| Makes a string introducing a person
165 ||| @first The person's first name
166 ||| @last The person's last name
167 makeHello : (first : String) -> (last : String) -> String
168 makeHello first last = "hello, my name is " ++ first ++ " " ++ last
170Like Haskell, Idris functions can be defined by pattern matching. For
171example
173.. code:: idris
175 sum : List Int -> Int
176 sum [] = 0
177 sum (x :: xs) = x + (sum xs)
179Similarly case analysis looks like
181.. code:: idris
183 answerString : Bool -> String
184 answerString False = "Wrong answer"
185 answerString True = "Correct answer"
187Dependent Functions
188~~~~~~~~~~~~~~~~~~~
190Dependent functions are functions where the type of the return value
191depends on the input value. In order to define a dependent function,
192named parameters must be used, since the parameter will appear in the
193return type. For example, consider
195.. code:: idris
197 zeros : (n : Nat) -> Vect n Int
198 zeros Z = []
199 zeros (S k) = 0 :: (zeros k)
201In this example, the return type is ``Vect n Int`` which is an
202expression which depends on the input parameter ``n``. ### Anonymous
203Arguments in anonymous functions are separated by comma.
205::
207 (\x => <expr>)
208 (\x, y => <expr>)
210Modifiers
211~~~~~~~~~
213Visibility
214^^^^^^^^^^
216::
218 public
219 abstract
220 private
222Totality
223^^^^^^^^
225::
227 total
228 implicit
229 partial
230 covering
232Options
233^^^^^^^
235::
237 %export
238 %hint
239 %no_implicit
240 %error_handler
241 %error_reverse
242 %assert_total
243 %reflection
244 %specialise [<name list>]
246Misc
247----
249Comments
250~~~~~~~~
252::
254 -- Single Line
255 {- Multiline -}
256 ||| Docstring (goes before definition)
258Multi line String literals
259~~~~~~~~~~~~~~~~~~~~~~~~~~
261::
263 foo = """
264 this is a
265 string literal"""
267Directives
268----------
270::
272 %lib <path>
273 %link <path>
274 %flag <path>
275 %include <path>
276 %hide <function>
277 %freeze <name>
278 %access <accessibility>
279 %default <totality>
280 %logging <level 0--11>
281 %dynamic <list of libs>
282 %name <list of names>
283 %error_handlers <list of names>
284 %language <extension>