===== Idris syntax =====
| [[Idris]] $\blacktriangleright$ Idris syntax $\blacktriangleright$ [[...]] |
==== Note ====
I'll try to take all the primitive notions and write down one example with them, respectively.

This list largely overlaps with [[Haskell]].

== Defining types ==
<code/Haskell>
data Beagle	 = Bigtime | Burger | Bouncer | Baggy | Bankjob | Bugle | Babyface
data Kid   	 = Tick | Trick | Track
data Parent 	 = Donald | Dasy
data Grandparent = Dagobert

data Singleton   = Point
</code>

== Prelude types ==
<code/Haskell>
my_number : Int 
my_number = 7
my_string : String
my_string = "a string"
my_char : Char
my_char = 'a'
my_bool : Bool
my_bool = False
</code>

== Defining functions, explicitly ==
<code/Haskell>
favorite_parent : Kid -> Parent
favorite_parent Trick = Dasy
favorite_parent k     = Donald -- k is any term of the Kid type

toPoint : Int -> Singleton
toPoint n = Point

toPointLambda : Int -> Singleton
toPointLambda = \n => Point

kid_identity : Kid -> Kid
identity k = k
</code>

== Defining types 2, inductively by defining functions ==
<code/Haskell>
data Nat_    = Z_ | S_ Nat_ 
-- Z_ : Nat_
-- S_ : Nat_ -> Nat_

data List_ a = End_ | Cons_ a (List_ a) -- here 'a' may be any type
-- List_ : Type -> Type
-- End_ : List_ a -- '[]' is the empty list
-- Cons_ : a -> List_ a -> List_ a -- '::' is usually used for Cons_
</code>

== Defining functions, patter maching ==
<code/Haskell>
plus : Nat_ -> Nat_ -> Nat_
plus Z_     y = y
plus (S_ k) y = S_ (plus k y) -- uses 'plus' again
</code>

== Defining functions, dependent type ==
<code/Haskell>
mkSingle : (x : Bool) -> natOrList x
mkSingle True = 0
mkSingle False = []

natOrList : Bool -> Type
natOrList True = Nat
natOrList False = List Nat
</code>

>todo: check this

<code/Haskell>
identity : (t : Type) -> t -> t
identity t = \x => x
</code>

== Prelude functions ==
>todo:
>=>
<code/Haskell>
(==) : Eq ty => ty -> ty -> Bool
(*)  : Num ty => ty -> ty -> ty
(+)  : Num ty => ty -> ty -> ty
</code>

== type, where ==
<code/Haskell>
data Vect : Nat -> Type -> Type where
   Nil  : Vect Z a
   (::) : a -> Vect k a -> Vect (S k) a
</code>

== functions, where ==
<code/Haskell>
reverse : List a -> List a
reverse xs = revAcc [] xs where
  revAcc : List a -> List a -> List a -- Indentation is significant here
  revAcc acc [] = acc
  revAcc acc (x :: xs) = revAcc (x :: acc) xs
</code>

== case ==
<code/Haskell>
case_fun : Int -> Int
case_fun x = case isLT of
            Yes => x + 100
            No  => x + 10
    where
       data MyLT = Yes | No
       isLT : MyLT
       isLT = if x < 20 then Yes else No
</code>

== if ==
<code/Haskell>
AorB : Bool -> String
AorB b = if b then "A" else "B" -- if-construction
</code>


== For infix definitions ==
Here one may use those symbols in combinations
<code/Haskell>
-- :+-*\/=.?|&><!@$%^~#
</code>
except to form those predefined ones
<code/Haskell>
-- : => -> <- = ?= | ** ==> \ % ~ ? !
</code>



=== Discussion ===
=== Reference ===

-----
=== Related ===
[[Haskell]],
[[Haskell type system]]

=== Requirements ===
[[Idris]]