5Examples are mostly adapted from the Idris tutorial.
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.
21 module MyModule -- module header
23 import Data.Vect -- an import
25 %default total -- a directive
27 foo : Nat -- a declaration
30.. _syntax-module-headers:
35A file can start with a module header, introduced by the ``module`` keyword:
41Module names can be hierarchical, with parts separated by ``.``:
45 module Semantics.Transform
47Each file can define only a single module, which includes everything defined in
50Like with declarations, a :ref:`docstring <syntax-comments>` can be used to
51provide documentation for a module:
55 ||| Implementation of predicate transformer semantics.
56 module Semantics.Transform
63An ``import`` makes the names in another module available for use by the current
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:
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``:
86 import public Data.Vect
93A variable is always defined by defining its type on one line, and its
94value on the next line, using the syntax
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:
122a more interesting example:
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:
137Idris provides two kinds of syntax for defining data types. The first,
138Haskell style syntax, defines a regular algebraic data type. For example
142 data Either a b = Left a | Right b
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``).
157 data Vect : Nat -> Type -> Type where
159 (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
175Equality and Relational
176~~~~~~~~~~~~~~~~~~~~~~~
204 if <test> then <true> else <false>
223Named functions are defined in the same way as variables, with the type
224followed by the definition.
228 <id> : <argument type> -> <return type>
238Functions can also have multiple inputs, for example
242 makeHello : String -> String -> String
243 makeHello first last = "hello, my name is " ++ first ++ " " ++ last
245Functions can also have named arguments. This is required if you want to
246annotate parameters in a docstring. The following shows the same
247``makeHello`` function as above, but with named parameters which are
248also annotated in the docstring
252 ||| Makes a string introducing a person
253 ||| @first The person's first name
254 ||| @last The person's last name
255 makeHello : (first : String) -> (last : String) -> String
256 makeHello first last = "hello, my name is " ++ first ++ " " ++ last
258Like Haskell, Idris functions can be defined by pattern matching. For
263 sum : List Int -> Int
265 sum (x :: xs) = x + (sum xs)
267Similarly case analysis looks like
271 answerString : Bool -> String
272 answerString False = "Wrong answer"
273 answerString True = "Correct answer"
278Dependent functions are functions where the type of the return value
279depends on the input value. In order to define a dependent function,
280named parameters must be used, since the parameter will appear in the
281return type. For example, consider
285 zeros : (n : Nat) -> Vect n Int
287 zeros (S k) = 0 :: (zeros k)
289In this example, the return type is ``Vect n Int`` which is an
290expression which depends on the input parameter ``n``.
295Arguments in anonymous functions are separated by comma.
336 %specialise [<name list>]
341.. _syntax-qualified-names:
346If multiple declarations with the same name are visible, using the name can
347result in an ambiguous situation. The compiler will attempt to resolve the
348ambiguity using the types involved. If it's unable --- for example, because
349the declarations with the same name also have the same type signatures --- the
350situation can be cleared up using a *qualified name*.
352A qualified name has the symbol's namespace prefixed, separated by a ``.``:
358This would specifically reference a ``length`` declaration from ``Data.Vect``.
360Qualified names can be written using two different shorthands:
3621. Names in modules that are :ref:`imported <syntax-imports>` using an alias
363 can be qualified by the alias.
3652. The name can be qualified by the *shortest unique suffix* of the
366 namespace in question. For example, the ``length`` case above can likely
367 be shortened to ``Vect.length``.
378 ||| Docstring (goes before definition)
380Multi line String literals
381~~~~~~~~~~~~~~~~~~~~~~~~~~
389.. _syntax-directives:
402 %access <accessibility>
404 %logging <level 0--11>
405 %dynamic <list of libs>
406 %name <list of names>
407 %error_handlers <list of names>
408 %language <extension>
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list