Topoi Core draft (3)

-- 'Topoi Core' is basically the desugared topoi language.
-- Only consists of basic primitive atoms and functions.

-- This is largely referenced to the ML language, Pie language from the book
-- 'The Little Typer' and (GHC Core)
-- [https://gitlab.haskell.org/ghc/ghc/wikis/commentary/compiler/core-syn-type]


-- write once variable, top level no need to write `let`
n = 3

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

-- Tuple
a = (Int, Bool)
a.0 a.1 -- 0-index

-- Closure
(x) => { ... body }
(x) => { (y) => { ... body } }

-- Type
(x : Type) => { ... body }

-- let...in expression
let ( ... ) in ...


-- Case expressions
-- Case expressions are the most complicated bit of Core, as the GHC Core.
-- * Haskell use this to reach the WHNF of the function
-- * Case tree from Agda
-- * Rose tree from REFAL https://www.wikiwand.com/en/Refal

note: Closure no need so many variants, can be ambiguous.

note: Need to add named argument to this core lanaguage