3 Glow Reference Manual

3.1 Basic Syntax

3.1.1 The #lang glow line

Any program that you write in Glow starts with the mandatory line:

#lang glow

3.1.2 Commenting your code

To comment your code in Glow, // creates a line comment and /* and */ create a block comment, just like in ReScript and JavaScript:

// This is a line comment

/* This is a block comment */

3.1.3 Naming objects in Glow

A variable name is made one or more of the characters [_a-zA-Z0-9!$] but must start with an alphabetic character.

Moreover, the variable _ is reserved to denote a pattern that matches anything but whose value is ignored. A few other names are reserved, notably for the keywords of the language or a few languages that might be problematic.

There are terms that can’t be used to name objects, as they are already used as Keywords by either Glow or other languages that interact with it:

abstract arguments assert! boolean break byte case catch class char const continue data debugger default delete deposit! do double else enum eval export extends false final finally float for function goto if implements import in instanceof int interface let long native new null package private protected public publicly! publish! rec require require! return short static sum super switch synchronized this throw throws transient true try type typeof var verifiably! verify! void volatile while with yield withdraw!

Capitalization is conventionally used for types, constructors and constants, while regular variables conventionally start with lower-case letter and are in "CamelCase". This convention isn’t enforced by the language.

3.2 Definitions

3.2.1 Value Definitions

let name = expr;

Defines name and assigns it the value of expr.

Example:

let c = 299792458;

The name is only defined for the scope after the let statement, so the expr cannot refer to name recursively. If there is a previous name, the let statement shadows it for statements after it, but the expr will only refer to the previous one.

Example:

let x = 1;

let x = x + 1;

The x in the x + 1 refers to the first let statement defining it as 1, and so second let statement defines x as 2.

3.2.2 Function Definitions

let name = (params) => expr;

Defines name as a function that takes the params as input and produces the body expr as output.

Example:

let avg = (a, b) => (a + b) / 2;

The name is only defined for the scope after the let statement, so the body expr cannot refer to name recursively.

In the future there will be an option for let rec to allow recursion, as described in Near-Future Plans.

3.2.3 Interaction Definitions

@interaction([participants]) let name = (params) => expr;

Defines name as an interaction function that takes the participants and params as input and produces the body expr as output.

Example:

@interaction([A, B])

let publishHello = () => {

@A let ha = "Hello, B, I am A. How do you do?";

publish! A -> ha;

@B let hb = "Hello, A. I am B. How do YOU do?";

publish! B -> hb;

};

The name is only defined for the scope after the let statement, so the body expr cannot refer to name recursively.

3.2.4 Statement-Block Expressions

{ body }

A statement-block expression can have either a sequence of statements in the body, or statements followed by a final expression, separated by ; semicolons.

Statement-blocks are often used in function definitions after =>, for function bodies:

let name = (params) => { body };

Example:

let avg = (a, b) => {

(a + b) / 2

};

Since statement-blocks are not the only expressions that use curly-braces, empty records written as {} override possible empty statement-blocks, so if you want an empty function body to do "nothing", use () instead of {}.

3.3 Interaction Effects

The Interaction Effects in this section are only valid within interactions, or within the body of an @interaction statement.

publish! participant -> names;

For the given participant, makes them the active participant and sends a message with the values of all the given names to the consensus.

For all other participants, it receives the message and defines the names with the values from the message.

For example in an interaction between A and B, publish! A -> x; makes A the active participant, has A publish x to the consensus, and has B receive x from the consensus.

deposit! participant -> amount;

For the given participant, makes them the active participant and deposits the given amount of their assets to the consensus.

For all other participants, it checks that the next message to the consensus includes this deposit.

For example in an interaction between A and B, deposit! A -> 1; makes A the active participant, has A deposit 1 unit of their assets to the consensus, and has B check that the message included that deposit.

withdraw! participant <- amount;

