BAM Weblog

Type system of Fortnite's Verse language

Brian McKenna — 2023-03-29

Epic Games released an initial public implementation of the Verse programming language. Verse has been designed by some people who really know what they’re doing:

  • Lennart Augustsson
  • Joachim Breitner
  • Koen Claessen
  • Ranjit Jhala
  • Simon Peyton Jones
  • Olin Shivers
  • Tim Sweeney

It’s amazing to see a CEO help design a programming language but Tim Sweeney has been advocating for functional programming in games since at least 2000 and has previously worked on dependent typing.

I’ve read comments that it’s funny for Fortnite to use such a unique and interesting functional programming language. First of all, why not implement Fortnite using functional programming? But it’s also missing the point.

The goal behind Verse is even more ambitious. When people think of Fortnite, they’re probably thinking about the battle royale game mode. A battle royale lobby has just 100 players, which fit within a single compute shard.

But Fortnite is much more than just battle royale. A huge number of Fortnite players are on custom game modes made by people outside of Epic Games. It’s easy to imagine game modes having a few thousand players which can’t fit within a single shard. How do you scale to handle all that game state, correctly?

Software transactional memory is at the core of Verse. Computation is categorised by transactions and ability to rollback. The goal is to make it easy to write working software across multiple servers. A big goal; we don’t often see programmers do that successfully!

As a functional programmer, here are my thoughts about the current implementation of the Verse type system.

Types are values

Type aliasing is giving names to types. In Verse, this works just like giving names to any other values.

ExampleValue := "Hello world"

integer := int
optional(a : type)<computes> := ?a

This might remind you of Agda or Idris, where type aliases are written in pretty much the same way.

Which might make you ask about full on dependent typing! Let’s try something simple:

int_or_float(b : logic)<computes> : type :=
  if(b?):
    int
  else:
    float

X : int_or_float(true) := 10
Y : int_or_float(false) := 10.0

The above compiles, which seems fantastic! We should have a type which depends on a boolean (called logic in Verse) - but wait!

Z : int_or_float(false) := "Hello"

The above also compiles. How does that make any sense?

int_or_float doesn’t actually represent either an int or a float. It always represents the any type! I’m not sure why but it happens whenever you have an explicit return type of type. All of the following uselessly represent the any type:

any1 : type := int
any2 : type := string
any3() : type := interface:
any4() : type := class:

I thought that Verse should just make explicit returns of type into an error, but the issue is much deeper. You can write a function which allows explicit type ascription and things are still broken:

The(x : type, X : x)<computes> : x := X
typeOfInt()<computes> := The(type, int)

# Broken()<computes> : int := The(typeOfInt(), 1)

And I have no idea what the error means:

This function parameter expects a value of type tuple(type(false, int),int), but this argument is an incompatible value of type tuple(supertype(int),type{1})

So explicitly referencing type is only useful in type parameters and the only way to define an alias is to not say it returns a type. Maybe we can get dependent types without that! Let’s try something super simple:

documentedInt(S : string)<computes> := int

Nope, doesn’t compile. We hit an explicit Verse restriction and get an error message:

Parameters of a function without a specified return type must be of type type.

So actual dependent types are specifically prohibited right now, but I’m guessing that some form of dependent types are coming soon. The only paper available on Verse is on the untyped Verse Calculus, so it’s hard to say, but this really looks like it’s “just” an implementation restriction.

Simon Peyton Jones also gave an interesting type example at the Haskell Exchange:

isEven (which succeeds on even numbers and fails otherwise) is a type

But he must have been talking about this theoretically because I can not see a way of actually doing that today.

Higher-kinded types

It’s almost possible to express the kind of type constructors:

typeConstructor := type{_(:type)<computes> : type}

This type checks but suffers from the same problem with type being used as a return type - it’s inferred to be any.

But we don’t have to use that broken alias, syntactically we can write down a functor interface like so:

functor(F(: type)<computes> : type) : type := interface:
    Map(a : type, b : type, G(:a)<computes> : b, MA : F(a))<computes> : F(b)

But this has an explicit return type of type which means it’s equivalent to any. If we remove that explicit return type we’ll again get the message about parameters only being able to be type:

Parameters of a function without a specified return type must be of type type.

