Topoi lang draft - (2)

-- comments
--| doc comments (default markdown)
--| prefix | prefixed comments
--[ block comment

]--

--[ prefix |
prefixed block comment
]--

---------------------------------------------
-- as you seen, comments are all start with
-- the `--`
---------------------------------------------


[1, 2, 3] -- list
1 :: 2 :: 3 :: [] -- list desugared

-- Type constructor starts with uppercase letters
Bool

-- Tuple
(Int, Bool)
-- Named Tuple
(i: Int, b: Bool)

-- A named tuple is nothing more than a record. It is basically the same.
{i: Int, b: Bool} -- Tuple index=String val=Type

-- So the unamed tuple? It is index in number
(1: Int, 2: Bool) -- Tuple index=Nat val=Type

sum : (x: Int32) (y: Int32) -> Int32

-- Why don't we use : for the return type of sum function?
-- Because this syntax we can easily recognise a function that returns a function

sumAllPlus100 : (exposed_x: Int32) (exposed_y: Int32) -> Int32
sumAllPlus100 x y = sum 100 (sum x y)

sumAllPlus100 exposed_x=3 exposed_y=4
-- equivalent to
sumAllPlus100 exposed_y=4 exposed_x=3
-- equivalent to
sumAllPlus100 3 4
-- but not
sumAllPlus100 exposed_y=4 3
sumAllPlus100 exposed_x=3 4

-- It is treated as a tuple but can be applied without tuple literal
-- And since there are equivalent, this is the syntax sugar of function application
sumAllPlus100' : (exposed_x: Int32, exposed_y: Int32) -> Int32
sumAllPlus100' (x, y) = sum (100, (sum x y))

----------------------------------------------------------------------------
-- yes it is newline sensitive, and I try to avoid semicolon as mandatory
-- because some of the keyboard layouts are hard to type `;`, if they want
-- to make a term multiline, then use parenthesis.
----------------------------------------------------------------------------

someFunc a b c d e f
-- equivalent to
someFunc (
  a       -- there is no comma here, whitespaces or newline is fine
  b
  c
  d
  e
  f
)


--- 
fact : (n: Int32) -> Int32 = reduce (*) 1 (1..n)
---
-- So the type signature will be...
(n: Int32) -> Int32

an_integer : Int32 = 2
a_boolean = true

-- arrays

-- it is always `[n-ary]type`, so you can make it nested

a : [3][2]Int -- means there is 3 array that contains 2 element of Int
= [[1, 2], [3, 4], [5, 6]]
-- but this is invalid [[1, 2, 3], [4, 5, 6]]

-- random access of data
a : [3][2]i32 = [[1, 2], [3, 4], [5, 6]]
a[1] -- [1, 2]

-- Closures, ad-hoc unnamed function
(x:type)... => body
(x:type)... => { body }
(exposed_name as alias: Type) => { body }

-- Ultimately you can write like this
a : (exposed_name as alias: Type) -> Type => {
  use alias...
}

Package management

from pkg import *
from .pkg import (...)
from ..pkg import (...)