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
data Beagle	 = Bigtime | Burger | Bouncer | Baggy | Bankjob | Bugle | Babyface
data Kid   	 = Tick | Trick | Track
data Parent 	 = Donald | Dasy
data Grandparent = Dagobert
 
data Singleton   = Point
Prelude types
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
Defining functions, explicitly
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
Defining types 2, inductively by defining functions
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_
Defining functions, patter maching
plus : Nat_ -> Nat_ -> Nat_
plus Z_     y = y
plus (S_ k) y = S_ (plus k y) -- uses 'plus' again
Defining functions, dependent type
mkSingle : (x : Bool) -> natOrList x
mkSingle True = 0
mkSingle False = []
 
natOrList : Bool -> Type
natOrList True = Nat
natOrList False = List Nat
todo: check this
identity : (t : Type) -> t -> t
identity t = \x => x
Prelude functions
todo:
⇒
(==) : Eq ty => ty -> ty -> Bool
(*)  : Num ty => ty -> ty -> ty
(+)  : Num ty => ty -> ty -> ty
type, where
data Vect : Nat -> Type -> Type where
   Nil  : Vect Z a
   (::) : a -> Vect k a -> Vect (S k) a
functions, where
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
case
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
if
AorB : Bool -> String
AorB b = if b then "A" else "B" -- if-construction
For infix definitions

Here one may use those symbols in combinations 

-- :+-*\/=.?|&><!@$%^~#

except to form those predefined ones 

-- : => -> <- = ?= | ** ==> \ % ~ ? !

Discussion

Reference

Haskell, Haskell type system

Requirements

Idris