Today, we released Pact 2.0 to our open source repo. The headline feature is the addition of static/explicit types.
Why was Pact untyped before?
Pact was designed to be highly legible, and easy to program. Our goal in not having types was to keep clutter out of the code, and enable rapid prototyping and development. With database programming, we liked the idea of being able to add extra data to a row to capture arbitrary event details that weren’t important to the smart contract functionality itself.
With Pact 2.0, you can still code this way. But most importantly, you can get all the benefit of strong typing without littering types all over your code, thanks to the magic of type inference.
Type Inference in Pact
Pact types, when specified, are enforced at runtime. If you say that argument a of your function is a string and the user passes in an integer, the interpreter enforces this and errors out before your function executes.
As such, Pact does no typechecking when you load code into the environment. Instead, the REPL environment offers the typecheck function, which will perform type inference on the entire module and alert you to any type errors, or anywhere it cannot determine the type.
The type inference algorithm is based on Hindley-Milner, although it is “lazier” about function types for some native functions which are overloaded. For instance, the + function is heavily overloaded to handle numbers, lists, objects and strings, and even handle upcasting integer/decimal combinations:
Overloads for +
x <a[integer,decimal]>, y <a[integer,decimal]> → <a[integer,decimal]>
x <a[integer,decimal]>, y <b[integer,decimal]> → decimal
x <a[string,[<l>],object:<{o}>]>, y <a[string,[<l>],object:<{o}>]>
→ <a[string,[<l>],object:<{o}>]>As a result, the type inference must first substitute all types for non-overloaded functions, before attempting to solve each overload.
Also, Pact does not typecheck user code as-is. When it typechecks a function, it resolves the entire AST of the function with all of its references fully inlined. As a result, function types as specifid are not used per-se, but instead applied piecewise to the AST elements in whatever application is using them.
So, Pact inference is its own unique beast, but it works well and is a superb development aid.
Formal Verification
The typechecker is also essential for a new feature we will be demonstrating at the Stanford Blockchain Conference: formal verification of Pact functions by compiling Pact to SMT-LIB2 and using Z3.
The typechecker’s exploded, inlined AST result is precisely what is needed for SMT-LIB2 compilation. Since Pact is already SSA and Turing-incomplete, its compiled form is strikingly similar to the SMT language.
Preview of Z3 compilation
But the code must fully typecheck: the prover can’t work with anything but concrete types.
Code Your Way
Type inference makes for a pretty unique system. You can code without types altogether, relying on unit tests to provide necessary coverage.
;; module with no types
(module pay 'module-keyset
(deftable accounts)
(defun pay (from to amount)
(with-read accounts from { "balance":= from-bal }
(with-read accounts to { "balance":= to-bal }
(check-balance)
(update accounts from
{ "balance": (- from-bal amount),
"amount": (- amount) })
(update accounts to
{ "balance": (+ to-bal amount),
"amount": amount }))))
(defun check-balance (balance amount)
(enforce (>= balance amount) "Insufficient Funds")))You can use the typechecker to add “just enough” types for it to be happy, meaning you’re fully type-safe, and no more. Why have the runtime check more types than it absolutely needs?
;; module with schema and types to keep TC happy
(module pay 'module-keyset
(defschema account
balance:decimal
amount:decimal)
(deftable accounts:{account})
(defun pay (from to amount)
(with-read accounts from { "balance":= from-bal }
(with-read accounts to { "balance":= to-bal }
(check-balance)
(update accounts from
{ "balance": (- from-bal amount),
"amount": (- amount) })
(update accounts to
{ "balance": (+ to-bal amount),
"amount": amount }))))
(defun check-balance (balance:decimal amount)
(enforce (>= balance amount) "Insufficient Funds")))Note that last function: since >= expects both arguments to be the same type, the typechecker only needs to know the type of one of the arguments.
But, you might want types to document your API. So go fully-typed:
;; module with schema and types to keep TC happy
(module pay 'module-keyset
(defschema account
balance:decimal amount:decimal)
(deftable accounts:{account})
(defun pay (from:string to:string amount:decimal)
(with-read accounts from { "balance":= from-bal }
(with-read accounts to { "balance":= to-bal }
(check-balance)
(update accounts from
{ "balance": (- from-bal amount),
"amount": (- amount) })
(update accounts to
{ "balance": (+ to-bal amount),
"amount": amount }))))
(defun check-balance (balance:decimal amount:decimal)
(enforce (>= balance amount) "Insufficient Funds")))Actually the example is still not fully-typed: pay is string, since update returns a status message; check-balance is bool, per enforce. They don’t add any information to your API, so why bother?
Other benefits of type inference
Coders familiar with Haskell or Scala know how nice type inference is, compared to Java or C++: once you go inference-style, other code just seems riddled with warts everywhere, harming readability.
In Pact’s case, there are other benefits too. Leaving types off will cause the typechecker to fail if a variable is unused, as it can’t use a function signature to infer the type. This is especially helpful during refactoring, where maybe you’re no longer updating that one field in the database: the typechecker’s complaints might save the day!
What’s the big deal?
With type inference and database schemas, the typical database-focused pact code won’t need any types outside of the schemas. At which point Pact starts to look a lot like SQL, which is of course strongly-typed by dint of the column types in the database, without needing to declare them in each query.
That’s a good thing: we want Pact to stay as streamlined as possible. Meanwhile, though, there is a sophisticated type inference engine that can handle far more complex scenarios that don’t touch the database: for all of it’s Turing-incompleteness, single-assignment, and simplicity, Pact is still a full programming language. As such, it’s nice to have an advanced feature like type inference to boost productivity!