Withdraws the given amount of assets from the consensus and transfers it to the given participant. This does not have to be the active participant, it can be any participant in the interaction.

For example in an interaction between A and B, withdraw! A <- 1; withdraw! B <- 2; withdraws a combined 3 units of assets from the consensus and transfers 1 to A and 2 to B without changing the active participant.

@publicly!(participant) let name = expr;

Defines name from the given participant’s evaluation of expr, in a way that can be published and verified on the consensus.

Equivalent to:

@verifiably!(participant) let name = expr;

publish! participant -> name;

verify! name;

@verifiably!(participant) let name = expr;

Defines name privately for the given participant from their evaluation of expr. The name remains associated with the expr by an equation that can be verified later on the consensus with verify! once the name and its dependencies in expr have all been published.

verify! names;

Verifies the equation associated with each name in names. Each equation is determined by the previous @verifiably! statement defining name. Each name and its dependencies must all be published beforehand, and the equations must hold.

require! expr;

Checks at runtime a predicate holds and if not fails the active user’s transaction. The predicate must be computable at runtime by all the parties using their common knowledge, so that the contract may verify it. If some of the data comes from user input, it is the user’s responsibility to provide data satisfying the predicate in a timely fashion. Informally, require! means "if this fails, the active user is at fault".

In the future require! will be upgraded to check whether expr is satisfiable, as described in Near-Future Plans.

@participant stmt;

Evaluates the given stmt privately for the given participant.

For example in an interaction between A and B, @A let x = 1; defines x privately to A. Neither B nor the consensus can see x until A publishes it.

3.4 Conditionals

if (a) { b } else { c }

Evaluates a and produces b if a is true, or c if a is false.

switch (val) { cases }

Evaluates val, and pattern-matches it against each case in cases in order. When a pattern in a case matches val, it produces the case body associated with it.

Example:

let status = (code) =>

switch (code) {

| 1 => "Info"

| 2 => "Success"

| 3 => "Redirect"

| 4 => "Client Error"

| 5 => "Server Error"

| _ => "Other"

};

In the future, switch will be upgraded to deal with compound types, as described in Near-Future Plans.

3.5 Datatypes

3.5.1 Booleans and Equality

Bool

The type for booleans, containing the values true and false.

true

The Bool value true, so that if (true) { a } else { b } evaluates a.

false

The Bool value false, so that if (false) { a } else { b } evaluates b.

Both values have to be typed in lowercase.

a == b

The equality operation, produces true if a is equal to b, which must have the same type.

! a

The Bool "not" operation, produces false if a is true, or true if a is false.

! true == false

a && b

The Bool "and" operation, produces true if both a and b are true, or false otherwise. It is short-circuiting, just like in JavaScript: it only evaluates the right-hand-side expression b if a produces to true.

a || b

The Bool "or" operation, produces true if either a or b are true, or false if both are false. It is also short-circuiting just like in JavaScript: it only evaluates the right-hand-side expression b if a evaluates to false.

3.5.2 Integers

Int

The type for integers.

The syntax is for literal integers is just decimal for the moment: just write a non-empty sequence of digits from 0 to 9. For instance, 0, 1, 2, 42, 1729 are values of type Int.

At this moment, Glow only supports the type Nat which contains non-negative natural integers.

Furthermore, as an implementation limitation, when deploying on Ethereum or a similar network, numbers are also restricted to fit in 256 bits (or 32 bytes), the same as the usual type UInt256 of Ethereum. Operations that yield integers greater or equal to 2**256 or less than zero will cause a runtime error.

In the future, Int will allow negative integers and BigInts, as described in Near-Future Plans.

3.5.2.1 Integer Arithmetic

a + b

Produces the Int addition of a plus b.

a - b

Produces the Int subtraction of b from a.

a * b

Produces the Int multiplication of a and b.

a / b

Produces the Int division of a by b.

a % b

Produces the Int remainder of the euclidian division of a by b.