So I think we’re blocked on being able to reduce code duplication. You’ll have to write functions for lists, maps, arrays, optionals, etc. separately. Code duplication! Gross!

Effects

The effect system is different from most others, it’s all about transactions. The “exclusive effects” are:

  • Converges (terminates)
  • Computes (pure)
  • Varies (reads random or non-constant state)
  • Transacts (has mutation)
  • No rollback (side-effects)

You can’t write your own effects and you can’t write effect handlers. It’s all built-in to Verse. You can’t even write a converges function today, that’s reserved for native code. I can imagine Verse gaining a totality checker to enable writing non-native converges functions.

The documentation says that the default effect is no_rollback but this isn’t true for at least one case. Above I wrote a type alias for optional types:

optional(a : type)<computes> := ?a

But it looks like when Verse infers a return of type, it implicitly adds the computes effect. So this is equivalent:

optional(a : type) := ?a

What about effect polymorphism? For example, these two functions are not the same:

Twice(F() : void) : void :=
  F()
  F()

TwiceTransacts(F()<transacts> : void)<transacts> : void :=
  F()
  F()

Sadly Verse doesn’t support writing it just once, but it’s easy to imagine:

Twice(e : exclusive_effect, F()<e> : void)<e> : void :=
  F()
  F()

Since effects are quite limited, I’m not sure how useful effect polymorphism would be in a production system. I can easily see it being possible but I’m not sure there would be a demand for it.

Documentation

From reading forum posts, it looks like Verse has been in alpha testing for at least 6 months. I’m guessing the documentation has been slowly written over this time because I can see things which are slightly off but which might have worked at some point in Verse’s development.

The page on Type Aliasing says parametric type aliases are not supported, but the example given actually seems to work totally fine:

comparison := enum:
    LT
    EQ
    GT

predicate(t : type) := type{_(:t, :t)<computes> : comparison}
compareInts(a : int, b : int)<computes> : comparison :=
    if (a > b):
        comparison.GT
    else if (a = b):
        comparison.EQ
    else:
        comparison.LT
intPredicate : predicate(int) := compareInts

The last example from Parametric Types has a shadowed name (i.e. t) - which Verse doesn’t allow:

class4(t : type) := class:
    Property : ?t

    Flatten(X:?class4(t) where t:type):?t =
        if (Y := X):
            Y.Property
        else:
            false

The first example for the Type Macro doesn’t work at all because Foo needs to have a computes effect to be used in a type context and the type macro just doesn’t support arbitrary expressions at all - it only supports function types!

Foo() : int = 0
Bar(X : type{Foo()}) : type{Foo()} = X

Finally, at the bottom of each of the documentation pages there’s a link to a “Learning Library” which is 404.

Since most of these documentation issues are about restrictions, I’m going to guess the restrictions were added/removed after the documentation was already written. I think Verse team just needs some help to keep the docs up to date!

Summary

I remember getting into programming by modding games like Half-Life. I struggled with learning C++ to be able to build the experiences that I wanted to make. I’m really excited that there will be 12-year-olds being introduced to programming by making Fortnite islands, using Verse and functional programming. On the public release day of Verse and the Unreal Editor for Fortnite, over 1000 projects were created every minute. The number of people who will learn functional programming using this tool is extremely exciting!

Verse’s compiler and tooling are currently closed source but both Tim Sweeney and Simon Peyton Jones have said that Verse is going to be open at some point.

I can see a path to full dependent types and I believe some form of dependent typing must be coming in the near future. It looks like dependent types have just been explicitly been disallowed for reasons, I’m guessing mostly implementation.

The same restrictions make it impossible to abstract over type constructors and higher-kinded types. Code duplication will be here until this restriction is lifted and I hope it is long before full dependent types are sorted out.

The effect system is very limited and definitely not the algebraic form that functional programmers might be used to. Some categories will be familiar (e.g. computes means pure) but don’t be confused and expect Verse effects to have any extensible functionality in terms of IO, configuration, error handling, etc.

The Verse team needs to start automating their documentation pages, they’re slightly outdated and I’m sure the Verse team is making changes quickly given the massive influx of users.

Verse has some interesting features and is a key part of an enormous project. Very exciting, I’ll continue to follow closely!

Please enable JavaScript to view the comments powered by Disqus.