Harmony Language Details
Value Types and Operators
Chapter 4 provides an introduction to Harmony values Below is a complete list of Harmony value types with examples:
Type  Name  Example 

Boolean  "bool"  False , True 
Integer  "int"  ..., 2, 1, 0, 1, 2, ... 
String  "str"  " example" , .example 
Program Counter  "pc"  ((method names, lambdas, and labels) 
List  "list"  [ 1, 2, 3, ], ( (1, 2), 3 ), [1,], () 
Dictionary  "dict"  { .account: 12345, .valid: False }, {:} 
Set  "set"  {}, { 1, 2, 3 }, { False , .id, 3 } 
Address  "address"  ?lock, ?flags[2], None 
Context  "context"  (generated by stop or save expression) 
In Harmony, there is no distinction between tuples (denoted with parentheses) and lists (denoted by square brackets). That is, their format is either (e, e, ..., e,) or [e, e, ..., e,]. They map indexes (starting at 0) to Harmony values. If the list has two or more elements, then the final comma is optional.
Method type e
returns the type name of e
.
All Harmony values are ordered with respect to one another. First they
are ordered by type according to the table above. So, for example,
True
\(<\) 0 \(<\) .xyz \(<\) { 0 }. Within types, the following rules
apply:

False
\(<\)True
; 
integers are ordered in the natural way;

strings are lexicographically ordered;

program counters are ordered by their integer values;

lists are lexicographically ordered;

dictionaries are first converted into a list of ordered (key, value) pairs. Then two dictionaries are lexicographically ordered by this representation;

a set is first converted into an ordered list, then lexicographically ordered;

Except for
None
, an address is a pair of a function a list of arguments. Addresses are lexicographically ordered accordingly.None
is the smallest address. 
contexts are ordered deterministically in an unspecified way.
Harmony supports the following comparison operators:
e == e  equivalence 
e != e  inequivalence 
e \(<\) e, e \(<=\) e, e \(>\) e, e \(>=\) e  comparison 
Comparison operators can be chained: x <= y == z
means x <= y and y == z
, although y is evaluated once in the
former and twice in the latter expression.
Harmony supports atomic expression evaluation using the
following syntax: atomically e
, where e
is some expression.
Boolean
The boolean type has only two possible values: False
and True
.
Unlike Python, in Harmony booleans are distinct from integers, and in
particular \(\mathbf{False} < 0\). In statements and expressions where
booleans are expected, it is not possible to substitute values of other
types.
Operations on booleans include:
e and e and ...  conjuction 
e or e or ...  disjunction 
e =\(>\) e, e not =\(>\) e  implication 
not e  negation 
v if e else v'  v or v' depending on e 
any s, all s  disjunction / conjunction for set or list s 
Integer
The integer type supports any whole number. Harmony supports
decimal integers, hexadecimal integers (start with 0x
),
binary integers (start with 0b
), and octal integers (start
with 0o
).
In the Cbased model checker, integers are currently implemented by two's complement 60bit words. The model checker checks for overflow on various operations.
Operations on integers include:
Operation  Description 

e  negation 
abs e  absolute value 
e + e + ...  sum 
e  e  difference 
e * e * ...  product 
e / e, e // e  integer division 
e % e, e mod e  integer division remainder 
e e  power 
~e  binary inversion 
e  e 
e  e 
e ^ e ^ ...  binary exclusive or 
e << e  binary shift left 
e >> e  binary shift right 
{ e..e' }  set of integers from e to e' inclusive 
String
A string is a sequence of zero or more unicode characters. If it
consists entirely of alphanumerical characters or underscore characters
and does not start with a digit, then a string can be represented by a
"." followed by the characters. For example, .example is the same as
the string "
example"
.
Native operations on strings include the following:
Operation  Description 

s k  indexing 
s + s + ...  concatenation 
s * n  n copies of s concatenated 
v [not] in s  check if v is [not] a substring in s 
len s  the length of s 
str e  string representation of any value e 
Set
In Harmony you can create a set of any collection of Harmony values. Its
syntax is { v_0, v_1, ... }
. Python users: note that in Harmony the
empty set is denoted as {}
. (In Python, {}
means the empty dictionary,
which is represented as {:}
in Harmony.)
The set
module contains various convenient routines that operate on
sets. Native operations on sets include:
Operation  Description 

len s  cardinality 
s  s  set difference 
s & s & ...  intersection 
s \(\vert\) s \(\vert\) ...  union 
s \^ s \^ ...  inclusion/exclusion (elements in odd number of sets) 
choose s  select an element (Harmony will try all) 
min s  minimum element 
max s  maximum element 
any s  True if any value is True 
all s  True if all values are True 
In Python, the \(<\) operator on sets represents the subset relation.
However, in Harmony \(<\) is a total order. If you want to check if x
is a subset of y
, either use the subset
method in the set
module
or write something like (x  y) == y
(the union of x
and y
is y
).
Harmony also supports set comprehension. In its simplest form,
{ f(v) for v in s }
returns a set that is constructed by applying f
to all elements in s (where s is a set or a list). This is known as
mapping. But set comprehension is much more powerful and can include
joining multiple sets (using nested for loops) and filtering (using the
where
keyword).
For example: { x + y for x in s for y in s where (x * y) == 4 }
returns a set that is constructed by summing pairs of elements from s
that, when multiplied, have the value 4.
List or Tuple
In Harmony, there is no distinction between a list or a tuple.
You can denote a list by a sequence of values, each value terminated
by a comma. As per usual, you can use brackets or parentheses
at your discretion. For Python users, the important thing to note
is that a singleton list in Harmony must contain a comma. For
example [1,]
is a list containing the value 1
, while [1]
is simply the value 1
.
The list
module contains various
convenient routines that operate on lists or tuples.
Native operations on lists or tuples include the following:
Operation  Description 

t k  indexing 
t + t + ...  concatenation 
t * n  n copies of t concatenated 
v [not] in t  check if v is [not] a value in t 
len t  the length of t 
min t  the minimum value in t 
max t  the maximum value in t 
any t  True if any value is True 
all t  True if all values are True 
Lists and tuples support comprehension.
In its most basic form: [f(v) for v in t]
.
For example, to check if any element in a list t
is even, you
can write: any((x % 2) == 0 for x in t)
.
The domain of a list \(L\) of length \(n\), interpreted as a function, are the
integers \(0..n1\). It is illegal to read \(L[n]\). However, unlike
Python, it is possible to write into \(L[n]\). For example, if
variable x
contains [1, 2]
, then the statement x[2] = 3
results in x
having the value [1, 2, 3]
.
Dictionary
A dictionary maps a set of values (known as keys) to another set of
values. The generic syntax of a dictionary is
\(\{ k_0:v_0, k_1:v_1, ... \}\). Different from Python, the empty
dictionary is written as {:}
(because {} is the empty set in
Harmony). If there are duplicate keys in the list, then only the one
with the maximum value survives. Therefore the order of the keys in the
dictionary does not matter.
Dictionaries support comprehension. The basic form is: {
f
(v):g
(v) for v in s }.
There are various special cases of dictionaries, including lists, tuples, strings, and bags (multisets) that are individually described below.
Operations on dictionaries include the following:
Operation  Description 

d k  indexing 
len d  the number of keys in d 
keys d  the set of keys in d 
k [not] in d  check if k is [not] a value in d 
min d  the minimum value in d 
max d  the maximum value in d 
any d  True if any value is True 
all d  True if all values are True 
d & d & ...  dictionary intersection 
d \(\vert\) d \(\vert\) ...  dictionary union 
Because in Harmony brackets are used for parsing purposes only, you can write d[k] (or d(k)) instead of d k. However, if k is a string like .id, then you might prefer the notation k.id.
Dictionary intersection and dictionary union are defined so that they work well with bags. With disjoint dictionaries, intersection and union work as expected. If there is a key in the intersection, then dictionary intersection retains the minimum value while dictionary union retains the maximum value. Unlike Python, Harmony dictionary intersection and union are commutative and associative.
Bag or Multiset
A bag is represented by a dictionary that maps each element to its
multiplicity. For example: { 10:2, 12:1 }
is the bag containing
two copies of 10 and one copy of 12. The bag
module contains
various convenient routines that operate on bags. Native
operations on bags include the following:
Operation  Description 

v [not] in b  check if v is [not] in b 
t & t & ...  bag intersection 
t \(\vert\) t \(\vert\) ...  bag union 
Program Counter
A program counter is an integer that can be used to index into Harmony bytecode. When you define a method, a lambda function, or a label, you are creating a constant of the program counter type.
Operations on program counters include the following:
Operation  Description 

m a  invoke method with program counter m and argument a 
countLabel l  return the number of threads executing at label l 
You can create lambda functions similarly to Python, except that the expression has to end on the keyword end. For example: lambda(x,y): x+y end.
Address
A Harmony address is a closure consisting of a function
and a list of arguments. A function can be a constant or a variable
and the arguments are all Harmony values. Given an address
p = ?a[b][c]...
, you can use the notation !p
to find its value.
Harmony will first evaluate a
, then apply the result to b
, then
apply the result to c
, and so on.
As a simple example, ?5
is the address of the constant 5, and
therefore !?5
evaluates to 5.
Now consider the following program:
let p = ?5:
assert !p == 5
!p = 5
!p = 4
The only line in this program that fails is the last one, as you are not allowed to store 4 at the address of 5.
a
can be a constant that maps Harmony values to Harmony values:
dictionaries, lists, and strings. In that case, ?a[b]
refers to
the value of entry b
in a
.
The most common use of addresses is when a
is a shared variable.
In that case !?a
evaluates to the current value of a
.
Finally, a
can be a program counter value (method or lambda).
?a(b)
is then the closure of method a
and argument b
.
In this case, !?a(b)
evaluates a(b)
. For example, the
following Harmony program, perhaps surprisingly, does not run into
failing assertions:
counter = 0
def f():
counter += 1
result = counter
let p = ?f():
if !p != 1: assert False
if !p != 2: assert False
if !p != 3: assert False
Internally, Harmony uses the address of a method variable
and sometimes you see them on the stack during a computation.
If k
is a method variable, then its address is output as ?@k
.
However, at the Harmony language level there is no such thing
as the address of a local variable.
Consider the following two programs:


In the program on the left, x
is a shared variable, and ?x
is
the location of variable x
. In the program on the right, x
is a local variable. ?x
evaluates x
and then takes its address,
so in this case ?x
equals ?1
.
Like C, Harmony supports the shorthand p>v
for the expression (!p).v
.
Context
A context value (aka continuation) captures the state of a thread. A context is itself composed over various Harmony values.
The following operations generate contexts:
save e 
returns a Harmony value (see below) 
stop p 
saves context in !p and stops the thread (see below) 
The save e
expression, when invoked, returns a tuple (e, c)
where
c
is the context value of the thread right after the save
instruction
finished.
Using go c r
the context can be turned into a new thread that, instead,
returns r
from the save e
expression. See Figure A.1
for an example of how this could be used to fork a thread into
two threads.
The stop p
expression stores the context of the thread right after
the expression in !p
(i.e., p
must be an address value) and
terminates the thread. The thread can later be reinstantiated with
go !p r
, in which case the stop
expression returns r
.
A thread can be for ever suspended using stop None
or just stop()
.
Statements
Harmony currently supports the following statements (below, S
is a
list of statements and an lvalue is an expression you can use on
the lefthand side of an assignment statement):
Statement  Description 

e  e is an expression 
lv = [lv =]... e  lv is an lvalue and e is an expression 
lv [op]= e  op is one of + ,  , * , / , // , % , & ,  , ^ , and, or 
l: S 
l is a label 
assert b [, e]  b is a boolean. Optionally report value of expression e 
await b  b is a boolean 
const a = e  a is a bound variable, e is a constant expression 
def m a [returns v]: S 
m is an identifier, a a bound variable, and v a variable 
del lv  delete lv 
finally e  e is a boolean expression that must hold in each final state 
for a[:b] in e [where c]: S 
a and b are bound variables, e is a set, dictionary, or string 
from m import ...  m identifies a module 
go c e  c is a context, e is an expression 
if b: S else: S 
b is a boolean, S is a list of statements 
import m, ...  m identifies a module 
invariant e  e is an invariant (must always hold) 
let a = e: S 
a is a bound variable, e is an expression 
pass  do nothing 
print e  e is an expression 
sequential v, ...  v has sequential consistency 
spawn [eternal] m e [, t]  m is a method, e is an expression, t is the threadlocal state 
trap m e  m is a method and e is an expression 
var v = e  v is a new variable, e is an expression 
when b: S 
b is a boolean, S a list of statements 
when exists a in e: S 
a is a bound variable, e is an expression 
while b: S 
b is a boolean, S a list of statements 

Bound variables are readonly.

A statement can be preceded by the atomically keyword to make the statement atomic.

Multiple for statements can be combined into a single statement.

Multiple let and when statements can be combined into a single statement.
Single expression evaluation
Any expression by itself can be used as a statement. The most common
form of this is a function application, for example: f
(). This
statement evaluates f
() but ignores its result. It is equivalent to
the assignment statement \(\_ = \mathtt{f}()\).
Assignment
The statement x = 3 changes the state by assigning 3 to variable x
(assuming x was not already 3). x may be a local variable or a
shared variable. The statement x = y = 3 first updates y,
then x. The statement x[f
()] = y[g
()] = h
() first
computes the address of x[f
()], then computes the address of
y[g
()], then evaluates h
(), then assigns the resulting value to
y[g
()] (using its previously computed address), and finally
assigns the same value to x[f
()] (again using its previously
computed address). The statement a,b = c assumes that c is a
tuple with two values. It first evaluates the addresses of a and b
and first assigns to the latter and then the former. If c is not a
tuple with two values, then Harmony will report an error.
Assigning to _
(underscore) evaluates the righthand side expression
but is otherwise a noop.
The lefthand side can also contain constants.
For example (3, x) = (3, True)
assigns True
to x
.
However, (3, x) = (4, True)
fails.
The statement \(x~+\)\(= 3\) loads x, adds 3, and then stores the results
in x. In this case, it is equivalent to \(x = x + 3\). However, in
general this is not so. For example, x[f
()] += 3 only evaluates
f
() once. Unlike Python, however, x += [3,] is equivalent to x =
x + [3,] in Harmony. (In Python, the following two compound
statements lead to different results for y: x = y = [ ]; x +=
[3] and x = y = [ ]; x = x + [3].)
assert
The statement assert b evaluates b and reports an error if b is false. It should be considered a noopit is part of the specification, not part of the implementation of the algorithm. In particular, it specifies an invariant: whenever the program counter is at the location where the assert statement is, then b is always true.
If b is an expression, then it is evaluated atomically. Moreover, the expression is not allowed to change the state. If it does change the state, Harmony will report an error as well.
As in Python, you can specify an additional expression: assert b, e. The value of e will be reported as part of the error should b evaluate to false.
atomically
A statement can be preceded by the atomically keyword to make the
statement atomic. The statement atomically: S1
; S2
; ...
evaluates statements S1
, S2
, ... atomically. This means that the
statement runs indivisiblyno other thread can interleave in the
atomic statement. The only exception to this is if the atomic block
executes a stop expression. In this case, another thread can run.
When the original thread is resumed (using a go statement), it is
once again atomically executing.
atomically statements are useful for specification and implementing synchronization primitives such as testandset. It is also useful for testing. It is not a replacement for lock/unlock, and should not generally be used for synchronization otherwise. Lock/unlock does allow other threads to run concurrentlyjust not in the same critical section.
await
The statement await b is equivalent to when b: pass. It is intended to improve readability of your code.
const
The expression const N
= 3 introduces a new constant N
with the
value 3. Evaluating N
does not lead to loading from a memory location.
The assignment can be overridden with the c
flag: harmony cN=4
executes the model checker with 4 assigned to N
instead of 3. Harmony
also supports const N
, M
= 3, 4, which assigns 3 to N
and 4 to
M
. Harmony has limited support for constant folding. For example,
const N
= 3 + 4 assigns value 7 to constant N
.
def
The statement def m a [returns v]: S1
; S2
: ... defines a new program
counter constant m referring to a method that takes an argument a
and executes the statements S1
, S2
, .... The argument a can be a
tuple pattern similar to those used in let and for statements.
Examples include (), (x,), (x, y), and (x, (y, z)). The
given local variable names are assigned upon application and are
readonly. Optionally, a result variable r
can be declared. If not declared,
there is (for backwards compatibility), a default result variable
called result
, initialized to None
. Harmony does not support a return
statement that breaks out of the code before executing the last statement.
del
The statement del x removes variable x from the state. x can be either a local or a shared variable. For example, the statement del x.age removes the .age field from dictionary x. Harmony automatically removes toplevel local variables that are no longer in use from the state in order to attempt to reduce the number of states that are evaluated during model checking.
Because Harmony lists are dictionaries, deleting from lists is different
from Python: del
can also be used to remove elements from a list.
x = [.a, .b, .c]; del x[1]
results in x having value [.a, .c]
.
finally
The statement finally c
declares that boolean expression c
must hold in each final state. c
is only allowed to read
shared variables and is evaluated in each final state. If it
evaluates to False
, Harmony reports an error. Harmony also
reports an error if the expression evaluates to a value other
than False
or True
.
for ... in ... [where ...]
The statement for x in y: S1
; S2
; ... iterates over y
and executes for each element the statements S1
, S2
, .... y must
be a set, list, dictionary, or string. y is evaluated only once at the
beginning of the evaluation of this statement. In case of a set, the
result is sorted (using Harmony's global order on all values). In case
of a dictionary, the statement iterates over the keys in order. This makes
iterating over lists intuitive and identical to Python. For each element,
the statements S1
, S2
, ... are executed with local variable y
having the value of the element. x can be a pattern such as \((a)\) or
\((a, (b, c))\). If the pattern cannot be matched, Harmony detects and
error. It is allowed, but discouraged, to assign different values to x
within statements S1
, S2
, ....
Harmony also supports the form for k:v
in y: S1
; S2
; .... This works similar, except that k is
bound to the key and v is bound to the value.
If y is not a dictionary, then k ranges from 0 to
len(y)  1.
The statement also supports nesting and filtering. Nesting is of the
form for x1 in y1 for x2 in y2: S1
; S2
;
..., which is equivalent to the statement for x1 in y1:
for x2 in y2: S1
; S2
; .... Filtering is of the form
for x in y where z: S1
; S2
; .... For example,
for x in 1 .. 10 where (x % 2) == 0: S1
; S2
; ...
only evaluates statements S1
, S2
, ... for even x, that is, 2, 4,
6, 8, and 10.
Harmony does not support break or continue statements.
from ... import
The statement from x import a, b, ... imports module x and makes its constants a, b, ... also constants in the current module. If a module is imported more than once, its code is only included the first time. The constants will typically be the names of methods (program counter constants) within the module.
You can import all constants from a module m (including program
counter constants) using the statement from m import *. This,
however, excludes constants whose names start with the character _
:
those are considered private to the module.
go
def fork():
atomically:
let (r, ctx) = save True:
result = r
if r:
go ctx (False, None)
def main():
if fork():
print "parent"
else:
print "child"
spawn eternal main()
The statement go c e starts a thread with context c that has executed a stop or save expression. The stop or save expression returns value e. The same context can be started multiple times, allowing threads to fork. See Figure A.1 for an example.
if ... [elif ...]* [else]
Harmony supports if statements. In its most basic form, if c:
S1
; S2
; ... evaluates c and executes statements S1
, S2
, ...
if and only if boolean expression c evaluated to true. Harmony checks
that c is either False
or True
if neither is the case, Harmony
reports an error. The statement if c: S1
, S2
, ... else:
T1
; T2
; ... is similar, but executes statements T1
, T2
, ... if
and only if c evaluated to False
. You can think of elif \(c:\) as
shorthand for else: if c:.
import
The statement import m1, m2, ... imports modules m1, m2,
... in that order. If a module is imported more than once, its code is
only included the first time. The constants (including method constants)
and shared variables declared in that module can subsequently be
referenced by prepending "m.". For example, method f
() in imported
module m is invoked by calling m.f
(). If you would prefer to
invoke it simply as f
(), then you have to import using the statement
from m import f
.
invariant
The statement invariant c declares that boolean expression c is
an invariant. c is only allowed to read shared variables and is
evaluated atomically after every state change. If it ever evaluates to
False
Harmony reports and error. Harmony also reports an error if the
expression evaluates to a value other than False
or True
.
The predicate has access to two immutable variables called
pre
and post
. post
is a name for the current shared state,
and thus post.x == x
for any shared variable x
. pre
is
a name for the prior shared state in a state change. For example,
invariant pre.p => post.p
(or equivalently invariant pre.p = p
)
states that p
is a stable predicate: once true, it is always true.
invariant pre.x <= x
states that variable x
grows monotonically.
Harmony (like TLA+) requires that such invariants are "invariant under
stuttering", which means that for any predicate \(P\) and any reachable
state \(S\) the following must hold: (pre
= \(S\) = post
)
\(\Rightarrow P\). Less formally, \(P\) must hold in a state change that
does not affect the variables that \(P\) accesses. For example, the
following invariant would be problematic: invariant pre.x < x
,
which states that \(x\) grows strictly monotonically no matter what
state changes. This is problematic because it would not hold in a
state change that, say, changes \(y\) but leaves \(x\) untouched.
Invariants can be useful to specify the type of a global variable.
For example, you can write invariant (type(x) == "int") and ((x % 2) == 0)
to state that x
is an even integer variable.
let
You can introduce new bound variables in a method using the let
statement. The statement let a = b: S1
; S2
, ... evaluates
b, assigns the result to readonly variable a, and evaluates
statements S1
, S2
, .... let supports pattern matching, so you
can write let x, (y, z) = b: S1
; S2
, .... This will
only work if b is a tuple with two elements, the second of which also
being a tuple with two elementsif not, Harmony will report an error.
let statements may be nested, such as let a1 = b1 let
a2 = b2: S1
; S2
; .... Doing so can improve readability by
reducing indentation compared to writing them as separate statements.
Compare the following two examples:
let a = y:
let b = z:
...
let a = y
let b = z:
pass
The pass statement does nothing.
The statement print e evaluates e and adds the result to the print log. The print log is used to create an "external behavior DFA" for the Harmony program.
sequential
In Harmony, shared variable Load
and Store
operations are atomic and
have sequential consistency. However, Harmony does check for data
races. A data race occurs when two or more threads simultaneously
access the same shared variable, with at least one of the accesses being
a Store
operation outside of an atomic block. If so, Harmony will
report an error. This error can be suppressed by declaring the shared
variable as sequential. In particular, the statement sequential x,
y, ... specifies that the algorithm assumes that the given variables
have sequential consistency.
Note that few modern processors support sequentially consistent memory by default, as doing so would lead to high overhead.
spawn
The statement spawn m a starts a new thread that executes method m with argument a. m must be a program counter constant, and a is typically a tuple containing zero or more parameters to be passed to the method.
The default threadlocal state of the thread, called self, is the empty dictionary by default. It can be specified by adding a parameter: spawn m a, e specifies that e should be the initial value of the threadlocal state.
Harmony normally checks that all threads eventually terminate. If a thread may never terminate, you should spawn it with spawn eternal m a to suppress those checks.
trap
The statement trap m a specifies that the current thread should
execute method m with argument a and some future, unspecified, time.
It models a timer interrupt or any kind of asynchronous event to be
handled by the thread. Such interrupts can be disabled by setting the
interrupt level of the thread to True
using the setintlevel
operator.
var
You can introduce new local variables in a method using the var statement. The statement var a = b evaluates b and assigns the result to local variable a. var supports pattern matching, so you can write var x, (y, z) = b. This will only work if b is a tuple with two elements, the second of which also being a tuple with two elementsif not, Harmony will report an error.
when
The statement when c: S1
; S2
; ... executes statements S1
,
S2
, ... after waiting until c evaluates to True
. when
statements are most useful when combined with the atomically
keyword. If waiting is an unused local variable, then atomically
when c: S1
; S2
; ... is equivalent to
var waiting = True
while waiting:
atomically:
if c:
S1
S2
...
waiting = False
Multiple let and when statements can be combined. The expressions before the colon are reevaluated repeated until all when conditions are satisfied.
when exists ... in ...
The statement when exists x in y: S1
; S2
; ...
requires that y evaluates to a set value. The statement does the
following three things:

it waits until y is nonempty;

it selects one element of y nondeterministically (using a choose expression);

it executes statements
S1
,S2
, ... with the selected element bound to readonly variable x.
x may be a pattern, like in let, for, and def statements. Harmony reports an error if y evaluates to a value that is not a set.
when statements are most useful when combined with the
atomically keyword. If waiting is an unused local variable, then
atomically when exists x in y: S1
; S2
; ... is
equivalent to
var waiting = True:
while waiting:
atomically:
if y != {}:
let x = choose(y):
S1
S2
...
waiting = False
The statement is particularly useful in programming network protocols when having to wait for one or more messages and executing a set of actions atomically after the desired messages have arrived.
while
The statement while c: S1
; S2
; ... executes statements S1
,
S2
, ... repeatedly as long as c evaluates to True
. Harmony does
not support break or continue statements.
Harmony is not objectoriented
Python is objectoriented, but Harmony is not. For Python programmers, this can lead to some unexpected differences. For example, consider the following code:
x = y = [ 1, 2 ]
x[0] = 3
assert y[0] == 1
In Python, lists are objects. Thus x and y point to the same list, and the assertion would fail if executed by Python. In Harmony, lists are values. So, when x is updated in Line 2, it does not affect the value of y. The assertion succeeds. Harmony supports references to values (Chapter 7), allowing programs to implement shared objects.
Because Harmony does not have objects, it also does not have object
methods. However, Harmony methods and lambdas are program counter
constants. These constants can be added to dictionaries. For example, in
Figure 7.1 you can add the P_enter
and P_exit
methods
to the P_mutex
dictionary like so:
{ .turn: 0, .flags: [ False, False ], .enter: P_enter, .exit: P_exit }
That would allow you to simulate object methods.
There are at least two reasons why Harmony is not objectoriented. First, objectorientation often adds layers of indirection that would make it harder to model check and also to interpret the results. Consider, for example, a lock. In Python, a lock is an object. A lock variable would contain a reference to a lock object. In Harmony, a lock variable contains the value of the lock itself. Thus, the following statement means something quite different in Python and Harmony:
x = y = Lock()
In Python, this creates two variables x and y referring to the same lock. In Harmony, the two variables will be two different locks. If you want two variables referring to the same lock in Harmony, you might write:
lock = Lock()
x = y = ?lock
or, using the alloc
module,
from alloc import malloc
x = y = malloc(Lock())
The second reason for Harmony not being objectoriented is that many
concurrency solutions in the literature are expressed in C or some other
lowlevel language that does not support objectorientation, but instead
use malloc
and free
.
Constants, Global and Local Variables
Each (nonreserved) identifier in a Harmony program refers to either a global constant, a global shared variable, a local bound variable, a local mutable variable, or a module. Constants are declared using const statements. Those constants are evaluated at compiletime.
Mutable method variables can be declared using the returns
clause of
a def
statement or using var
. Bound variables, which are immutable,
can be declared in def statements (i.e., arguments), let statements,
for loops, and when exists
statements. Mutable variables can be
declared with the var statement. Also, each method has an implicitly
declared result variable, which is initialized to None
. Each thread
has a mutable variable called this that contains the threadlocal state.
Method variables are tightly scoped and cannot be shared between threads.
While in theory one method can be declared within another, they cannot share
local variables either. All other variables are global and must be
initialized before spawned threads are start executing.
Operator Precedence
In Harmony, there is no syntactic difference between applying an argument to a function or an index to a dictionary. Both use the syntax a b c .... We call this application, and application is leftassociative. So, a b c is interpreted as (a b) c: b is applied to a, and then c is applied to the result. For readability, it may help to write \(a(b)\) for function application and \(a[b]\) for indexing. In case b is a simple string, you can also write \(a.b\) for indexing.
There are three levels of precedence. Application has the highest precedence. So, !a b is interpreted as !(a b) and a b + c d is interpreted as (a b) + (c d). Unary operators have the next highest precedence, and the remaining operators have the lowest precedence. For example, \(2 + 3\) evaluates to 1, not \(5\).
Associative operators (\(+\), \(*\), \(\), \(\string&\), \(\string^\), and, or) are interpreted as general \(n\)ary operators, and you are allowed to write \(a + b + c\). However, ambiguous expressions such as \(a  b  c\) are illegal, as is any combination of operators with an arity larger than one, such as \(a + b < c\). In such cases you have to add parentheses or brackets to indicate what the intended evaluation order is, such as \((a + b) < c\).
In almost all expressions, subexpressions are evaluated left to right.
So, a[b] + c first evaluates a, then b (and then applies b
to a), and then c. The one exception is the expression a if
c else b, where c is evaluated first. In that expression, only
a or b is evaluated depending on the value of c. In the expression
a and b and \(...\), evaluation is left to right but stops
once one of the subexpressions evaluates to False
. Similarly for
or, where evaluation stops once one of the subexpressions evaluates
to True
. A sequence of comparison operations, such as \(a < b < c\), is
evaluated left to right but stops as soon as one of the comparisons
fails.
As an aside: the expression a not in b is equivalent to
not (a in b). Harmony generalizes this construct for any
pair of a unary (except '\(\)') and a binary operator. In particular, a
not and b is the same as not (a and b). For those
familiar with logic gates, not and is the equivalent of NAND
.
Similarly, not =\(>\) is nonimplication.
Tuples, Lists, and Pattern Matching
Harmony tuples and lists are equivalent.
They can be bracketed either by '(' and ')' or by '[' and
']', but the brackets are often optional. Importantly, with a singleton
list, the one element must be followed by a comma. For example, the
statement x = 1,;
assigns a singleton tuple (or list) to x.
Harmony does not support special slicing syntax like Python. To
modify lists, use the subseq
method in the list
module.
Harmony allows pattern matching against nested tuples in various language constructs. The following are the same in Python and Harmony:

x, = 1,: assigns 1 to x;

x, y = 1, (2, 3): assigns 1 to x and (2, 3) to y;

x, (y, z) = 1, (2, 3): assigns 1 to x, 2 to y, and 3 to \(z\);

x, (y, z) = 1, 2: generates an runtime error because 2 cannot be matched with (y, z);

x[0], x[1] = x[1], x[0]: swaps the first two elements of list x.
As in Python, pattern matching can also be used in for statements. For example:
for key, value in [ (1, 2), (3, 4) ]: ...
Harmony (but not Python) also allows pattern matching in defining and invoking methods. For example, you can write:
def f
[a, (b, c)]: ...
and then call f
[1, (2, 3)]. Note that the more familiar: def
g
(a) defines a method g
with a single argument a. Invoking
g
(1, 2) would assign the tuple (1, 2) to a. This is not consistent
with Python syntax. For single argument methods, you may want to declare
as follows: def g(\(a,\)). Calling g(1,) assigns 1 to a, while
calling g(1, 2) would result in a runtime error as (1, 2) cannot be
matched with (a,).
Pattern matching can also be used in const, let, and when exists statements.
### For Loops and Comprehensions While Harmony does not support general iterators such as Python does, Harmony allows iterating over sets, lists, and dictionaries. When iterating over a set, the set is always traversed in order (see Language Details for how Harmony values are ordered). When iterating over a dictionary, it is always traversed in the order of the keys.
Harmony supports nesting and filtering in for loops.
For example:
In case of dictionaries, you can access both keys and values (not supported in Python):for i in { 1..10 } for j in { 1..10 } where i < j: ...
Harmony also supports set, list, and dictionary comprehensions. Comprehensions are similar to Python, except that filtering uses the keywordfor k:v in .a: 1, .b: 2: ...
where
instead ofif
.
Dynamic Allocation
Harmony supports various options for dynamic allocation. By way of example, consider a stack. Figure A.2 presents a test program for a stack. We present four different stack implementations to illustrate options for dynamic allocation:

Figure A.3 uses a single list to represent the stack. It is updated to perform
push
andpop
operations; 
Figure A.4 also uses a list but, instead of updating the list, it replaces the list with a new one for each operation;

Figure A.5 represents a stack as a recursively nested tuple \((v, f)\), where v is the element on top of the stack and r is a stack that is the remainder;

Figure A.6 implements a stack as a linked list with nodes allocated using the
alloc
module.
While the last option is the most versatile (it allows cyclic data
structures), Harmony does not support garbage collection for memory
allocated this way and so allocated memory that is no longer in use must
be explicitly released using free
.
from stack import Stack, push, pop
teststack = Stack()
push(?teststack, 1)
push(?teststack, 2)
v = pop(?teststack)
assert v == 2
push(?teststack, 3)
v = pop(?teststack)
assert v == 3
v = pop(?teststack)
assert v == 1
def Stack() returns stack:
stack = []
def push(st, v):
(!st)[len(!st)] = v
def pop(st) returns next:
let n = len(!st)  1:
next = (!st)[n]
del (!st)[n]
import list
def Stack() returns stack:
stack = []
def push(st, v):
!st += [v,]
def pop(st) returns next:
let n = len(!st)  1:
next = (!st)[n]
!st = list.subseq(!st, 0, n)
def Stack() returns stack:
stack = ()
def push(st, v):
(!st) = (v, !st)
def pop(st) returns next:
let (top, rest) = !st:
next = top
!st = rest
from alloc import malloc, free
def Stack() returns stack:
stack = None
def push(st, v):
!st = malloc({ .value: v, .rest: !st })
def pop(st) returns next:
let node = !st:
next = node>value
!st = node>rest
free(node)
Comments
Harmony supports the same commenting conventions as Python. In particular,
anything after a #
character on a line is ignored. You can also enclose
comments on separate lines within triple quotes. In addition,
Harmony supports nested multiline comments of the form (* comment *)
.
Type Checking
Harmony is dynamically typed. You can add type annotations to your program in the form of assertions and invariants. For example:
invariant (type(x) == "int") and ((x % 2) == 0)
x = choose { 0, 2, 4, 6 }
def double(n) returns result:
assert type(n) == "int"
result = n * 2
assert type(result) == "int"
def main():
x = double(x)
spawn main()
The invariant in Line~1 states that x
is an even integer.
The assertion in Line~5 states that the argument to function
double
is an integer. The assertion in Line~7 states that
the return value of the function is also an integer. Harmony
checks these types as it evaluates the program.