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
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


Requirements

Link to graph
Log In
Improvements of the human condition