This is an old revision of the document!
Idris syntax
-- TOOD: Use different numbers, some that get larger and larger y : Integer y = 42 --n: save and typecheck k : Integer k = -7 --err k = someword --REPL 2+3 --REPL 1+1 --REPL 1*0 --REPL y --REPL k --REPL 2+y --REPL y * k --REPL k + y * k --REPL -y --REPL x -- not defined --err y : Integer -- extra def --err y = 8 -- extra def --err y = 7 --typecheck correctly and then REPL y --type y=7, typecheck error, and then REPL y, it's gone --'esc' to close info --typecheck correctly and then REPL y --u v : Interger --err n = -103 n : Integer n2 : Integer myFavoriteNumber : Integer some_integer : Integer n3 : Integer --err n3 = 4.5 --comment: --42 is a popular number --comment: --I called this y because I did in the first video --commant: {- this is the first video where we use types -} --comment: {- Setting n3 = 4.5 doesn't work when n3 is an Integer -} m : Integer willNotComeBackTo : Integer --REPL willNotComeBackTo --REPL willNotComeBackTo + 3 n = 22 --REPL n e4hole : Integer e4hole = ?will_complete_in_another_video n' : Integer n' = 33 n_ : Integer n_ = 44 _n : Integer _n = 55 -- err .n : Integer -- err n. : Integer u : Integer u = 2+5 --REPL u --REPL u+1 v : Integer v = n + 10 --err |4 -- just wrting 4 --err |=4 -- just wrting 4 --err |hello -- just wrting hello --err | 4 -- just wrting 4 a : Integer a = 5000000 --REPL a --REPL | = 5000000 b : Integer b = 3000 --REPL b --err |3000 msg : String msg = "Hello" youtube : String youtube = "https://www.youtube.com" --REPL youtube --err msg = 3 faulty : Integer --err faulty = "you know what's gonna happen" --REPL msg --REPL youtube ++ msg youtube_prefix : String youtube_prefix = youtube ++ "/watch?v=" episode2 : String episode2 = youtube_prefix ++ "OGmwGSpwT1U" editor : String editor = "Atom" blank : String blank = " " greeting : String greeting = msg ++ blank ++ editor --REPL "hello" ++ " my friend" --err "hello" + " my friend" --err 2 ++ 3 --err 2 * "dear" s3 : String s3 = "check\nthis\nout" warning : String myword : String --err myword : String --err youword : Strings --err someword : Madeup --REPL String --n String : Type ------ -- Note that there are much more basic types defined. -- We'll also define a lot of our own types. -- Sometimes the REPL will tell us infomration -- involving types we don't know yet. -- Don't worry, we're gonna cover all the basics eventually. -- Some more types beyond Integers, String, for example, -- Bool, Double, Int, Nat, and then also some more complicated types like -- List of Integers, or List of Strings, or List of Booleans. -- And in languages like Haskell or Idris, we also have to do with -- "type variables". This will be discussed soon. ------ f : Integer -> Integer f x = x + 2000 -- REPL f 7 -- REPL z -- REPL f z -- REPL f (f z) zplus : Integer zplus = f z -------- --load in terminal repl --explain 'it' --explain :r --explain :l
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
-- : => -> <- = ?= | ** ==> \ % ~ ? !