Simon Peyton Jones, Tim Sweeney
Lennart Augustsson, Koen Claessen, Ranjit Jhala, Olin Shivers
Epic Games
December 2022

Tim’s vision of the metaverse

 Social interaction in a shared real-time 3D simulation
 An open economy with rules but no corporate overlord A creation platform open to all programmers, artists, anddesigners, not a walled garden

 Much more than a collection of separately compiled, staticallylinked apps: everyone’s code and content must interoperate
dynamically, with live updates of running code Pervasive open standards. Not just Unreal, but any othergame/simulation engine e.g. Unity.

Like the metaverse vision, Verse itself is open We will publish papers, specification for anyone to implement
 We will offer compiler, verifier, runtime under permissive
open-source license with no IP encumbrances.

Goal: engage in a rich dialogue with the community that will
make Verse better.

 Objectively: no. All languages are Turing-complete.
 But we think we can do better with a new language

 Scalable to running code, written by millions of programmers who do notknow each other, that supports billions of users
 Transactional from the get-go; the only plausible way to manage
concurrence across 1M+ programmers
 Strong interop guarantees over time: compile time guarantees that a
module subsumes the API of the previous version.

 And …

 Learnable as a first language (c.f. Javascript yes, C++ no) Extensible: mechanisms for the language to grow over time, without
breaking code.

❑❑❑Verse 1: a familiar FP subset
Verse 2: choice
Verse 3: functional logic Verse is a functional logic language (like Curry or Mercury).
 Verse is a declarative language: a variable names a single
value, not a cell whose value changes over time.
 Verse is lenient but not strict: Like strict:, everything gets evaluated in the end Like lazy: functions can be called before the argument has a value

 Verse has an unusual static type system: types are firstclass values.

 Verse has an effect system, rather than using monads.

 A subset of Verse is a fairly ordinary functional language Integers

3 Tuples/arrays

3+7
(3,4)

fst(3,4)“array{..}” islong-form
syntaxarray{3,4}((92,2),3, 4)a[7]array{3}Indexing

Singleton
tuple

Syntax: ":=” and “;”

x:=3; x+x
x:=3; y:=x+1; x*yy:=x+1; x:=3; x*y
Order does
not matter

For now, think“letrec-binding”

Arguments on
the LHS…

f(x:int):int := x+1;f(3)..or use lambda

f:=(x:int=>x+1); f(3)Verse uses infix “=>” for lambda

fac(x:int):int :=if (x=0) then 1 else n * fac(n-1)

Conditionals

Recursion

 A Haskell expression denotes one value A Verse expression denotes a sequence of zero or more values

3

Choiceoperator

One value

3 | 4

Two values

false?

Zero values

1..10

Ten values

A quirky notation
for “fail”

x:=(1|7|2); x+1

Denotes sequence of
three values: 2, 8, 3

 A bit like Haskell list comprehension[x+1 | x<-[1,7,2]]

 Key point: a variable is always bound to a single value,
not to a sequence of values. I.e.
 We execute the (x+1) with x bound to 1, then with x bound to 7, thenwith x bound to 2.
 Not with x bound to (1|7|2)

 What sequence of values does this denote?

x:=(1|2); y:=(7|8); (x,y)
 Answer: (1,7), (1,8), (2,7), (2,8)
 Like Haskell list comprehension [(x,y) | x<-[1,2]; y<-[7,8]]
 But more fundamentally built in Key point again: a variable is always bound to a single value,
not to a sequence of valuesx:=(1|2); y:=(7|8); (x,y)
 You can also write((1|2), (7|8))

 This still produces the same sequence of pairs,
not a single pair containing two sequences!

 Same for all operations

77 + (1|3)

means the same as(77+1) | (77+3)

77 + false?

means the same as

false?

 What sequence of values does this denote?

x:=(y|2); y:=(7|8); (x,y)
 Answer: (7,7), (8,8), (2,7), (2,8)
 Order of results is still left-to-right But data dependencies can be “backwards”
 Haskell[(x,y) | x<-[y,2]; y<-[7,8]]-- Rejected!

 No Booleans!

if (e) then e1 else e2
 Returns e1 if e succeeds
 “Succeeds” = returns one or more values

 Returns e2 if e fails
 “Fails” = returns zero values

