Content deleted Content added
Tactics via elaborator reflection |
m Task 70: Update syntaxhighlight tags - remove use of deprecated <source> tags |
||
Line 35:
===Functional programming===
The syntax of Idris shows many similarities with that of Haskell. A [[hello world program]] in Idris might look like this:
<
module Main
main : IO ()
main = putStrLn "Hello, World!"
</syntaxhighlight>
The only differences between this program and its [[Haskell (programming language)#Code examples|Haskell equivalent]] are the single (instead of double) colon in the [[type signature]] of the main function, and the omission of the word "where" in the module declaration.<ref>{{cite web|url=https://docs.idris-lang.org/en/v1.3.2/reference/syntax-guide.html|title=Syntax Guide — Idris 1.3.2 documentation|access-date=27 April 2020}}</ref>
Line 47:
Idris supports [[inductively-defined data type]]s and [[parametric polymorphism]]. Such types can be defined both in traditional "[[Haskell 98|Haskell98]]" syntax:
<
data Tree a = Node (Tree a) (Tree a) | Leaf a
</syntaxhighlight>
or in the more general [[Generalized algebraic data type|GADT]] syntax:
<
data Tree : Type -> Type where
Node : Tree a -> Tree a -> Tree a
Leaf : a -> Tree a
</syntaxhighlight>
===Dependent types===
With [[dependent type]]s, it is possible for values to appear in the types; in effect, any value-level computation can be performed during [[typechecking]]. The following defines a type of lists whose lengths are known before the program runs, traditionally called [[Array data structure|vectors]]:
<
data Vect : Nat -> Type -> Type where
Nil : Vect 0 a
(::) : (x : a) -> (xs : Vect n a) -> Vect (n + 1) a
</syntaxhighlight>
This type can be used as follows:
<
total
append : Vect n a -> Vect m a -> Vect (n + m) a
append Nil ys = ys
append (x :: xs) ys = x :: append xs ys
</syntaxhighlight>
The functions append a vector of m elements of type a to a vector of n elements of type a. Since the precise types of the input vectors depend on a value, it is possible to be certain at compile-time that the resulting vector will have exactly (n + m) elements of type a.
Line 82:
Another common example is pairwise addition of two vectors that are parameterized over their length:
<
total
pairAdd : Num a => Vect n a -> Vect n a -> Vect n a
pairAdd Nil Nil = Nil
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys
</syntaxhighlight>
Num a signifies that the type a belongs to the [[type class]] Num. Note that this function still typechecks successfully as total, even though there is no case matching Nil in one vector and a number in the other. Since both vectors are ensured by the type system to have exactly the same length, we can be sure at compile time that this case will not occur. Hence it does not need to be mentioned for the function to be total.
| |||