Is Epic Games' Verse gradually typed?

Question

I've just watched an interview on YouTube with Simon Peyton Jones where they talk about Epic's Verse language. Here (at roughly 51:30) they start talking about the type system.

Simon mentions that Verse's version of type checking (he calls it verification) is done via functions written in Verse. These functions have to be side-effect free and receive one value as an argument. This argument is then checked inside this function of whether it adheres to the spec of the type we want to define and either succeeds with a certain value (the type checks out) or fails (it doesn't type-check).

For example, to define a type even that only accepts even integers, I could write something along these lines (using Haskell here since I'm not familiar enough with Verse):

int x = True -- pseudo function to check whether a value is an integer

even x | int x && x `mod` 2 == 0 = x
       | otherwise = error "doesn't type check"

-- pseudo Haskell
x :: even
x = 1 -- uneven, type error
x = 2 -- even, ok

Now this is a fairly easy example where a compiler could figure this out statically (I guess this is what refinement types are?), but what happens if the compiler cannot see the value of x (e.g. it's read from stdin at runtime)?

At 53:35 in the interview, Simon then explains some of the benefits of static type checking and how Verse approaches this topic. He then says, that the verifier can either accept or fail a type test, but it (in my opinion) sounds like failing verification doesn't necessarily result in the program being rejected by the compiler (see 55:00). Does this mean that there will be some sort of type checking happening at runtime? Or does he just mean that type checking can fail for rather arbitrary/opaque reasons until the verifier is more fleshed out?

Disclaimer: I'm not an expert in PL design, so I might've gotten some details wrong. I apologize in advance.

Answer 1

It's worth noting that gradual typing does not mean checking types at run time (in either direction). Verse is not gradually-typed because it does not permit untyped code to exist: "a type is assigned to every identifier".

The purpose of verification of this sort is to allow expressing complex constraints on values that are fairly straightforward to write code for, but hard to describe out of typical type combinators. These could represent calculations on numbers or strings ("starts with < and ends with >), constraints on multiple values ("x is within the range of indices of array y), and so on. The compiler will attempt to confirm that the predicate is always true, based on the knowledge it has about the program state at the relevant point.

The portion of the discussion you link to at 55:00 does not seem to be suggesting that unverified programs can run at all, but in fact explicitly saying the opposite.

Unlike Haskell, there won't be a clean bright line between programs that can be verified and programs that can't, right, because it'll be a function of just how smart the verifier has become. On any one day we might hope to characterise as precisely as possible where that boundary lies, but it is a boundary that will move over time.

The point is that future advancements in the verifier may permit additional predicates to be verified, or additional code to be confirmed as meeting the requirements that couldn't be today. The example given earlier is knowing that x^2 is always non-negative — the verifier may not know that today, and so not allow that expression to be assigned to a natural-number variable, but a future version that had the "x^2 can't be negative" rule included would accept the same code. Until then, the program would be rejected as unverifiable.

It even goes on to discuss hypothetical user-controlled extensions where the user might add a false rule, and notes that this could cause the program to crash in a horrible way; this is not a concern if you're already allowing unverified programs to run!

In your example, if the compiler cannot see the value of x, and doesn't have any guarantee from elsewhere that it must be an even number, then verification fails, and the program is rejected.

---

There are languages using this sort of verification that do permit deferring some checks to run time, and crash in a controlled way if they are found not to be met. Even then, it's usually seen as a stopgap. Verse does not appear to be one of those, and I wouldn't consider the ones that do to be gradually-typed either; the gradual typing people have very specific ideas of what that term means and it fundamentally requires that removing annotations is possible without affecting program behaviour.