if (x<20) then e1 else e2
 (x<20)

 fails if x >= 20
 succeeds if x < 20, returning the left operand Example: (3 + (x<20)) Succeeds if x=7, returning 10
 Fails if x=25

 Example: (0 < x < 20) Succeeds if x is between 0 and 20, returning 0 Fails if x is out of range
if (0<x<20)
 (<) is right-associativec.f. Haskell

then e1 else e2

if (0<x && x<20) then … else …

if (x<20, y>0) then e1 else e2
 The tuple expression (x<20,y>0) fails
if either (x<20) or (y>0) fails

if (x<20 | y>0) then e1 else e2
 Choice succeeds if either branch succeeds

if (x=0) then e1 else e2
 (x=0) fails if x is not zero succeeds if x is zero, returning x

As we will see, “=” is asuper-important operator

 “If x is 2 or 3 then…”

if (x=(2|3)) then e1 else e2
c.f. Haskell

if (x==2 || x==3) then … else…

 for turns a choice into a tuple/arrayfor{ 3 }The singleton tuple, array(3)for{ 3 | 4 }The tuple (3,4)

for{ false? }The empty tuple ()for{ 1..10 }The tuple (1,2,…, 10) for turns a choice into a tuple/arrayfor{ 3 | 4 }The tuple (3,4)

for{ 4 | 3 }The tuple (4,3)

 That’s why we say that an expression denotes a sequence ofvalues, not a bag of values, and definitely not a set.
 So “|” is associative but not commutative

for e1 do e2
Form the N-tuple from thevalue(s) of range e2

Iterate over the N (non-failing)
choices in the domain e1for (i:=1..3) do i*i(variables bound in e1 scope over e2)=( (1*1), (2*2), (3*3))=(1,4,9)for e1 do e2
Form the N-tuple from thevalue(s) of range e2

Iterate over the N (non-failing)
choices in the domain e1(variables bound in e1 scope over e2)

 Range expression can yield multiple valuesfor (i:=1..3) do (i|i+7)==

And we can use thatchoice to iterate:( (1|8), (2|9), (3|10) )(1,2,3) | (1,2,10) |(1,9,3) | (1,9,10) |..

xs := for(1..5) do (0|1|2); ...xs...

xs is successively bound to all
5-digit numbers in base 3

for e1 do e2
Form the N-tuple from thevalue(s) of range e2

Iterate over the N (non-failing)
choices in the domain e1(variables bound in e1 scope over e2)

 Range expression can failfor (i:=1..4) do (i<3)=(1<3, 2<3, 3<3, 4<3)=

(1, 2, false?, false?)=

false?

for e1 do e2
Form the N-tuple from thevalue(s) of range e2

Iterate over the N (non-failing)
choices in the domain e1(variables bound in e1 scope over e2)

 Domain expression can failfor (i:=1..4, isEven(i)) do (i*i)=(2*2, 4*4)=

(4,16)

1..n is (1 | 2 | ... | n)for{i:=1..Length(as); as[i]+1}

Returns (4,8,5)

 Indexing an array/tuple, as[i], fails on bad indicesas:=(3,7,4)

as[0]Denotes one value, 3as[2]Denotes one value, 4

as[7]Fails: denotes zero values

if (x:=as[i]) then x+1 else 0

Returns 0 if i is out of range

New: i:int brings i into scope
without giving it a value

as:=(3,7,4);for{i:int; as[i]+1}
 What values can i take? Clearly just 0,1,2!
 So expand as[i] to those three choices
 This is called “narrowing” in the functional logic literature
as:=(3,7,4);for{i:int; as[i] + 1}

Haskell=as:=(3,7,4);for{i:int; ((i=0; 3+1) |(i=1; 7+1) |(i=2; 4+1)) }array (bounds a) [ (i,a!i + 1) | i<-indices a ]Fails on empty tuple

head(xs):= xs[0]tail(xs):= for{i:int; i>0; xs[i]}cons(x,xs):= for{x | xs[i:int]}
snoc(xs,x):= for{xs[i:int] | x}
append(xs,ys) := for{xs[i:int] | ys[j:int]}
map(f,xs):= for{f(xs[i:int])}x:=7; x+1>3; y=x*2
means the same as

x:int; x=7; x+1>3; y=x*2
Bring x into
scope.
I’m not telling
you what its
value is yet

By the way,
x must be 7
(or else fail)The very same“=” as before

x:=7; x+1>3; y=x*2
means the same as