TODO: a ** b for exponentiation

Unlike in Javascript, ++ and -- aren’t in use, because variables and data structure elements cannot be modified. You can only compute new values and new data structures that may somehow shadow the old values and data structures.

Addition and subtraction are not allowed to overflow. An attempt to do so will be detected at runtime, result in an error, and cause the transaction containing the overflow to be aborted, at which point the interaction will remain at its previous state.

For instance, you can’t divide by zero; for the moment, Glow doesn’t support negative numbers; and currently on our Ethereum backend, all numbers must be less than 2**256.

Also note that you can’t perform operations between strings and numbers: you have to explicitly convert values from one type to another.

3.5.2.2 Integer Comparisons

a < b

Produces true when the a is less than b, or false otherwise.

a > b

Produces true when the a is less than b, or false otherwise.

a <= b

Produces true when the a is less than or equal to b, or false otherwise.

a >= b

Produces true when the a is less than or equal to b, or false otherwise.

3.5.2.3 Bitwise Integer Operations

a &&& b

Produces the bitwise-and of a and b.

a ||| b

Produces the bitwise-or of a and b.

a ^^^ b

Produces the bitwise-xor of a and b.

~~~ a

Produces the bitwise-not of a.

a << b

Produces the bitwise-shift-right of a by b.

a >> b

Produces the bitwise-shift-left of a by b.

3.5.3 Byte Strings

Bytes

The type for byte strings made of finite sequences (or arrays) of bytes (integers from 0 to 255 included).

For now, the syntax for byte strings is to write arbitrary ASCII characters between double quotes.

Our syntax is currently limited to ASCII characters, but we will soon add an escape syntax for arbitrary bytes.

Currently available escape sequences are :

• \" for a double-quote (ASCII 34)

• \n for a newline (ASCII 10)

• \\ for a backslash (ASCII 92)

The syntax for a string is a double quote " followed by unescaped ASCII characters or escape sequences.

Unescaped ASCII characters are any character in the ASCII table from space (ASCII 32) to tilde (ASCII 126), except double-quote " (ASCII 34) and backslash (ASCII 92) that must be espaced.

Recognized escape sequences currently include \" to represent the double-quote (ASCII 34) and \\ to represent a backslash (ASCII 92). We will support more escape sequences and an alternate byte-oriented syntax in the near future.

Important note

Note that the choice of characters as non-negative 8-bit bytes, is deliberate: DApps have to deal with digesting exactly well-defined sequences of bytes in consensually executed code that where string validation, like each bit of computation, costs literally millions of times more to execute than code running in private on your local device. In this context, concepts like Unicode, valid codepoints, UTF-8, normalization forms, etc., are extremely expensive nonsense that will rack up immense bills for no benefit whatsoever. Thus, when interfacing between Glow and other languages, make sure that you represent Glow bytestrings as sequences of bytes in your language, and not "native" strings of Unicode or any such dangerously misfit type.

3.5.4 Digests and Signatures

Digest

The type for digests, or hash-values produced by digest.

digest(exprs)

Produces a Digest value representing the hash of the values of the exprs.

Two digests computed from two values should only be equal iff the values are equal.

For example, digest(salt, hand) produces a digest will be the same when computed with the same salt and hand, but different when computed with either different, so a different salt with the same hand produces a different digest, preventing rainbow-table attacks if both the salt and hand are private.

Digests are often used with @verifiably! and verify! to commit to a private choice that can’t be changed later:

@verifiably!(A) let commitment = digest(salt, handA);

publish! A -> commitment;

Then later when they must show their hand it can be published and verified:

publish! A -> salt, handA;

verify! commitment;

Signature

The type for signatures, produced by sign.

sign(digest)

Within a private participant’s evaluation, produces a Signature value confirming that the participant has signed the Digest digest.

isValidSignature(participant, signature, digest)

