This is an old revision of the document!
Idris syntax
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
For infix definitions
Here one may use those symbols in combinations
-- :+-*\/=.?|&><!@$%^~#
except to form those predefined ones
-- : => -> <- = ?= | ** ==> \ % ~ ? !