Think:• “:” brings the variable
into scope.
• Scope extends to theleft as well as right

x:int; x=7; x+1>3; y=x*2
means the same asx=7; x+1>3; y=(x:int)*2
x+1>3; y=(x:=7)*2

 Haskell

 Verselet (y,z) = if (x=0) then (3,4)
else (232, 913)
in y+zBring y,z into scope

y:int; z:int;
if (x=0) then { y=3;
z=4 }else { y=232; z=913 };y+z
Give them values Partial values

x:tuple(int,int);
x = (2,y:int);
x = (z:int,3);x

x’s first component is 2
y is a fresh unbound variable

x’s second component is 3
z is a fresh unbound variable You can even pass those in-scope-but-unbound variables to afunctionf(p:int,q:int):int:= if (x=0) then { p=3;
q=4 }else { p=232; q=913 };y:int; z:int;f(y,z);
Pass y,z to f, which binds
each of them to a value
y+z…and add up theresults

f(p:int,q:int):int :=if (x=0) then { p=3;
q=4 }else { p=232; q=913 };y:int; z:int;f(y,z);y+z

 y,z look very like logical variables in Prolog,
aka “unification variables”.

 And “=” looks very like unification.

 We can do the usual “run functions backwards” thingswap(x:int, y:int) := (y,x)

swap(3,4)

Run swap “forward”: returns (4,3)

w:tuple(int,int);swap(w) = (3,4);w

Run swap “backward”: Also returns (4,3)

 What does this do?
Sets the valueof x

x:int; y:int;
if (x=0) then y=1 else y=2;
x=7;
yReads theSets thevalue of x
value of y

 One plan (Curry): two different equality operators
 Verse plan: inside a conditional scrutinee, variables bound outside (e.g. x) are“rigid” and can only be read, not unified
 outside, x is “flexible” and can be unified Clearly Verse cannot be strict“Residuation”

 call-by-value
 with a defined evaluation orderbecause earlier bindings may refer to later ones;
and functions can take as-yet-unbound logical variables as arguments And it cannot be lazy, because all those “=“ unifications must
happen, to give values to variables.
 So Verse is lenient Everything is eventually evaluated But only when it is “ready”
 Like dataflow

x:int;
if (x=0) …;
f(x);…

‘if’ is stuck until x
gets a value
Let’s hope f
gives x its value MaxVerse: the glorious vision.
A significant research project in its own right.

 ShipVerse: a conservative subset we will ship to users in2023.

 MaxVerse is a big language

MaxVerse code To give it precise semantics, we use a small Core Verse
language:
CoreVerse code
 Desugar MaxVerse into CoreVerse Give precise semantics to CoreVerse CoreVerse might well be a good compiler intermediate language Analogy:
 MaxVerse = Haskell
 CoreVerse = Lambda calculus“=” is a language construct, not a primop (like gt)

<v1,..,vn> for tuples to avoid ambiguity with (x)“x” is what we previously wrote “x:ty” (except I’m not telling you about types)

fail is a language construct, alongside “|”Core Verse is untyped (like lambda calculus)

x:tuple(int,int);
x = (2,y:int);
x = (z:int,3);x

Desugarx. x = (y. <2,y>);x = (z. <z,3>);x

 Main constructs
 exists
 unification
 sequencing
 choice conditional
 for-loops=;|, failoneallbrings a variable into scopesays that two expressions have the same value
sequences unifications

return first successreturn all successesx. x = (y. <2,y>);x = (z. <z,3>);x Execution = “solve the equations”
 Find values for the exists variables that make all the equations true.

 In this example:
 x=<2,3>, z=2, y=3

 Operationally: unification.
 But unification is hard for programmers
 backtracking, choice points, undoing, rigid variables, …

foo x = x*x + 1
foo (3+2)
foo 5

5*5 + 1

let x=3+2 in x*x + 1(3+2)*(3+2) + 1
5*(3+2) + 1(3+2)*5 + 1

25 + 126

let x=5
in x*x + 1

5*5 + 1

 To answer "what does this program do, or what does it mean?“just apply the rewrite rules
 Rewrite rules are things like
 Add/multiply constants
 Replace a function call with a copy of the function's RHS, making substitutions
 Substitute for a let-binding You can apply any rewrite rule, anywhere, anytime They should all lead to the same answer (“confluence”)

 Good as a way to explain to a programmer: just source-to-source rewrites
 Good for compilers, when optimising/transforming the program Not good as a final execution mechanism

