Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
idris_syntax [2016/05/08 20:48] nikolaj |
idris_syntax [2017/06/06 13:07] nikolaj |
||
---|---|---|---|
Line 1: | Line 1: | ||
===== Idris syntax ===== | ===== Idris syntax ===== | ||
+ | |||
+ | <code> | ||
+ | -- 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 | ||
+ | |||
+ | </code> | ||
+ | |||
| [[Idris]] $\blacktriangleright$ Idris syntax $\blacktriangleright$ [[...]] | | | [[Idris]] $\blacktriangleright$ Idris syntax $\blacktriangleright$ [[...]] | | ||
==== Note ==== | ==== Note ==== | ||
- | I'll try to take all the primitive notions and write down 1 example with them, respectively. | + | I'll try to take all the primitive notions and write down one example with them, respectively. |
This list largely overlaps with [[Haskell]]. | This list largely overlaps with [[Haskell]]. | ||
- | |||
- | > | ||
- | >Todo: | ||
- | > | ||
- | >Draw some neat images (and find some quite place...) | ||
- | > | ||
== Defining types == | == Defining types == | ||
Line 149: | Line 364: | ||
=== Related === | === Related === | ||
[[Haskell]], | [[Haskell]], | ||
- | [[Haskell type system]], | + | [[Haskell type system]] |
- | [[Notes on Idris semantics]] | + | |
=== Requirements === | === Requirements === | ||
[[Idris]] | [[Idris]] |