Produces true if signature comes from the given participant signing the digest with sign(digest), or produces false otherwise.

For a given participant and digest, the expression isValidSignature(participant, sign(digest), digest) always produces true.

3.6 Near-Future Plans

3.6.1 Static Safety Analyses

In the future, Glow will help you prove the safety of your entire applications. We will start by helping you prove safety invariants of your interactions within the execution model of our language, with static analyses that are discharged by a theorem solver.

Eventually, we want to be able to prove entire applications safe, from interface down to hardware, which involves proving every program correct, including compilers and runtimes, and even chips. However, for now, we are focusing on the most pressing issue for decentralized applications, an issue that is not handled by previously existing tools, and that causes millions of dollars every year to be lost to mistakes and frauds: the correctness of the financial interactions between untrusting participants. This involves not just the "contract" on the public blockchain, but also the programs on each participant’s private computer.

3.6.1.1 Specifying Application Invariants

assert! expr;

NOTE: This feature is not supported yet, though it is in the near-future plans.

Will check at compile-time that the predicate alway holds no matter what, as long as this point in the program was reached while the current user and the contract indeed run code generated by the Glow compiler, and the underlying infrastructure runs within the allowed parameters. Informally, assert! means "if this fails, the program won’t even start."

In the future, require! will be upgraded so that the Glow compiler will reject the program unless it can prove that the required assertion is indeed satisfiable for the active user, and generate code that satisfies the assertion.

In the future, assume! will be another kind of assertion. Within an @A it will mean that the active user assumes the given predicate to be true. Outside an @A it will mean that every user assumes the given predicate to be true. Informally, it will mean "you must not run this program unless you know this to be true."

3.6.1.2 Logical Invariants

3.6.1.3 Security properties we will prove about interactions written in Glow

• Non-negativity: Amounts of assets in any account or sub-account are always non-negative.

• Linearity: Assets cannot be created or destroyed or duplicated or divided, only added via explicit deposits, removed via explicit deposits or transfered between accounts.

• Balance: The amount in sub-accounts of an interaction at the end of the interaction is 0.

• Optimality: Within the participants’ respective explicit economic hypotheses, a/the optimal strategy for each participant is to keep executing his program.

• Non-loss: Within the participant’s explicit economic hypotheses, whatever the actions of other participants, each participant’s wallet will keep its value, except for the payment of transaction fees, which is bounded in gas (though the price of gas itself may float up).

• Programmer-defined: The programmer may specify additional application-dependent invariants of his own to the interaction.

The Glow compiler will extract a specification from these invariants, and feed them to a theorem prover. It will reject the program if the theorem prover fails to prove any of these invariants. It will present any counter-examples found by the theorem provers in a way that is legible in terms of execution traces with source-level binding assignments.

3.6.1.4 Correctness of the Glow implementation

In a yet further future, we will want to prove the correctness of the Glow compiler toolchain itself. That will be another endeavour that will require much more capital investment than we can currently afford. Yet we’re confident that our approach will make it much cheaper, more general and more robust than our competitors’ approaches to eventually prove the correctness of an entire toolchain.

3.6.2 Recursive Functions

let rec name = (params) => { body };

NOTE: This feature is not supported yet, though it is in the near-future plans.

Will define name as a recursive function that takes the params as input and produces body as output.

Example:

let rec factorial = (n) => {

if (n == 0) {

0

} else {

n * factorial(n - 1)

}

};

3.6.3 Compound Data Types and Switch Patterns

type Name = Type;

NOTE: This feature is not supported yet, though it is in the near-future plans.

Will define Name as a type alias for the given existing Type.

Example:

type Point2D = (Int, Int);

The Name will only be defined for the scope after the type statement, so the Type cannot refer to Name recursively.

data Name = Variants;

NOTE: This feature is not supported yet, though it is in the near-future plans.

Will define Name as a new algebraic data type with the given Variants.

It will be able to define enumerations:

