Processing math: 0%

Idris syntax

Idris 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