Foreword

This document is intended as a reference manual for the Topoi language. It lists the language constructs, and gives their precise syntax and informal semantics. It is by no means a tutorial introduction to the language.

In future we will make a proper landing page for the language. But right now it serves as our internal team's draft.

Notations

The syntax of the languages is given in BNF-like notation.

Where square brackets [...] denote optional components, curly brackets {...} denotes zero, one or several repetitions of the encolesd components.

Curly brackets with a trailing asterisk sign {...}* denote one or several repetitions of the encolosed components.

Parentheses (...) denote grouping of components.

Identifier and Keywords

identifier           
  = letter (letter | "_" | "'" )* 
  | "_" identifier

qualified_identifier 
  = (identifier ".")+

When referencing something inside a module or a record, or a tuple, we use a qualified name (qualified_identifier).

Comment and Documentation

prefix                 
  = letter (letter | "_" | "'" )* 
  | "_" prefix

comment
  = "--" (char)* newline

doc_comment 
  = "--|" (char)* newline

prefixed_doc_comment
  = "--|" prefix "|" (char)* newline

block_comment 
  = "--[" (char)* "]--"

prefixed_block_comment 
  = "--[" prefix "|" (char)* "]--" 

Content enclosed in documentation comment (doc_comment) and prefixed block comment (prefixed_block_comment) are conversed in AST and will be output or generated as web content.

The prefix is just a name that will let compiler pass to know what generator used to process the content inside the doc comment or block comment. eg.: LaTex, KaTeX, markdown...

Primitive value and types

Full Grammar

program 
  = {definition}+

definition 
  = constant_definition
  | type_definition

constant_definition
  = assignable [":" type] ":=" expression

assignable
  = identifier
  | destructurable

destructurable
  = "(" 
    {identifier [":" type] ["as" assignable]","}* 
    ["..." identifier] 
  ")"

expression
  = function_abstraction
  | function_application
  | identifier
  | record
  | adt_construction

function_abstraction
  = "{" {assignable "->" expression ","}+ "}"

function_application
  = expression "." expression

record
  = "(" {record_body ","}*")"

record_body
  = identifier [":" type] [":=" expression]
  | spread_expression

spread_expression
  = "..." expression

type
  = identifier
  | function_type
  | record_type
  | type_function_application

type_function_application
  = function_application

function_type
  = record_type "->" (record_type|function_type)

record_type
  = "(" {identifier [":" type]}* ")"

type_definition
  =  "type" identifier [":" type ":=" type_body]

type_body
  = {"|" constructor [record_type] ":" type}+

constructor
  = identifier

Expressions

Record

Record expression are key-value pairs. Each record are enclosed by round brackets.

Record Construction

Empty record is denoted as ().

Examples of non-empty records:

(name := "topoi", age := "12")

Each property of a record can so be optionally typed, to ensure that the property will be initiated with the correct type.

(name : String = "topoi", age := "0")

We can also construct nested record:

(
  name := "topoi", 
  friend := (
    name := "haskell", 
    age := "30"
  )
)

Shorthand construction

Suppose we have two variables x and y, to create a record like (x := x, y := y), we can instead write as (x, y). This feature can prevent property mismatch like (x := y, y := y).

Record Type

The type of each record can be inferred by the Topoi type system, for example (name := "topoi", age := "12") has the type of (name: String, age: String)

Record destructuring

The property of each record can be destructured, and be populated in the current environment.

(name, age) := (name := "topoi", age := "0")
-- `name` and `age` will be exposed to the current environment as named variables

Note that not all of the properties need to be destructured.

(name) := (name := "topoi", age := "0")

Also, the destructuring order does not matter:

(age, name) := (name := "topoi", age := "0")

Besides that, we can also re-alias the property name using they keyword as.

(name as myName, age) = (name := "topoi", age := 1)
-- `myName` and `age` is exposed, but `name` is not

Accessing properties

We can do it by using the dot notation.

record.propertyName

For example:

me := (name := "john", age := 2)

myName = me.name

Mutating properties

In Topoi, properties mutation is not allowed, however we can use the spread notation with the triple dot operator.

For example,

me := (name := "john", age := 2)

newMe := (...me, age := 3)

Basically it's the same as JavaScript spread operation.

We can also combine the properties of multiple records into one as such:

me := (name := "john", age := 2)
otherDetail := （address := "sea")

fullMe = (...me, ...otherDetail)

Function

Constructing function

We can construct an unnamed function using the {arguments -> body} notation.

However, note that the function arguments must be of record type, and the return type must also be record type or function type.

For example:

add := {
  (value: Int, by: Int) -> (
    result := 0
  )
}

Function type

Each function has a type, for example, the add function above has the type of:

(value: Int, by: Int) -> (result: Int)

Because of that, we can also define the add function as such:

add 
  : (value: Int, by: Int) -> (result: Int)
  = {
    (value, by) -> (result := 0)
  }

Using function

In Topoi, we can use (a.k.a. apply) a function using the following notation (note that this is the only allowed notation):

arg1.func(arg2 := value1, arg3 := value2, ...)

Note that the first argument can ignore the property name, and the order is not important.

For example, the following function usage are equivalent:

1.add(by := 2)
2.add(value := 1)
(value:=1, by:=2).add

We can also chain function call:

1.add(by:= 2).add(by:= 3) 

Because of the dot notation, we can also directly apply an unnamed function (a.k.a. lambda) to an expression.

(x:=1, y:=2).{
  (x, y) -> x.add(by:=y)
}

Pattern Matching (not finalized)

We can pattern match a value using the equal operator.

For example:

divide : (value: Int, by: Int) -> (result: Result.where(ok:= Int, fail:= String)) := {
  (by = 0) -> Result.fail("Cannot divide by 0"),
  (value, by) -> (
    result := -- something
  )
}

Another example:

type Shape := 
  | Circle (radius: Float)
  | Rectangle (height: Float, width: Float)
  | None

area: (shape: Shape) -> (result: Float) := {
  (shape = Circle(radius)) -> 
    radius.square.multiple(by:= pi),

  (shape = Rectangle(height, width)) ->
    height.multiple(by:= width),

  (shape = None) ->
    0
}