data Hand = Rock | Paper | Scissors;

Or structures containing values:

data Color = Rgb(Int, Int, Int);

Or enumerations of structures, for example:

data Shape2D = Circle(Point2D, Int)

| Triangle(Point2D, Point2D, Point2D)

| Quadrangle(Point2D, Point2D, Point2D, Point2D);

It is called an algebraic data type because the structures form products of types, while the enumerations form sums, making the new type a sum of products.

The Name will be defined for the scope of the Variants as well as the scope after the data statement, so the Variants can refer to Name recursively.

In the future, switch will be upgraded to deal with compound types including constructors from data types, for example:

type Point2D = (Int, Int);

data Shape2D = Circle(Point2D, Int)

| Triangle(Point2D, Point2D, Point2D)

| Quadrangle(Point2D, Point2D, Point2D, Point2D);

let center = (shape) =>

switch (shape) {

| Circle(c, r) => c

| Triangle((x1,y1), (x2,y2), (x3,y3)) =>

((x1 + x2 + x3)/3, (y1 + y2 + y3)/3)

| Quadrangle((x1,y1), (x2,y2), (x3,y3), (x4,y4)) =>

((x1 + x2 + x3 + x4)/4, (y1 + y2 + y3 + y4)/4)

};

3.6.4 Integers with Negatives and BigInts

In the future, the Int type will allow negative integers, and it will not be limited in size as it is now: it will allow BigInts in JavaScript parlance (or bignums as called in the Lisp tradition).

Nevertheless integer literals in Glow do not and will not take a final n at the end like they do in JavaScript.

Also, we will support a richer set of integer types in the near future, and will add hexadecimal syntax.

3.6.5 Unit and Tuple Types

(Types)

NOTE: This feature is not supported yet, though it is in the near-future plans.

Creates a tuple type, a simple cartesian product of the given types. They contain as elements "tuples", each made of one element of each of the types in the product, in order. There can be any natural number of types in a tuple type. () is an empty tuple, (A, B) is a pair, (A, B, C) is a triple, and so on.

For example, the type (Bool, Nat, Bytes) contains such elements as (true, 4, "hello") and (false, 42, "world").

Do note that (A,B,C) is different from both (A,(B,C)) and ((A,B),C): these types are syntactically different and semantically disjoint; just in a sense they are "isomorphic" since you can write a reversible pair of functions that take one into the other and vice versa.

Unit

NOTE: This feature is not supported yet, though it is in the near-future plans.

Another name for the empty tuple type (), contains the single value ().

(exprs)

NOTE: This feature is not supported yet, though it is in the near-future plans.

Will create a tuple as an expression. () is an empty tuple, (a, b) is a pair, (a, b, c) is a triple, and so on.

3.6.6 Record Types

{ TypeEntries }

NOTE: This feature is not supported yet, though it is in the near-future plans.

Creates a record type. { x: A, y: B, z: C } is a record type with fields x, y, and z, where the types of the fields are A, B, and C respectively.

The order of the fields does not matter for record types.

For the syntax see the Glow Language Grammar.

{ expr_entries }

NOTE: This feature is not supported yet, though it is in the near-future plans.

Will create a record as an expression. { x: a, y: b, z: c } creates a record with fields x, y, and z, where the values of the fields are a, b, and c respectively.

The order of the fields determines evaluation order, but once evaluated, the field order doesn’t matter for the value itself. { x: a, y: b } == { y: b, x: a }.

Empty records written as {} override possible empty statement-blocks written with curly-braces, so if you want an empty function body to do "nothing", use () instead of {}.

For the syntax see the Glow Language Grammar.

3.7 Glow Language Grammar

This surface syntax is inspired by ReScript, Javascript, and Haskell. Most forms based on ReScript. However, @ attributes are based on Javascript, and datatype definitions based on a combination of ReScript and Haskell.

The semantics corresponding to these forms will be most similar to ReScript.