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
161The signature of type constructors may use dependent types
165 data DPair : (a : Type) -> (a -> Type) -> Type where
166 MkDPair : {P : a -> Type} -> (x : a) -> (pf : P x) -> DPair a P
171There is a special syntax for data types with one constructor and
181This defines a constructor as well as getter and setter function for
186 MkA : a -> a -> Nat -> A a
188 set_foo : a -> A a -> A a
190The types of record fields may depend on the value of other fields
194 record Collection a where
195 constructor MkCollection
199Setter functions are only provided for fields that do not use dependant
200types. In the example above neither ``set_size`` nor ``set_items`` are
207Inifinite data structures can be introduced with the ``codata``
212 codata Stream : Type -> Type where
213 (::) a -> Stream a -> Stream a
215This is syntactic sugar for the following, which is usually preferred:
219 data Stream : Type -> Type where
220 (::) a -> Inf (Stream a) -> Stream a
222Every occurence of the defined type in a constructor argument will be
223wrapped in the ``Inf`` type constructor. This has the effect of delaying the
224evaluation of the second argument when the data constructor is applied.
225An ``Inf`` argument is constructed using ``Delay`` (which Idris will insert
226implicitly) and evaluated using ``Force`` (again inserted implicitly).
228Furthermore, recursive calls under a ``Delay`` must be guarded by a constructor
229to pass the totality checker.
245Equality and Relational
246~~~~~~~~~~~~~~~~~~~~~~~
274 if <test> then <true> else <false>
293Named functions are defined in the same way as variables, with the type
294followed by the definition.
298 <id> : <argument type> -> <return type>
308Functions can also have multiple inputs, for example
312 makeHello : String -> String -> String
313 makeHello first last = "hello, my name is " ++ first ++ " " ++ last
315Functions can also have named arguments. This is required if you want to
316annotate parameters in a docstring. The following shows the same
317``makeHello`` function as above, but with named parameters which are
318also annotated in the docstring
322 ||| Makes a string introducing a person
323 ||| @first The person's first name
324 ||| @last The person's last name
325 makeHello : (first : String) -> (last : String) -> String
326 makeHello first last = "hello, my name is " ++ first ++ " " ++ last
328Like Haskell, Idris functions can be defined by pattern matching. For
333 sum : List Int -> Int
335 sum (x :: xs) = x + (sum xs)
337Similarly case analysis looks like
341 answerString : Bool -> String
342 answerString False = "Wrong answer"
343 answerString True = "Correct answer"
348Dependent functions are functions where the type of the return value
349depends on the input value. In order to define a dependent function,
350named parameters must be used, since the parameter will appear in the
351return type. For example, consider
355 zeros : (n : Nat) -> Vect n Int
357 zeros (S k) = 0 :: (zeros k)
359In this example, the return type is ``Vect n Int`` which is an
360expression which depends on the input parameter ``n``.
365Arguments in anonymous functions are separated by comma.
393Sets explicitly to which extent pattern matching is terminating and/or
394exhaustive. A ``partial`` pattern matching makes no assumption. A ``covering``
395pattern matching ensures that pattern matching is exhaustive on its clauses.
396Furthermore, a ``total`` pattern matching enforces both exhaustivity and
397termination of the evaluation of its clauses.
417 %specialise [<name list>]
422.. _syntax-qualified-names:
427If multiple declarations with the same name are visible, using the name can
428result in an ambiguous situation. The compiler will attempt to resolve the
429ambiguity using the types involved. If it's unable --- for example, because
430the declarations with the same name also have the same type signatures --- the
431situation can be cleared up using a *qualified name*.
433A qualified name has the symbol's namespace prefixed, separated by a ``.``:
439This would specifically reference a ``length`` declaration from ``Data.Vect``.
441Qualified names can be written using two different shorthands:
4431. Names in modules that are :ref:`imported <syntax-imports>` using an alias
444 can be qualified by the alias.
4462. The name can be qualified by the *shortest unique suffix* of the
447 namespace in question. For example, the ``length`` case above can likely
448 be shortened to ``Vect.length``.
459 ||| Docstring (goes before definition)
461Multi line String literals
462~~~~~~~~~~~~~~~~~~~~~~~~~~
470.. _syntax-directives:
483 %access <accessibility>
485 %logging <level 0--11>
486 %dynamic <list of libs>
487 %name <list of names>
488 %error_handlers <list of names>
489 %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