x:tuple(int,int);
x = (2,y:int);
x = (z:int,3);x

Desugarx. x = (y. ⟨2,y〉);x = (z. ⟨z,3〉);x

x:tuple(int,int);
x = (2,y:int);
x = (z:int,3);x

x. y. z. x = ⟨2,y〉;x = ⟨z,3〉;x

Desugarx. x = (y. ⟨2,y〉);x = (z. ⟨z,3〉);x

x:tuple(int,int);
x = (2,y:int);
x = (z:int,3);x

x. y. z. x = ⟨2,y〉;x = ⟨z,3〉;x

Desugarx. x = (y. ⟨2,y〉);x = (z. ⟨z,3〉);xxyz. x = ⟨2,y〉; ⟨2,y〉= ⟨z,3〉; x

Substitute for(one occurrence of) x

x:tuple(int,int);
x = (2,y:int);
x = (z:int,3);x

x. y. z. x = ⟨2,y〉;x = ⟨z,3〉;x

x. x = (y. ⟨2,y⟩);x = (z. ⟨z,3⟩);x

Desugarxyz. x = ⟨2,y〉; ⟨2,y〉= ⟨z,3〉; xxyz. x = ⟨2,y〉; z=2; y=3; x

Decompose equalityof pairs (unification)

x:tuple(int,int);
x = (2,y:int);
x = (z:int,3);x
Substitute forx.anothery. z. x = ⟨2,y〉;occurrence of xx = ⟨z,3〉;xxyz. x = ⟨2,y〉; y=3; z=2; ⟨2,y〉xyz. x = ⟨2,y〉; y=3; z=2; ⟨2,3〉

Desugarx. x = (y. ⟨2,y〉);x = (z. ⟨z,3〉);x

Substitute for yxyz. x = ⟨2,y⟩; ⟨2,y⟩=Garbage⟨z,3⟩; x collectxyz. x = ⟨2,y〉; y=3; z=2; x⟨2,3〉

x:tuple(int,int);
x = (2,y:int);
x = (z:int,3);x

x. y. z. x = ⟨2,y〉;x = ⟨z,3〉;xx. y. z. x = ⟨2,y〉;x = ⟨z,3〉;⟨z,3〉
xyz. x = ⟨2,y〉; z=2; y=3; ⟨2,3〉

Desugarx. x = (y. ⟨2,y〉);x = (z. ⟨z,3〉);xxyz. x = ⟨2,y〉; ⟨2,y〉= ⟨z,3〉; ⟨z,3〉

xyz. x = ⟨2,y〉; z=2; y=3; ⟨z,3〉⟨2,3〉 Desugar conditionals like this:one: a new, simpler construct

Variables bound in e1 can scope over e2

 Rewrite rules for one

 Desugar for-loops like this:

Variables bound in e1 canscope over e2

 Rewrite rules for ‘all’ How to rewrite (e1 | e2)?

Duplicate surrounding context
E.g. (x + (y | z) *2) → (x + y*2) | (x + z*2)

 First attempt to give a deterministic rewrite semantics to afunctional logic language.

 Much more detail, lots of examples
 Sad lack of a confluence proof. It’s tricky. Details maychange.

 Mutable state, I/O, and other effects.
 An effect system, not a monadic setup

 Pervasive transactional memory Structs, classes, inheritance The type system and the verifier – lots of cool stuff here In Verse, a “type” is simply a function
 that fails on values outside the type
 and succeeds on values inside the type

 So int is the identity function on integers, and fails otherwise
 isEven (which succeeds on even numbers and fails otherwise) is a type array int succeeds on arrays, all of whose elements are integers...
hmm, scratch head... ‘array’ is simply ‘map’!



𝜆𝑥. ∃𝑝, 𝑞. 𝑥 = 𝑝, 𝑞 ; 𝑝 < 𝑞 is the type of pairs whose first component issmaller than the second The Verifier rejects programs that might go wrong. This is wildly
undecidable in general, but the Verifier does its best.

 Verse is extremely ambitious
 Kick functional logic programming out the lab and into the mainstream Stretches from end users to professional developers
 Transactional memory at scale Very strong stability guarantees
 A radical new approach to types

 Verse is open
 Open spec, open-source compiler, published papers (I hope!)

Before long: a conversation to which you can contribute