-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathindex.html
More file actions
310 lines (280 loc) · 10.9 KB
/
index.html
File metadata and controls
310 lines (280 loc) · 10.9 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<meta http-equiv="X-UA-Compatible" content="ie=edge">
<title>Topoi Programming Language</title>
<link rel="stylesheet" type="text/css" href="Inter (Web)/inter.css">
<link rel="stylesheet" type="text/css" href="style.css">
</head>
<body>
<header>
<h1>The Topoi Programming Language</h1>
<div class="flexbox">
<div class="left">
<h2>Reasonable, sound, and friendly. Write terser code.</h2>
<p>A type-safe functional programming language that aims to be terse, small core functionality and simple, featuring dependent type and type inference.</p>
</div>
<div class="right">
<a href="https://github.com/topoi-lang"><button class="btn">View source on GitHub</button></a>
<small>
This project is still WIP implementation of these ideas.
</small>
<small>
If you are interested, please support the project via stars. Thank you for your time and generosity.</small>
</small>
</div>
</div>
</header>
<main>
<!-- content starts here -->
<section id="1-foreword">
<h1 id="foreword">Foreword</h1>
<p>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.</p>
<blockquote>
<p>In future we will make a proper landing page for the language.
But right now it serves as our internal team's draft.</p>
</blockquote>
<h2 id="notations">Notations</h2>
<p>The syntax of the languages is given in BNF-like notation.</p>
<p>Where square brackets <code>[...]</code> denote optional components, curly brackets <code>{...}</code> denotes zero, one or several repetitions of the encolesd components.</p>
<p>Curly brackets with a trailing asterisk sign <code>{...}*</code> denote one or several repetitions of the encolosed components.</p>
<p>Parentheses <code>(...)</code> denote grouping of components.</p>
<table>
<thead>
<tr>
<th>Notation</th>
<th>Repetition</th>
</tr>
</thead>
<tbody>
<tr>
<td><code>{...}?</code></td>
<td>0 or 1</td>
</tr>
<tr>
<td><code>{...}*</code></td>
<td>0 or more</td>
</tr>
<tr>
<td><code>{...}+</code></td>
<td>1 or more</td>
</tr>
</tbody>
</table>
</section>
<section id="2-lexical">
<h2 id="identifier-and-keywords">Identifier and Keywords</h2>
<pre><code>identifier
= letter (letter | "_" | "'" )*
| "_" identifier
qualified_identifier
= (identifier ".")+
</code></pre>
<p>When referencing something inside a module or a record, or a tuple, we use a qualified name (<code>qualified_identifier</code>).</p>
<h3 id="comment-and-documentation">Comment and Documentation</h3>
<pre><code>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)* "]--"
</code></pre>
<p>Content enclosed in documentation comment (<code>doc_comment</code>) and prefixed block comment (<code>prefixed_block_comment</code>) are conversed in AST and will be output or generated as web content.</p>
<p>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...</p>
<h2 id="primitive-value-and-types">Primitive value and types</h2>
<h2 id="full-grammar">Full Grammar</h2>
<pre><code>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
</code></pre>
</section>
<section id="3-record">
<h1 id="expressions">Expressions</h1>
<h2 id="record">Record</h2>
<p>Record expression are key-value pairs.
Each record are enclosed by round brackets.</p>
<h3 id="record-construction">Record Construction</h3>
<p>Empty record is denoted as <code>()</code>.</p>
<p>Examples of non-empty records:</p>
<pre><code class="language-go">(name := "topoi", age := "12")
</code></pre>
<p>Each property of a record can so be optionally typed, to ensure that the property will be initiated with the correct type.</p>
<pre><code class="language-go">(name : String = "topoi", age := "0")
</code></pre>
<p>We can also construct nested record:</p>
<pre><code class="language-go">(
name := "topoi",
friend := (
name := "haskell",
age := "30"
)
)
</code></pre>
<h3 id="shorthand-construction">Shorthand construction</h3>
<p>Suppose we have two variables <code>x</code> and <code>y</code>, to create a record like <code>(x := x, y := y)</code>, we can instead write as <code>(x, y)</code>. This feature can prevent property mismatch like <code>(x := y, y := y)</code>.</p>
<h3 id="record-type">Record Type</h3>
<p>The type of each record can be inferred by the Topoi type system, for example <code>(name := "topoi", age := "12")</code>
has the type of <code>(name: String, age: String)</code></p>
<h3 id="record-destructuring">Record destructuring</h3>
<p>The property of each record can be destructured, and be populated in the current environment.</p>
<pre><code class="language-hs">(name, age) := (name := "topoi", age := "0")
-- `name` and `age` will be exposed to the current environment as named variables
</code></pre>
<p>Note that not all of the properties need to be destructured.</p>
<pre><code class="language-hs">(name) := (name := "topoi", age := "0")
</code></pre>
<p>Also, the destructuring order does not matter:</p>
<pre><code class="language-hs">(age, name) := (name := "topoi", age := "0")
</code></pre>
<p>Besides that, we can also re-alias the property name using they keyword <code>as</code>.</p>
<pre><code class="language-hs">(name as myName, age) = (name := "topoi", age := 1)
-- `myName` and `age` is exposed, but `name` is not
</code></pre>
<h2 id="accessing-properties">Accessing properties</h2>
<p>We can do it by using the dot notation.</p>
<pre><code>record.propertyName
</code></pre>
<p>For example:</p>
<pre><code class="language-hs">me := (name := "john", age := 2)
myName = me.name
</code></pre>
<h2 id="mutating-properties">Mutating properties</h2>
<p>In Topoi, properties mutation is not allowed, however we can use the spread notation with the triple dot operator.</p>
<p>For example,</p>
<pre><code class="language-hs">me := (name := "john", age := 2)
newMe := (...me, age := 3)
</code></pre>
<p>Basically it's the same as JavaScript spread operation.</p>
<p>We can also combine the properties of multiple records into one as such:</p>
<pre><code class="language-sh">me := (name := "john", age := 2)
otherDetail := （address := "sea")
fullMe = (...me, ...otherDetail)
</code></pre>
</section>
<section id="4-function">
<h1 id="function">Function</h1>
<h2 id="constructing-function">Constructing function</h2>
<p>We can construct an unnamed function using the <code>{arguments -> body}</code> notation.</p>
<p>However, note that the function arguments must be of record type, and the return type must also be record type or function type.</p>
<p>For example:</p>
<pre><code class="language-hs">add := {
(value: Int, by: Int) -> (
result := 0
)
}
</code></pre>
<h2 id="function-type">Function type</h2>
<p>Each function has a type, for example, the <code>add</code> function above has the type of:</p>
<pre><code>(value: Int, by: Int) -> (result: Int)
</code></pre>
<p>Because of that, we can also define the <code>add</code> function as such:</p>
<pre><code class="language-hs">add
: (value: Int, by: Int) -> (result: Int)
= {
(value, by) -> (result := 0)
}
</code></pre>
<h2 id="using-function">Using function</h2>
<p>In Topoi, we can use (a.k.a. apply) a function using the following notation (note that this is the only allowed notation):</p>
<pre><code>arg1.func(arg2 := value1, arg3 := value2, ...)
</code></pre>
<p>Note that the first argument can ignore the property name, and the order is not important.</p>
<p>For example, the following function usage are equivalent:</p>
<pre><code>1.add(by := 2)
2.add(value := 1)
(value:=1, by:=2).add
</code></pre>
<p>We can also chain function call:</p>
<pre><code>1.add(by:= 2).add(by:= 3)
</code></pre>
<p>Because of the dot notation, we can also directly apply an unnamed function (a.k.a. lambda) to an expression.</p>
<pre><code>(x:=1, y:=2).{
(x, y) -> x.add(by:=y)
}
</code></pre>
<h2 id="pattern-matching-not-finalized">Pattern Matching (not finalized)</h2>
<p>We can pattern match a value using the <code>equal</code> operator.</p>
<p>For example:</p>
<pre><code class="language-hs">divide : (value: Int, by: Int) -> (result: Result.where(ok:= Int, fail:= String)) := {
(by = 0) -> Result.fail("Cannot divide by 0"),
(value, by) -> (
result := -- something
)
}
</code></pre>
<p>Another example:</p>
<pre><code class="language-hs">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
}
</code></pre>
</section>
<!-- content ends here -->
</main>
</body>
</html>